Averaging

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

Grid averaging + choice

Statement of p.phase.comparison's conclusions e.phase.comparison.average / e.phase.comparison.choice in the discrete-grid setting, plus the C4-glue lemma.

C4 glue

ae_coarseBlockQuadratic_bounds_of_thetaEllipticLaw turns the amended ThetaEllipticLaw Θ L (whose measurability conjunct is exactly what makes this possible) into the a.s. C1′ two-sided bound on the coarse observable, by routing each realization through the C2 truncation bridge exists_ellipticFieldOn_ae_eq to an everywhere-(1,Θ)-elliptic representative with the same coarse block matrix, then applying the deterministic C1′ sandwich.

The averaging argument

M2 pointwise-in-a; exchange ∫ ∂L with the finite grid sum (integral_finset_sum); M0 coverage sum_indicator_gridPhase_corridor_le (constant 3d/ℓ); the C4-glue F ≤ 2M²; |F_σ − F|² ≤ 4M²·|F_σ − F|; below-average member of the nonempty grid (N ≥ ℓ ≥ 4 > 0). M² := Θ·|p|² + |q|².

theorem HCPolySupport.ae_coarseBlockQuadratic_bounds_of_thetaEllipticLaw {d : ℕ} [NeZero d] {L : Book.Ch04.RestrictionCoeffLaw d} {Θ : ℝ} (hΘ : 1 ≤ Θ) (hell : ThetaEllipticLaw Θ L) (m : ℤ) (P : BlockVec d) : ∀ᵐ (a : RegCoeffField d) ∂L, 0 ≤ blockVecDot P (blockMatVecMul (coarseBlockMatrix (cubeSet (originCube d m)) a.toFun) P) ∧ blockVecDot P (blockMatVecMul (coarseBlockMatrix (cubeSet (originCube d m)) a.toFun) P) ≤ 2 * (Θ * vecNormSq P.1 + vecNormSq P.2)

C4 glue. Under the amended ThetaEllipticLaw Θ L, the coarse block observable a.s. satisfies the C1′ two-sided bound 0 ≤ F ≤ 2(Θ|p|² + |q|²).

The measurability conjunct of ThetaEllipticLaw supplies the entrywise measurability that the C2 bridge exists_ellipticFieldOn_ae_eq needs; that bridge produces, from each a.s. realization, an everywhere-(1,Θ)-elliptic representative a' with coarseBlockMatrix U a' = coarseBlockMatrix U a, whence the deterministic C1′ sandwich (zero_le_blockVecDot_coarseBlockMatrix_cube, blockVecDot_coarseBlockMatrix_cube_le) transfers.

Per-realization summed bound

For a single measurable, a.e.-(1,Θ)-elliptic realization a, pass it through the C2 bridge to an everywhere-elliptic representative a' with the same coarse block matrices, take the minimizer Z for a' (one Z serves every phase), apply M2-core per phase, and sum with the M0 grid-coverage count 3d/ℓ and the C1′ energy bound F ≤ 2M².

theorem HCPolySupport.gridPhase_summed_sq_le_of_realization {d : ℕ} [NeZero d] {Θ : ℝ} (hΘ : 1 ≤ Θ) {m : ℤ} {ℓ : ℝ} (hℓ : 4 ≤ ℓ) {N : ℕ} (hN : ℓ ≤ ↑N) (P : BlockVec d) {a : CoeffField d} (hmeas : ∀ (i j : Fin d), Measurable fun (x : Vec d) => a x i j) (haeEll : ∀ᵐ (x : Vec d), IsEllipticMatrix 1 Θ (a x)) : (∀ (σ : Fin d → Fin N), |blockVecDot P (blockMatVecMul (coarseBlockMatrix (cubeSet (originCube d m)) (corridorField ℓ (gridPhase ℓ N σ) a)) P) - blockVecDot P (blockMatVecMul (coarseBlockMatrix (cubeSet (originCube d m)) a) P)| ≤ 2 * (Θ * vecNormSq P.1 + vecNormSq P.2)) ∧ ∑ σ : Fin d → Fin N, |blockVecDot P (blockMatVecMul (coarseBlockMatrix (cubeSet (originCube d m)) (corridorField ℓ (gridPhase ℓ N σ) a)) P) - blockVecDot P (blockMatVecMul (coarseBlockMatrix (cubeSet (originCube d m)) a) P)| ^ 2 ≤ 576 * ↑d * Θ * ↑N ^ d * (Θ * vecNormSq P.1 + vecNormSq P.2) ^ 2 / ℓ

The finite-grid summed square deviation, bounded pointwise-in-a by 576 d Θ N^d (M²)² / ℓ, together with the per-phase bound ≤ 2M², for any measurable a.e.-(1,Θ)-elliptic realization.

theorem HCPolySupport.exists_gridPhase_meanSq_le_uniform {d : ℕ} [NeZero d] : ∃ (Cd : ℝ), 0 ≤ Cd ∧ ∀ {Θ : ℝ}, 1 ≤ Θ → ∀ {L : Book.Ch04.RestrictionCoeffLaw d}, Book.Ch04.RestrictionLawCarrier L → ThetaEllipticLaw Θ L → ∀ {m : ℤ} {ℓ : ℝ}, 4 ≤ ℓ → ∀ {N : ℕ}, ℓ ≤ ↑N → ∀ (P : BlockVec d), ∃ σ ∈ Finset.univ, ∫ (a : RegCoeffField d), |blockVecDot P (blockMatVecMul (coarseBlockMatrix (cubeSet (originCube d m)) (corridorField ℓ (gridPhase ℓ N σ) a.toFun)) P) - blockVecDot P (blockMatVecMul (coarseBlockMatrix (cubeSet (originCube d m)) a.toFun) P)| ^ 2 ∂L ≤ Cd * Θ * ℓ⁻¹ * (Θ * vecNormSq P.1 + vecNormSq P.2) ^ 2

Uniform-constant grid-phase averaging. The constant Cd = 576·d is independent of Θ, L, m, ℓ, N, P.

theorem HCPolySupport.exists_gridPhase_meanSq_le {d : ℕ} [NeZero d] {Θ : ℝ} (hΘ : 1 ≤ Θ) {L : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier L) (hell : ThetaEllipticLaw Θ L) {m : ℤ} {ℓ : ℝ} (hℓ : 4 ≤ ℓ) {N : ℕ} (hN : ℓ ≤ ↑N) (P : BlockVec d) : ∃ (Cd : ℝ), 0 ≤ Cd ∧ ∃ σ ∈ Finset.univ, ∫ (a : RegCoeffField d), |blockVecDot P (blockMatVecMul (coarseBlockMatrix (cubeSet (originCube d m)) (corridorField ℓ (gridPhase ℓ N σ) a.toFun)) P) - blockVecDot P (blockMatVecMul (coarseBlockMatrix (cubeSet (originCube d m)) a.toFun) P)| ^ 2 ∂L ≤ Cd * Θ * ℓ⁻¹ * (Θ * vecNormSq P.1 + vecNormSq P.2) ^ 2

M3 (averaging + choice). Under a RestrictionLawCarrier Θ-elliptic law and 4 ≤ ℓ ≤ N, there is a deterministic grid phase σ_* whose mean-square coarse deviation is O(ℓ⁻¹), with an explicit dimensional constant Cd = 576 d. The per-realization summed bound gridPhase_summed_sq_le_of_realization is averaged over the probability law and a below-average phase is selected.