VarianceFinal

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.

The fixed-phase variance (Proposition 4.3), final assembly

This file closes p.fixed.phase.variance. It supplies the two remaining statement-plumbing inputs and chains them with the landed mathematics:

• Joint measurability (Obstruction 2). aestronglyMeasurable_phaseObservable_patchCore shows the two-field resampled observable (a, a') ↦ F_σ(patchCore k a a') is a.e.-strongly-measurable for the product law L ⊗ L. The approach is the one already used in EfronSteinPhase: clampedPhaseObservable is genuinely measurable on the product tuple space, the resampling-update map is measurable, and the exact update identity update_restrict_eq_restrict_patchCore together with the a.s. field congruence clampedPhaseObservable_restrict_eq_of_field (applied at the patched field, which is entrywise-measurable + a.e.-elliptic when both draws are) transfers measurability across the a.e. equality. The diagonal term a ↦ F_σ(a) gets the same treatment (aestronglyMeasurable_phaseObservable_of_thetaLaw).

• Uniform deterministic bound (Obstruction 1, consumed). summed_sq_le_of_ellipticFieldOn_uniform (a single dimensional constant B, independent of the realization pair and the core family) is applied a.s. after a C2-bridge of each realization to everywhere-elliptic representatives; the fixed-phase observable is unchanged under the bridge (phaseObservable_congr_ae).

The chain is efronStein_phaseObservable → integrable per-core terms (bounded a.s. by the uniform B-term + AESM) → sum/integral exchange (integral_prod, integral_finset_sum) → ∫∫ Σ ≤ B-term.

a.e.-congruence of the fixed-phase observable

theorem HCPolySupport.phaseObservable_congr_ae {d : ℕ} {ℓ : ℝ} {σ : Vec d} {m : ℤ} {P : BlockVec d} {b b' : CoeffField d} (hbb' : b =ᵐ[MeasureTheory.volume.restrict (cubeSet (originCube d m))] b') : phaseObservable ℓ σ m P b = phaseObservable ℓ σ m P b'

The fixed-phase observable depends on the coefficient field only through a null-set: if b =ᵐ b' on the cube, the observables agree.

Obstruction 2 — joint measurability

theorem HCPolySupport.aestronglyMeasurable_phaseObservable_of_thetaLaw {d : ℕ} [NeZero d] {ℓ : ℝ} {σ : Vec d} {Θ : ℝ} {m : ℤ} (hℓ : 0 < ℓ) (hΘ : 1 ≤ Θ) (P : BlockVec d) {L : MeasureTheory.Measure (RegCoeffField d)} (hLaw : ThetaEllipticLaw Θ L) (K : Finset (Fin d → ℤ)) (hK : ∀ (k : Fin d → ℤ), (coreBox ℓ σ k ∩ cubeSet (originCube d m)).Nonempty → k ∈ K) : MeasureTheory.AEStronglyMeasurable (fun (a : RegCoeffField d) => phaseObservable ℓ σ m P a.toFun) L

The single-field fixed-phase observable is a.e.-strongly-measurable under any Θ-elliptic law (via the genuinely measurable clamped observable on the diagonal restriction tuple).

theorem HCPolySupport.aestronglyMeasurable_phaseObservable_patchCore {d : ℕ} [NeZero d] {ℓ : ℝ} {σ : Vec d} {Θ : ℝ} {m : ℤ} (hℓ : 0 < ℓ) (hΘ : 1 ≤ Θ) (P : BlockVec d) {L : MeasureTheory.Measure (RegCoeffField d)} (hLaw : ThetaEllipticLaw Θ L) (K : Finset (Fin d → ℤ)) (hK : ∀ (k : Fin d → ℤ), (coreBox ℓ σ k ∩ cubeSet (originCube d m)).Nonempty → k ∈ K) (k : ↥K) : MeasureTheory.AEStronglyMeasurable (fun (p : RegCoeffField d × RegCoeffField d) => phaseObservable ℓ σ m P (patchCore ℓ σ (↑k) p.1.toFun p.2.toFun)) (L.prod L)

Obstruction 2 — joint measurability for the sum/integral exchange. For each core k, the two-field resampled observable (a, a') ↦ F_σ(patchCore k a a') is a.e.-strongly-measurable for the product law L ⊗ L.

The fixed-phase variance (Proposition 4.3)

theorem HCPolySupport.fixed_phase_variance_uniform {d : ℕ} [NeZero d] (hd : 3 ≤ d) : ∃ (Cd : ℝ), 0 ≤ Cd ∧ ∀ {m : ℤ} {ℓ Θ : ℝ} {σ : Vec d}, 4 ≤ ℓ → ℓ ≤ 3 ^ m → 1 ≤ Θ → ∀ (P : BlockVec d) {L : MeasureTheory.Measure (RegCoeffField d)} [MeasureTheory.IsProbabilityMeasure L], IsRestrictionUnitRangeDependentR L → ThetaEllipticLaw Θ L → ProbabilityTheory.variance (fun (a : RegCoeffField d) => phaseObservable ℓ σ m P a.toFun) L ≤ Cd * Θ ^ 3 * (ℓ / 3 ^ m) ^ (d - 2) * (Θ * vecNormSq P.1 + vecNormSq P.2) ^ 2

Uniform-constant fixed-phase variance. The constant Cd = B/2 is independent of m, ℓ, Θ, σ, P, L.

theorem HCPolySupport.fixed_phase_variance {d : ℕ} [NeZero d] (hd : 3 ≤ d) {m : ℤ} {ℓ Θ : ℝ} {σ : Vec d} (hℓ4 : 4 ≤ ℓ) (hℓL : ℓ ≤ 3 ^ m) (hΘ : 1 ≤ Θ) (P : BlockVec d) {L : MeasureTheory.Measure (RegCoeffField d)} [MeasureTheory.IsProbabilityMeasure L] (hURD : IsRestrictionUnitRangeDependentR L) (hLaw : ThetaEllipticLaw Θ L) : ∃ (Cd : ℝ), 0 ≤ Cd ∧ ProbabilityTheory.variance (fun (a : RegCoeffField d) => phaseObservable ℓ σ m P a.toFun) L ≤ Cd * Θ ^ 3 * (ℓ / 3 ^ m) ^ (d - 2) * (Θ * vecNormSq P.1 + vecNormSq P.2) ^ 2

p.fixed.phase.variance (Proposition 4.3). Under a restriction-unit-range-dependent, Θ-elliptic probability law, the variance of the fixed-phase observable obeys the O((ℓ/3^m)^{d−2}) bound with a single dimensional constant.