High-contrast homogenization: Provider.Quenched.SmallContrastSkewUnitRange

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

Unit range survives the recentering

The recentering of the reference block is a transformation of the coefficient field — subtraction of a constant skew — and the small-contrast argument runs at the recentered law. Stationarity, the ellipticity datum and both contrasts are already known to travel with it; the remaining frozen premise is unit range.

It travels for the same reason the triadic rebasing's does, and more simply: the recentering moves no point of space, so each local sigma-field is carried into itself. A generating statistic of the shifted sample is the statistic of the sample translated by a constant, and the constant depends only on the skew and the test function, so the pullback of a generator is a generator with the same test support.

theorem HCPolySupport.HighContrast.coeffSigma_comap_subSkew_le {d : ℕ} (U : Set (Vec d)) (g : Mat d) (hg : IsSkewMat g) : MeasurableSpace.comap (fun (a : CoeffSpace d) => a.subSkew g hg) (coeffSigma d U) ≤ coeffSigma d U

The recentering is local. Each local sigma-field is carried into itself, because a generating statistic of the shifted sample is the statistic of the sample translated by a constant with the same test support.

theorem HCPolySupport.HighContrast.isUnitRangeLaw_recenteredLaw {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} (hP : IsUnitRangeLaw P) {g : Mat d} (hg : IsSkewMat g) : IsUnitRangeLaw (Quenched.recenteredLaw P hg)

Unit range is invariant under the recentering.