High-contrast homogenization: Provider.Quenched.SmallContrastSkewLaw

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

The law-side skew-recentering invariance

The recentering of Section 2.5 of HC is a transformation of the coefficient field, hence of the law: the recentered law is the pushforward of P under a ↦ a - g, i.e. under CoeffSpace.subSkew. The paper uses it to assume, without loss of generality, that a homogenized skew vanishes, on the ground that the assumptions and the conclusions of the small-contrast argument are invariant.

This file proves that invariance for the objects the small-contrast argument actually carries:

• annealedBlock (and hence adaptedMean) is covariant: it acquires the shear congruence skewBlockCongr g;
• IsStationaryLaw is invariant;
• adaptedHattedContrast and annealedContrast are invariant, because both contrasts are skew-blind (SmallContrastSkewInvariants).

The recentering map is a measurable involution up to sign, so all integral transports go through integral_map_equiv, which needs no measurability side condition on the integrand.

The recentering map is a measurable equivalence

theorem HCPolySupport.HighContrast.Quenched.subSkew_neg_subSkew {d : ℕ} (a : CoeffSpace d) {g : Mat d} (hg : IsSkewMat g) : (a.subSkew g hg).subSkew (-g) ⋯ = a

Recentering by -g undoes recentering by g.

noncomputable def HCPolySupport.HighContrast.Quenched.subSkewEquiv {d : ℕ} {g : Mat d} (hg : IsSkewMat g) : CoeffSpace d ≃ᵐ CoeffSpace d

The recentering map as a measurable equivalence of the coefficient space.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HCPolySupport.HighContrast.Quenched.subSkewEquiv_apply {d : ℕ} {g : Mat d} (hg : IsSkewMat g) (a : CoeffSpace d) : (subSkewEquiv hg) a = a.subSkew g hg

noncomputable def HCPolySupport.HighContrast.Quenched.recenteredLaw {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) {g : Mat d} (hg : IsSkewMat g) : MeasureTheory.Measure (CoeffSpace d)

The recentered law: the pushforward of P under the recentering map.

Equations

• HCPolySupport.HighContrast.Quenched.recenteredLaw P hg = MeasureTheory.Measure.map (fun (a : HCPolySupport.HighContrast.CoeffSpace d) => a.subSkew g hg) P

theorem HCPolySupport.HighContrast.Quenched.recenteredLaw_eq_map {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) {g : Mat d} (hg : IsSkewMat g) : recenteredLaw P hg = MeasureTheory.Measure.map (⇑(subSkewEquiv hg)) P

instance HCPolySupport.HighContrast.Quenched.isProbabilityMeasure_recenteredLaw {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] {g : Mat d} (hg : IsSkewMat g) : MeasureTheory.IsProbabilityMeasure (recenteredLaw P hg)

Stationarity is invariant

theorem HCPolySupport.HighContrast.Quenched.translateCoeff_subSkew {d : ℕ} (z : Fin d → ℤ) (a : CoeffSpace d) {g : Mat d} (hg : IsSkewMat g) : translateCoeff z (a.subSkew g hg) = (translateCoeff z a).subSkew g hg

Recentering commutes with the integer translations.

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

Stationarity is invariant under the recentering.

The annealed block is shear-covariant

theorem HCPolySupport.HighContrast.Quenched.annealedBlock_recenteredLaw {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} (U : Book.Ch02.Domain d) (hint : HasIntegrableCoarseBlock P U.carrier) {g : Mat d} (hg : IsSkewMat g) : annealedBlock (recenteredLaw P hg) U.carrier = Response.skewBlockCongr g (annealedBlock P U.carrier)

The annealed block of the recentered law is the shear congruence of the annealed block: this is the law-level form of HC (2.65).

theorem HCPolySupport.HighContrast.Quenched.adaptedMean_recenteredLaw {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {q : Mat d} (hq : Matrix.PosDef q) (k : ℤ) (hint : HasFiniteAdaptedMean P q k) {g : Mat d} (hg : IsSkewMat g) : adaptedMean (recenteredLaw P hg) q k = Response.skewBlockCongr g (adaptedMean P q k)

The adapted mean of the recentered law.

Both contrasts are invariant

theorem HCPolySupport.HighContrast.Quenched.annealedContrast_recenteredLaw {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} (m : ℤ) (hint : HasFiniteAdaptedMean P 1 m) (hpd : Book.Ch02.BlockPosDef (annealedBlock P (centeredCube d m))) {g : Mat d} (hg : IsSkewMat g) : annealedContrast (recenteredLaw P hg) m = annealedContrast P m

The Euclidean annealed contrast is invariant under the recentering.