High-contrast homogenization: Provider.Quenched.UnitRangeCentring #

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

The centring block of the inner cells #

The concentration estimate centres each observable at its own mean, so the renormalization argument has to identify the block of those means with the annealed block at the inner generation. Two facts do that.

The mean commutes with the normalization, because the normalization is a fixed linear map of the entries. And the annealed block of an aligned cell is the annealed block of the centred cell of the same generation, because the law is invariant under integer translations and the coarse block is covariant under them. Together they replace the mean of every inner cell by one reference block.

The entry algebra of the difference and the scaling #

source

theorem HCPolySupport.HighContrast.Quenched.blockMatEntry_blockSub {d : ℕ} (A B : BlockMat d) (α β : BlockCoord d) :

blockMatEntry (blockSub A B) α β = blockMatEntry A α β - blockMatEntry B α β

The mean commutes with the normalization #

source

theorem HCPolySupport.HighContrast.Quenched.meanBlock_normalizedBlock {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {M : CoeffSpace d → BlockMat d} (E : BlockMat d) (hM : HasIntegrableBlock P M) :

(meanBlock P fun (a : CoeffSpace d) => normalizedBlock (M a) E) = normalizedBlock (meanBlock P M) E

The mean commutes with the normalization. The normalization is a fixed linear map of the entries, so it passes through the entrywise mean.

The annealed block of an aligned cell #

source

theorem HCPolySupport.HighContrast.Quenched.standardCell_eq_translateSet_centeredCube {d : ℕ} {l : ℤ} (hl : 0 ≤ l) (u : Fin d → ℤ) :

standardCell d l u = translateSet (Source.AKL.intTranslation (parentShift l u)) (centeredCube d l)

An aligned cell is the integer translate of the centred cell of the same generation.

source

theorem HCPolySupport.HighContrast.Quenched.annealedBlock_standardCell_eq_centeredCube {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} (hstat : IsStationaryLaw P) {l : ℤ} (hl : 0 ≤ l) (u : Fin d → ℤ) (hmeas : HasMeasurableCoarseBlock P (centeredCube d l)) :

annealedBlock P (standardCell d l u) = annealedBlock P (centeredCube d l)

The annealed block of an aligned cell is the annealed block of the centred cell. Integer stationarity of the law and the covariance of the coarse block under integer translations.