High-contrast homogenization: Provider.Quenched.AlignedSubdivisionVariance

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

Finite-range variance on an aligned adapted subdivision

For a unit-range law, the centred responses of aligned adapted cells split into finitely many independent colour classes. Applied to the exact subdivision of one adapted parent, this gives the square-root cardinality gain without passing through a Euclidean grouping of cell centres.

The normalizing block is arbitrary. In particular, the result can be read in the fixed reference normalization used by the small-contrast response estimate. The sole integrability input needed by the averaging theorem, finiteness of the adapted mean, follows from coarse ellipticity. The single-cell mixed norm is allowed to be infinite; that branch is handled in the extended-nonnegative carrier rather than introduced as a premise.

theorem HCPolySupport.HighContrast.Quenched.exists_alignedSubdivisionVarianceConstant (d : ℕ) (hd : 2 ≤ d) : ∃ (C : ℝ), 0 < C ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (g : ℝ) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P g E Ψ K S → ∀ (l : ℤ) (q : Mat d), IsRoundedGrid l q → ∀ (j p : ℤ), l ≤ j → j ≤ p → ∀ (F : BlockMat d), ∃ (Z : Finset (Fin d → ℤ)), ↑Z = {w : Fin d → ℤ | adaptedCellCenter q j w ∈ adaptedCell q p} ∧ Z.card = 3 ^ (d * (p - j).toNat) ∧ Z.Nonempty ∧ lqSchattenSize P 2 (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⁻¹)) * lqSchattenSize P 2 (fun (a : CoeffSpace d) => blockSub (coarseBlock (adaptedCell q j) a) (adaptedMean P q j)) F

There is a dimension-only constant for the L²(S₂) fluctuation of the exact aligned subdivision. The constant is selected before the law, coarse-ellipticity data, grid, scales, and normalizer.

The right side is the single-cell fluctuation in the same arbitrary normalization F. Thus F may be the fixed reference block used in the small-contrast response estimate.