High-contrast homogenization: Provider.Recurrence.FiniteRangeAveraging

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

l.fixed.geometry.matrix.averaging

The finite-range matrix averaging estimate: the mixed norm of the centred average of the responses of a family of distinct aligned adapted cells is smaller than the mixed norm of a single response by the square root of the number of cells.

The proof is the printed one. The scalarization display of l.fixed.geometry.matrix.averaging reduces the matrix estimate to the 4d² scalar estimates carried by the colour split and the independent-sum inequality, and reassembling them costs the factor 2d the printed proof records. The average contributes the weight M^{-1}, which together with the square root M^{1/2} produced by the independent sums is the gain M^{-1/2}.

The estimate is stated in the ℝ≥0∞ carrier the fixed-grid moments are written in, so an infinite single-cell moment makes the bound vacuous rather than false. The equal-weight form recorded here is the one the averaging step of p.fixed.geometry.parent.child.recurrence consumes; its last form replaces the single-cell moment by the centred moment v_j^q at the origin, the two being equal because each aligned cell is an integer translate of the cell at the origin.

Reassembling the 4d² entries

Symmetry and measurability of the centred aligned average

theorem HCPolySupport.HighContrast.Recurrence.isSymmetricBlockMat_alignedAverage {d : ℕ} {q : Mat d} {j : ℤ} (Z : Finset (Fin d → ℤ)) (a : CoeffSpace d) : IsSymmetricBlockMat (ofFullBlockMat ((↑Z.card)⁻¹ • ∑ w ∈ Z, toFullBlockMat (coarseBlock (adaptedCellAt q j w) a)))

The aligned average of the coarse responses is symmetric.

The estimate at an explicit constant

theorem HCPolySupport.HighContrast.Recurrence.lqSchattenSize_alignedAverage_le_of_lqNorm_le {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (hPs : IsStationaryLaw P) (hP : IsUnitRangeLaw P) {Q : ℝ} (hQ : 2 ≤ Q) {l : ℤ} {q : Mat d} (hq : IsRoundedGrid l q) {j : ℤ} (hj : l ≤ j) (hint : HasFiniteAdaptedMean P q j) (F : BlockMat d) {v : ENNReal} (hv : v ≠ ⊤) {Z : Finset (Fin d → ℤ)} (hZ : Z.Nonempty) (hbd : ∀ w ∈ Z, ∀ (α β : BlockCoord d), (lqNorm P Q fun (a : CoeffSpace d) => toFullBlockMat (normalizedBlock (blockSub (coarseBlock (adaptedCellAt q j w) a) (adaptedMean P q j)) F) α β) ≤ v) : lqSchattenSize P Q (fun (a : CoeffSpace d) => blockSub (ofFullBlockMat ((↑Z.card)⁻¹ • ∑ w ∈ Z, toFullBlockMat (coarseBlock (adaptedCellAt q j w) a))) (adaptedMean P q j)) F ≤ ENNReal.ofReal (2 * ↑d) * ENNReal.ofReal ((2 * Q + 4 * IndependentSums.rosenthalBennettIntegralConst * √Q) * (√(3 ^ d) * ↑Z.card ^ (-2⁻¹) * v.toReal))

l.fixed.geometry.matrix.averaging, equal weights, entrywise binder. The mixed norm of the centred aligned average is at most an explicit constant times M^{-1/2} times the uniform bound on the L^Q norms of the entries of the normalized centred responses.

The printed display

theorem HCPolySupport.HighContrast.Recurrence.finite_range_matrix_averaging (d : ℕ) (hd : 0 < d) {Q : ℝ} (hQ : 2 ≤ Q) : ∃ (C : ℝ), 0 < C ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → ∀ (l : ℤ) (q : Mat d), IsRoundedGrid l q → ∀ (j : ℤ), l ≤ j → HasFiniteAdaptedMean P q j → ∀ (F : BlockMat d) (v : ENNReal) (Z : Finset (Fin d → ℤ)), Z.Nonempty → (∀ w ∈ Z, lqSchattenSize P Q (fun (a : CoeffSpace d) => blockSub (coarseBlock (adaptedCellAt q j w) a) (adaptedMean P q j)) F ≤ v) → lqSchattenSize P Q (fun (a : CoeffSpace d) => blockSub (ofFullBlockMat ((↑Z.card)⁻¹ • ∑ w ∈ Z, toFullBlockMat (coarseBlock (adaptedCellAt q j w) a))) (adaptedMean P q j)) F ≤ ENNReal.ofReal (C * ↑Z.card ^ (-2⁻¹)) * v

l.fixed.geometry.matrix.averaging, equal weights: there is a constant C(d, Q) such that the mixed norm of the centred average of the responses over M distinct aligned adapted cells is at most C(d, Q) M^{-1/2} times a uniform bound on the mixed norms of the centred single-cell responses.

The form the fixed-grid recurrence consumes

theorem HCPolySupport.HighContrast.Recurrence.lqNorm_normalizedBlock_adaptedCellAt_eq {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} (hPs : IsStationaryLaw P) {Q : ℝ} {l : ℤ} {q : Mat d} (hq : IsRoundedGrid l q) {j : ℤ} (hj : l ≤ j) (E F : BlockMat d) (w : Fin d → ℤ) (α β : BlockCoord d) : (lqNorm P Q fun (a : CoeffSpace d) => toFullBlockMat (normalizedBlock (blockSub (coarseBlock (adaptedCellAt q j w) a) E) F) α β) = lqNorm P Q fun (a : CoeffSpace d) => toFullBlockMat (normalizedBlock (blockSub (coarseBlock (adaptedCell q j) a) E) F) α β

The entries of the normalized centred response have the same L^Q norm at every aligned adapted cell. Each aligned cell is an integer translate of the cell at the origin, and under stationarity of the coefficient law the translation preserves the law.

theorem HCPolySupport.HighContrast.Recurrence.lqNorm_normalizedBlock_adaptedCellAt_le_centeredMoment {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} (hPs : IsStationaryLaw P) {Q : ℝ} (hQ : 0 < Q) {l : ℤ} {q : Mat d} (hq : IsRoundedGrid l q) {j : ℤ} (hj : l ≤ j) (w : Fin d → ℤ) (α β : BlockCoord d) : (lqNorm P Q fun (a : CoeffSpace d) => toFullBlockMat (normalizedBlock (blockSub (coarseBlock (adaptedCellAt q j w) a) (adaptedMean P q j)) (adaptedMean P q j)) α β) ≤ centeredMoment P Q q j

The entries of the normalized centred response of an aligned adapted cell are bounded in L^Q by the centred moment v_j^q at the origin.

theorem HCPolySupport.HighContrast.Recurrence.lqSchattenSize_alignedAverage_le_centeredMoment {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (hPs : IsStationaryLaw P) (hP : IsUnitRangeLaw P) {Q : ℝ} (hQ : 2 ≤ Q) {l : ℤ} {q : Mat d} (hq : IsRoundedGrid l q) {j : ℤ} (hj : l ≤ j) (hint : HasFiniteAdaptedMean P q j) (hfin : centeredMoment P Q q j ≠ ⊤) {Z : Finset (Fin d → ℤ)} (hZ : Z.Nonempty) : lqSchattenSize P Q (fun (a : CoeffSpace d) => blockSub (ofFullBlockMat ((↑Z.card)⁻¹ • ∑ w ∈ Z, toFullBlockMat (coarseBlock (adaptedCellAt q j w) a))) (adaptedMean P q j)) (adaptedMean P q j) ≤ ENNReal.ofReal (2 * ↑d * ((2 * Q + 4 * IndependentSums.rosenthalBennettIntegralConst * √Q) * √(3 ^ d)) * ↑Z.card ^ (-2⁻¹)) * centeredMoment P Q q j

The averaging step of p.fixed.geometry.parent.child.recurrence. The mixed norm of the centred average of the responses over the M aligned scale-j cells is at most C(d, Q) M^{-1/2} times the centred moment v_j^q.