High-contrast homogenization: Provider.Recurrence.ColourClassAveraging

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

The independent-sum estimate on one colour class

l.fixed.geometry.matrix.averaging proves a matrix estimate by proving 4d² scalar ones, and each scalar one is a moment estimate for a sum of independent centred random variables: the entries of the normalized centred responses X_i = R^{-1/2}(𝐀(U_i) - 𝐄[𝐀(U_i)])R^{-1/2} over the cells of one colour class.

This file produces that scalar estimate. Its analytic inputs are the moment binders of the independent-sum inequality, and each is a consequence of data the fixed-grid estimates already carry.

Integrability of the Q-th powers. An entry of a normalized centred block is dominated pointwise by the Schatten size of that block, so a finite L^Q norm of the entry puts it in L^Q, and the Q-th power of its absolute value is then integrable.

Centring. The entries of the normalized centred response integrate to zero. This is stationarity of the coefficient law read through the translation invariance of the coarse block: the annealed block of an aligned adapted cell is the adapted mean at that scale, which is the block the response is centred by.

The uniform bound. The Q-th root of the Q-th absolute moment of an entry is the real form of its L^Q norm, so a uniform bound on those norms is exactly the uniform binder the inequality asks for.

With the three binders the uniform moment inequality for independent sums applies to the colour class, and the square root of the cardinality of the class — the fluctuation gain of the printed proof, before the average is normalized — appears in the bound.

Symmetry and the entrywise comparison

theorem HCPolySupport.HighContrast.Recurrence.isSymmetricBlockMat_coarseBlock_sub {d : ℕ} {U : Set (Vec d)} (a : CoeffSpace d) {E : BlockMat d} (hE : IsSymmetricBlockMat E) : IsSymmetricBlockMat (blockSub (coarseBlock U a) E)

The centred coarse response of a cell is symmetric as soon as the centring block is.

theorem HCPolySupport.HighContrast.Recurrence.lqNorm_normalizedBlock_le_lqSchattenSize {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) {Q : ℝ} (hQ : 0 < Q) {A : CoeffSpace d → BlockMat d} (hA : ∀ (a : CoeffSpace d), IsSymmetricBlockMat (A a)) (F : BlockMat d) (α β : BlockCoord d) (hmeas : MeasureTheory.AEStronglyMeasurable (fun (a : CoeffSpace d) => toFullBlockMat (normalizedBlock (A a) F) α β) P) : (lqNorm P Q fun (a : CoeffSpace d) => toFullBlockMat (normalizedBlock (A a) F) α β) ≤ lqSchattenSize P Q A F

An entry of a normalized block has L^Q norm at most the mixed norm of the block. This is the entrywise spectral comparison of l.fixed.geometry.matrix.averaging after the L^Q norm is taken.

The integrability binder

theorem HCPolySupport.HighContrast.Recurrence.memLp_toFullBlockMat_normalizedBlock_blockSub {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {Q : ℝ} {U : Set (Vec d)} (E F : BlockMat d) (α β : BlockCoord d) (hfin : (lqNorm P Q fun (a : CoeffSpace d) => toFullBlockMat (normalizedBlock (blockSub (coarseBlock U a) E) F) α β) ≠ ⊤) : MeasureTheory.MemLp (fun (a : CoeffSpace d) => toFullBlockMat (normalizedBlock (blockSub (coarseBlock U a) E) F) α β) (ENNReal.ofReal Q) P

An entry of the normalized centred response lies in L^Q as soon as its L^Q norm is finite.

theorem HCPolySupport.HighContrast.Recurrence.integrable_abs_rpow_of_memLp {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {Q : ℝ} (hQ : 0 < Q) {X : CoeffSpace d → ℝ} (hX : MeasureTheory.MemLp X (ENNReal.ofReal Q) P) : MeasureTheory.Integrable (fun (a : CoeffSpace d) => |X a| ^ Q) P

The Q-th power of the absolute value of an L^Q variable is integrable. This is the integrability binder of the independent-sum inequality.

The uniform binder

theorem HCPolySupport.HighContrast.Recurrence.rpow_inv_integral_abs_rpow_le_toReal {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {Q : ℝ} (hQ : 0 < Q) {X : CoeffSpace d → ℝ} (hX : MeasureTheory.MemLp X (ENNReal.ofReal Q) P) {v : ENNReal} (hv : v ≠ ⊤) (hle : lqNorm P Q X ≤ v) : (∫ (a : CoeffSpace d), |X a| ^ Q ∂P) ^ Q⁻¹ ≤ v.toReal

The uniform binder of the independent-sum inequality. The Q-th root of the Q-th absolute moment is the real form of the L^Q norm, so a bound on the latter is a bound on the former.

The centring binder

theorem HCPolySupport.HighContrast.Recurrence.integral_toFullBlockMat_normalizedBlock_adaptedCellAt_eq_zero {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (hP : IsStationaryLaw P) {l : ℤ} {q : Mat d} (hq : IsRoundedGrid l q) {j : ℤ} (hj : l ≤ j) (hint : HasFiniteAdaptedMean P q j) (F : BlockMat d) (w : Fin d → ℤ) (α β : BlockCoord d) : ∫ (a : CoeffSpace d), toFullBlockMat (normalizedBlock (blockSub (coarseBlock (adaptedCellAt q j w) a) (adaptedMean P q j)) F) α β ∂P = 0

The entries of the normalized centred response of an aligned adapted cell integrate to zero. The annealed block of an aligned cell is the adapted mean at that scale, by the translation invariance of the coarse block under stationarity of the coefficient law, and that mean is the block the response is centred by.

The independent-sum estimate

theorem HCPolySupport.HighContrast.Recurrence.lqNorm_finsetSum_le_of_iIndepFun {d : ℕ} {ι : Type u_1} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {Q : ℝ} (hQ : 2 ≤ Q) {v : ENNReal} (hv : v ≠ ⊤) (s : Finset ι) {Y : ι → CoeffSpace d → ℝ} (hindep : ProbabilityTheory.iIndepFun (fun (u : ↥s) => Y ↑u) P) (hmeas : ∀ (i : ι), Measurable (Y i)) (hmemLp : ∀ i ∈ s, MeasureTheory.MemLp (Y i) (ENNReal.ofReal Q) P) (hmean : ∀ i ∈ s, ∫ (a : CoeffSpace d), Y i a ∂P = 0) (hbd : ∀ i ∈ s, lqNorm P Q (Y i) ≤ v) : (lqNorm P Q fun (a : CoeffSpace d) => ∑ i ∈ s, Y i a) ≤ ENNReal.ofReal ((2 * Q + 4 * IndependentSums.rosenthalBennettIntegralConst * √Q) * (√↑s.card * v.toReal))

The scalar moment estimate of l.fixed.geometry.matrix.averaging, in the ℝ≥0∞ form the mixed norm is written in: a finite sum of independent centred real variables with L^Q norms at most v has L^Q norm at most a constant depending on Q times the square root of the number of summands times v. The square root is the fluctuation gain of the printed proof.

One colour class of a family of aligned adapted cells

theorem HCPolySupport.HighContrast.Recurrence.lqNorm_sum_colourClass_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 → ℤ)) (c : Fin d → ZMod 3) (α β : BlockCoord d) (hbd : ∀ w ∈ Z, (lqNorm P Q fun (a : CoeffSpace d) => toFullBlockMat (normalizedBlock (blockSub (coarseBlock (adaptedCellAt q j w) a) (adaptedMean P q j)) F) α β) ≤ v) : (lqNorm P Q fun (a : CoeffSpace d) => ∑ w ∈ Z with (fun (i : Fin d) => ↑(w i)) = c, toFullBlockMat (normalizedBlock (blockSub (coarseBlock (adaptedCellAt q j w) a) (adaptedMean P q j)) F) α β) ≤ ENNReal.ofReal ((2 * Q + 4 * IndependentSums.rosenthalBennettIntegralConst * √Q) * (√↑{u ∈ Z | (fun (i : Fin d) => ↑(u i)) = c}.card * v.toReal))

The scalar moment estimate on one colour class of aligned adapted cells. The entries of the normalized centred responses of a same-colour family of distinct aligned cells are independent and centred, so the uniform moment inequality for independent sums applies, and the square root of the cardinality of the class is the fluctuation gain it produces.