High-contrast homogenization: Entry.MatrixAveraging

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Finite-range matrix averaging

This module proves the finite-range matrix averaging statement of HCPoly/Entry/Statements/MatrixAveraging.lean. It serves the labelled result l.fixed.geometry.matrix.averaging: the even-moment matrix estimate, residue-class independence, stationary transport, and convex recombination from ordinary support.

We choose Csrc = 1 before the law and geometry. This preserves the exact standing threshold premise; it does not assert the stochastic source estimate with constant one. This averaging proof needs only moment finiteness, which the standing law supplies at every bounded cell. The unused standing binders are underscore-renamed without changing their type, kind, or position.

theorem HCPolySupport.HighContrast.Entry.fixed_geometry_matrix_averaging (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (_hγ : γ ∈ Set.Ico 0 1) : ∃ (Csrc : ℝ), 0 < Csrc ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P γ E Ψ K S → ∀ (N : ℕ), 2 ≤ N → Even N → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ⌈Csrc * Real.logb 3 (2 * K)⌉ ≤ ↑jStar → ∀ (m : Mat d), Matrix.PosDef m → ∀ (j : ℤ), ↑jStar ≤ j → ∀ (Z : Finset (Vec d)), Z.Nonempty → ↑Z ⊆ adaptedLatticeAtScale (Geometry.explicitRoundedGrid jStar m) j → ∀ (R : BlockMat d), IsSymmetricBlockMat R → Book.Ch02.BlockPosDef R → (lqSchattenNorm P ↑N fun (a : CoeffSpace d) => ofFullBlockMat ((↑Z.card)⁻¹ • ∑ z ∈ Z, toFullBlockMat (normalizedBlock (blockSub (coarseBlock (adaptedCellTranslate (Geometry.explicitRoundedGrid jStar m) j z) a) (adaptedMean P (Geometry.explicitRoundedGrid jStar m) j)) R))) ≤ ↑N * 3 ^ (↑d / 2) / ↑Z.card ^ (1 / 2) * lqSchattenNorm P ↑N fun (a : CoeffSpace d) => normalizedBlock (blockSub (coarseBlock (adaptedCell (Geometry.explicitRoundedGrid jStar m) j) a) (adaptedMean P (Geometry.explicitRoundedGrid jStar m) j)) R

The exact finite-range averaging statement; source near l.fixed.geometry.matrix.averaging.