Christoffel Support Decay

Abstract

Unit-circle support supplies normalized monomial witnesses whose geometric energy bound forces exterior Christoffel costs to vanish.

Theorem 1.1 (Unit-circle support forces exterior Christoffel decay).

$$\forall mu\in \mathrm{Measure}\left(\mathrm{Complex}\left(\right)\right),w\in \mathrm{Complex}\left(\right),\left(\mathrm{IsFiniteMeasure}\left(mu\right)\wedge \left(1<\Vert w\Vert \wedge \mathrm{Subset}\left(\mathrm{MeasureSupport}\left(mu\right),\mathrm{sphere}\left(0,1\right)\right)\right)\right)\Rightarrow \left(\left(\forall N\in \mathrm{Nat}\left(\right),\mathrm{let}pN:\mathrm{Polynomial}\left(\mathrm{Complex}\left(\right)\right):=\mathrm{PolynomialMonomial}\left(N,\mathrm{pow}\left(\mathrm{inv}\left(w\right),N\right)\right);\mathrm{NatDegree}\left(pN\right)\le N\wedge \left(\mathrm{PolynomialEval}\left(pN,w\right)=1\wedge \left(\left(\forall z\in \mathrm{Complex}\left(\right),\mathrm{Mem}\left(z,\mathrm{sphere}\left(0,1\right)\right)\Rightarrow \Vert \mathrm{PolynomialEval}\left(pN,z\right)\Vert =\mathrm{pow}\left(\mathrm{inv}\left(\Vert w\Vert \right),N\right)\right)\wedge \mathrm{ChristoffelEvaluationCost}\left(mu,w,N\right)\le \mathrm{MeasureOf}\left(mu,\mathrm{sphere}\left(0,1\right)\right)\cdot \mathrm{pow}\left(\mathrm{inv}\left(\mathrm{ENNRealOfReal}\left(\Vert w\Vert \right)\right),2\cdot N\right)\right)\right)\right)\wedge \mathrm{Tendsto}\left((N\mapsto \mathrm{ChristoffelEvaluationCost}\left(mu,w,N\right)),atTop,\mathrm{nhds}\left(0\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

For every degree, the explicit polynomial w inverse to the N, times z to the N, has degree at most N, equals one at w, and has constant norm on the unit circle.

Support on that circle identifies its full energy with the circle mass times the squared geometric ratio. This admissible witness bounds the canonical cost, and the ratio is below one because w lies outside the circle.

References

• Truth anchor: D5/S3/Analytic/ZetaObservation/ChristoffelSupportDecay.christoffel_support_decay
• Dependency: D5/S3/Analytic/ZetaObservation/ChristoffelAtomFloor