Christoffel Atom Floor

Abstract

A positive point mass forces a uniform positive floor on normalized polynomial energy and its degree-bounded Christoffel infimum.

Theorem 1.1 (An atom gives every Christoffel cost a positive floor).

$$\forall mu\in \mathrm{Measure}\left(\mathrm{Complex}\left(\right)\right),w\in \mathrm{Complex}\left(\right),m\in \mathrm{ENNReal}\left(\right),\left(\mathrm{MeasureSingleton}\left(mu,w\right)=m\wedge 0<m\right)\Rightarrow \left(\left(\forall p\in \mathrm{Polynomial}\left(\mathrm{Complex}\left(\right)\right),\mathrm{PolynomialEval}\left(p,w\right)=1\Rightarrow \left(\mathrm{Product}\left(m,\mathrm{ENNRealOfReal}\left(\mathrm{ComplexNormSq}\left(\mathrm{PolynomialEval}\left(p,w\right)\right)\right)\right)\le \mathrm{LIntegral}\left(mu,(z\mapsto \mathrm{ENNRealOfReal}\left(\mathrm{ComplexNormSq}\left(\mathrm{PolynomialEval}\left(p,z\right)\right)\right))\right)\wedge \mathrm{Product}\left(m,\mathrm{ENNRealOfReal}\left(\mathrm{ComplexNormSq}\left(\mathrm{PolynomialEval}\left(p,w\right)\right)\right)\right)=m\right)\right)\wedge \left(\forall N\in \mathrm{Nat}\left(\right),m\le \mathrm{ChristoffelEvaluationCost}\left(mu,w,N\right)\wedge 0<\mathrm{ChristoffelEvaluationCost}\left(mu,w,N\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Analytic/ZetaObservation/ChristoffelAtomFloor.christoffel_atom_floor (✓ std3). ∎

Source. Repository-derived.

Commentary.

The Christoffel evaluation cost is the literal infimum of the extended nonnegative squared-norm integral over complex polynomials whose degree is at most N and whose value at w is one.

Restricting the integral to the singleton w gives exactly the atom mass times the squared value there. Monotonicity from the singleton to the whole carrier yields the polynomial bound; taking the infimum yields the same positive floor for every degree.

References

• Truth anchor: D5/S3/Analytic/ZetaObservation/ChristoffelAtomFloor.christoffel_atom_floor