Variance

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), realization bound

The Efron–Stein sensitivity step of p.fixed.phase.variance assembled at the level of a single (everywhere-(1,Θ)-elliptic) realization pair a, a'.

For two fields elliptic on the closed cube U := cubeSet (originCube d m), the summed squared resampling deviation over any finite family of cores obeys the max·sum estimate of §4.3:

Σ_k (F_σ(patchCore k a a') − F_σ(a))² ≤ C_d · 4608 · Θ³ · (ℓ/3^m)^{d−2} · (Θ|p|² + |q|²)²,

with the per-core energies bounded by exists_perCore_minimizer_energy_le (Part B) and the total energy by the C1′ sandwich (blockVecDot_coarseBlockMatrix_cube_le). The single minimizer Z for the corridor field serves both the sensitivity (via abs_phaseObservable_resample_sub_le_of_minimizer) and the energies.

This is the deterministic, measurability-free core of Proposition 4.3.

The ratio power identity

Ellipticity of the two-field patch

theorem HCPolySupport.isEllipticFieldOn_patchCore {d : ℕ} {Θ : ℝ} {m : ℤ} {ℓ : ℝ} {σ : Vec d} {k : Fin d → ℤ} {a a' : CoeffField d} (hElla : IsEllipticFieldOn 1 Θ (cubeSet (originCube d m)) a) (hElla' : IsEllipticFieldOn 1 Θ (cubeSet (originCube d m)) a') : IsEllipticFieldOn 1 Θ (cubeSet (originCube d m)) (patchCore ℓ σ k a a')

The two-field core patch of two fields elliptic on the cube is elliptic on the cube.

The total energy of the cores

theorem HCPolySupport.sum_coreEnergy_le {d : ℕ} [NeZero d] {Θ : ℝ} {m : ℤ} {ℓ : ℝ} (hℓ : 0 ≤ ℓ) (σ : Vec d) (P : BlockVec d) {c : CoeffField d} (hEll : IsEllipticFieldOn 1 Θ (cubeSet (originCube d m)) c) {Z : BlockState d} (hZadm : IsBlockMuAdmissible (cubeSet (originCube d m)) P Z) (hZeng : Mu (cubeSet (originCube d m)) P c = blockEnergyAverage (cubeSet (originCube d m)) c Z) (K : Finset (Fin d → ℤ)) : ∑ k : ↥K, ∫ (x : Vec d) in coreBox ℓ σ ↑k ∩ cubeSet (originCube d m), blockVecDot (Z.eval x) (blockMatVecMul (blockCoeffField c x) (Z.eval x)) ≤ 2 * (Θ * vecNormSq P.1 + vecNormSq P.2) * (MeasureTheory.volume (cubeSet (originCube d m))).toReal

The summed core energy is bounded by the whole-cube energy ≤ 2 M² · (3^m)^d.

The per-realization summed-square bound

theorem HCPolySupport.summed_sq_le_of_ellipticFieldOn_uniform {d : ℕ} [NeZero d] (hd : 3 ≤ d) : ∃ (B : ℝ), 0 ≤ B ∧ ∀ {m : ℤ} {Θ : ℝ}, 1 ≤ Θ → ∀ {ℓ : ℝ}, 4 ≤ ℓ → ℓ ≤ 3 ^ m → ∀ (σ : Vec d) (P : BlockVec d) {a a' : CoeffField d}, IsEllipticFieldOn 1 Θ (cubeSet (originCube d m)) a → IsEllipticFieldOn 1 Θ (cubeSet (originCube d m)) a' → ∀ (K : Finset (Fin d → ℤ)), ∑ k : ↥K, (phaseObservable ℓ σ m P (patchCore ℓ σ (↑k) a a') - phaseObservable ℓ σ m P a) ^ 2 ≤ B * Θ ^ 3 * (ℓ / 3 ^ m) ^ (d - 2) * (Θ * vecNormSq P.1 + vecNormSq P.2) ^ 2

Uniform realization bound. The constant-outside form of summed_sq_le_of_ellipticFieldOn: a single dimensional constant B, independent of the realization pair (a, a') and the core family K, bounds the summed squared resampling deviation. Uniformity is inherited from exists_perCore_minimizer_energy_le_uniform.

theorem HCPolySupport.summed_sq_le_of_ellipticFieldOn {d : ℕ} [NeZero d] (hd : 3 ≤ d) {m : ℤ} {Θ : ℝ} (hΘ : 1 ≤ Θ) {ℓ : ℝ} (hℓ4 : 4 ≤ ℓ) (hℓL : ℓ ≤ 3 ^ m) (σ : Vec d) (P : BlockVec d) {a a' : CoeffField d} (hElla : IsEllipticFieldOn 1 Θ (cubeSet (originCube d m)) a) (hElla' : IsEllipticFieldOn 1 Θ (cubeSet (originCube d m)) a') (K : Finset (Fin d → ℤ)) : ∃ (Cd : ℝ), 0 ≤ Cd ∧ ∑ k : ↥K, (phaseObservable ℓ σ m P (patchCore ℓ σ (↑k) a a') - phaseObservable ℓ σ m P a) ^ 2 ≤ Cd * Θ ^ 3 * (ℓ / 3 ^ m) ^ (d - 2) * (Θ * vecNormSq P.1 + vecNormSq P.2) ^ 2

Realization bound for p.fixed.phase.variance. For two fields elliptic on the closed cube, the summed squared resampling deviation over any finite core family satisfies the max·sum estimate of §4.3, with an explicit (ℓ/3^m)^{d−2} scaling.

The per-realization summed-square bound, uniform constant