Multiscale Loewner Constraint

Abstract

One positive spectrum forces its multiscale budget matrix to be positive semidefinite.

Theorem 1.1 (A common resolvent spectrum gives a positive semidefinite scale matrix).

$$\begin{array}{c}\forall M:\mathbb{N},\\ nu:\mathrm{Measure}(\mathbb{R}),\\ u:\mathrm{Fin}(M)\to \mathbb{R},\\ (\forall i:\mathrm{Fin}(M),0<u_i)\wedge \\ \mathrm{Injective}(u)\wedge \\ (\forall t:\mathbb{R},0<t\Rightarrow \mathrm{Integrable}(xi\mapsto \frac{1}{x{i}^2+t},nu))\Rightarrow \\ \mathrm{let}B:\mathbb{R}\to \mathbb{R}:=t\mapsto \mathrm{integral}(nu,xi\mapsto \frac{1}{x{i}^2+t}),\\ \mathrm{let}L:\mathrm{Matrix}(\mathrm{Fin}(M),\mathrm{Fin}(M),\mathbb{R}):=(i,j)\mapsto \mathrm{if}(i=j,-\mathrm{deriv}(B,u_i),\frac{B\left(u_i\right)-B\left(u_j\right)}{u_j-u_i}),\\ \mathrm{PosSemidef}(L).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Weil/Budget/MultiscaleLoewnerConstraint.multiscale_loewner_constraint (✓ std3). ∎

Source. Repository-derived.

Commentary.

The measure is the common positive spectrum. Its budget curve and the piecewise divided-difference matrix are both constructed in the displayed proposition, including the derivative diagonal.

Positive scales make every resolvent finite under the stated integrability law. Distinct scales are the domain condition for the off-diagonal quotient in the source formula.

The proof identifies the matrix with the integral Gram kernel. A local half-scale resolvent dominates differentiation under the integral, so the diagonal identity is derived from the same measure.

References

• Truth anchor: D5/S3/Weil/Budget/MultiscaleLoewnerConstraint.multiscale_loewner_constraint