High-contrast homogenization: Provider.Quenched.SmallContrastSubdivisionSupply

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

The subdivision supply at the adapted-mean normalizer

The hypothesis hsubdiv normalizes both lqSchattenSize terms by adaptedMean P q p'. AlignedSubdivisionVariance.exists_alignedSubdivisionVarianceConstant quantifies over the normalizer, so it can be instantiated at this block. The result below has exactly the hsubdiv shape used by entry_lagged_variance_supply_of_block_split, entry_supply_slot_bound_of_block_split and entry_supply_deep_slot_bound_of_block_split, with no reshaping.

The one extra frozen premise the producer needs beyond the supplies' own is IsUnitRangeLaw P, which the subdivision constant carries.

theorem HCPolySupport.HighContrast.Quenched.exists_repaired_subdivision_supply (d : ℕ) (hd : 2 ≤ d) : ∃ (Csub : ℝ), 0 < Csub ∧ ∀ (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 → ∀ (lAl : ℤ) (mAl : Mat d), IsRoundedGrid lAl (roundedGrid lAl mAl) → ∀ (j' p' : ℤ), lAl ≤ j' → j' ≤ p' → ∃ (Z : Finset (Fin d → ℤ)), ↑Z = {w : Fin d → ℤ | adaptedCellCenter (roundedGrid lAl mAl) j' w ∈ adaptedCell (roundedGrid lAl mAl) 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 (roundedGrid lAl mAl) j' w) a))) (adaptedMean P (roundedGrid lAl mAl) j')) (adaptedMean P (roundedGrid lAl mAl) p') ≤ ENNReal.ofReal (Csub * ↑Z.card ^ (-2⁻¹)) * lqSchattenSize P 2 (fun (a : CoeffSpace d) => blockSub (coarseBlock (adaptedCell (roundedGrid lAl mAl) j') a) (adaptedMean P (roundedGrid lAl mAl) j')) (adaptedMean P (roundedGrid lAl mAl) p')

A single dimensional subdivision constant serves every law, grid, and scale pair at the adapted-mean normalizer.