Two-Moment Support Hole

Abstract

Moving probability atoms determine the exact price of excluding a support interval from a noisy two-moment model.

Definition 1.1 (Actual finite probability pairs).

$$M_H(a,b,\epsilon )=\{w\mid 0\le w\wedge \exists n,m\in \mathbb{N},z,u:\mathrm{Fin}\left(n\right)\to \mathbb{R},y,v:\mathrm{Fin}\left(m\right)\to \mathbb{R},(\forall i,a\le z\left(i\right)\wedge z\left(i\right)<1\wedge \neg (z\left(i\right)\in H))\wedge (\forall j,y\left(j\right)\in [a,b])\wedge (\forall i,0\le u\left(i\right))\wedge (\forall j,0\le v\left(j\right))\wedge w+\sum _{i}u\left(i\right)=1\wedge \sum _{j}v\left(j\right)=1\wedge |w+\mathrm{Prony}\left(z,u,1\right)-\mathrm{Prony}\left(y,v,1\right)|\le \epsilon \wedge |w+\mathrm{Prony}\left(z,u,2\right)-\mathrm{Prony}\left(y,v,2\right)|\le \epsilon \}$$

Formalization. D5/S3/Analytic/TwoMomentSupportHole.twoMomentMassSet (✓ std3).

Source. Repository-derived.

Commentary.

The designated atom is at one. Residual nodes lie in [a,1), outside the specified hole, and comparison nodes lie in [a,b]. Both measures have nonnegative weights and total mass one. The first two actual Prony moments differ by at most epsilon. Arbitrary finite cardinalities are allowed, and the exclusion of one from residual nodes makes w the actual endpoint mass.

Theorem 1.2 (Attained maxima and exact support-loss law).

$$\forall a,b,l,r,t\in \mathbb{R},(0\le a\wedge a<b\wedge b<1\wedge a\le l\wedge l<r\wedge r\le b\wedge l\le t\wedge t\le r\wedge 2t\le a+b\wedge l+r\le a+b)⟶\text{let }\epsilon :=\frac{(1-b)(b-t)}{2+t};c:=\frac{(1-b)(2+b)}{2+t};w_c:=1-\frac{c}{1-t};w_h:=\frac{(b-l)(b-r)+\epsilon (1+l+r)}{(1-l)(1-r)};\mathrm{IsGreatest}\left(M_{\varnothing }(a,b,\epsilon ),w_c\right)\wedge \mathrm{IsGreatest}\left(M_{(l,r)}(a,b,\epsilon ),w_h\right)\wedge w_c-w_h=\frac{(1-w_c)(t-l)(r-t)}{(1-l)(1-r)}$$

Proof. Machine-checked in Lean as D5/S3/Analytic/TwoMomentSupportHole.two_moment_support_hole_sharp (✓ std3). ∎

Source. Repository-derived.

Commentary.

For the stated continuous geometric parameters, epsilon=(1-b)(b-t)/(2+t) yields a moving residual atom at t in the unrestricted optimizer. Excluding (l,r) replaces it by explicit nonnegative masses at l and r. Both optimizers are normalized and saturate the actual first two moment errors. Quadratic certificates bound all competing finite laws and yield two IsGreatest conclusions. Their exact difference is (1-wc)(t-l)(r-t)/((1-l)(1-r)), including boundary zero loss. The complete all-noise curve, fixed-grid consequence and optimal transformed grid have ordinary proofs in the theory; this declaration formalizes the general moving-support and hole comparison.

References

• Truth anchor: D5/S3/Analytic/TwoMomentSupportHole.twoMomentMassSet
• Truth anchor: D5/S3/Analytic/TwoMomentSupportHole.two_moment_support_hole_sharp
• Dependency: D5/S3/Analytic/GoldenTomography/FinitePronyHankelReconstruction