High-contrast homogenization: Provider.Recurrence.AveragedEntries

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

The entries of the centred aligned average

The averaging step of p.fixed.geometry.parent.child.recurrence applies l.fixed.geometry.matrix.averaging to the average G = M^{-1}Σ_z 𝐀_j(z) of the responses of the aligned scale-j children of the parent cell. This file carries that average down to the scalar level.

Two things happen. First, normalization and centring are a fixed real-linear map of the entries of a doubled block, so an entry of the normalized centred average is the average of the entries of the normalized centred responses. Second, the family of children splits into at most 3^d colour classes, each of which carries the independent-sum estimate; summing the classes and applying Cauchy–Schwarz to the at most 3^d resulting terms leaves a single square root of the total cardinality, which is the M^{-1/2} gain of the printed proof once the average is normalized.

Linearity of the normalized centred entry

theorem HCPolySupport.HighContrast.Recurrence.toFullBlockMat_normalizedBlock_blockSub_average_apply {d : ℕ} {ι : Type u_1} {Z : Finset ι} (hZ : Z.Nonempty) (A : ι → BlockMat d) (E F : BlockMat d) (α β : BlockCoord d) : toFullBlockMat (normalizedBlock (blockSub (ofFullBlockMat ((↑Z.card)⁻¹ • ∑ w ∈ Z, toFullBlockMat (A w))) E) F) α β = (↑Z.card)⁻¹ * ∑ w ∈ Z, toFullBlockMat (normalizedBlock (blockSub (A w) E) F) α β

An entry of the normalized centred average is the average of the entries of the normalized centred summands. Normalization and centring by deterministic blocks are a fixed real-linear map of the entries, and the centring survives the average because the weights sum to one.

Summing the colour classes

theorem HCPolySupport.HighContrast.Recurrence.lqNorm_sum_aligned_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 → ℤ)) (α β : 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, toFullBlockMat (normalizedBlock (blockSub (coarseBlock (adaptedCellAt q j w) a) (adaptedMean P q j)) F) α β) ≤ ENNReal.ofReal ((2 * Q + 4 * IndependentSums.rosenthalBennettIntegralConst * √Q) * (√(3 ^ d) * √↑Z.card * v.toReal))

The scalar estimate of l.fixed.geometry.matrix.averaging on a whole family of aligned adapted cells. The family splits into at most 3^d colour classes, the independent-sum estimate applies to each, and Cauchy–Schwarz on the at most 3^d resulting square roots leaves the square root of the total cardinality.