High-contrast homogenization: Provider.Quenched.SmallContrastSkewDagger

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

Coarse ellipticity under the constant-skew recentering

The last clause of the law-side API for the recentering of Section 2.5 of HC: the frozen dagger assumption e.coarse.ellipticity survives the recentering, with the reference block replaced by its shear congruence and the source field composed with the inverse recentering.

The gauge, the growth witness and the exponent are untouched — the recentering does not move the source at all, it only relabels which sample carries it. The cell bound transports because the shear congruence preserves the doubled Loewner order (Response.skewBlockCongr_loewner_iff) and commutes with scalar dilation (Response.blockScale_skewBlockCongr).

def HCPolySupport.HighContrast.Quenched.standardCellDomain (d : ℕ) (k : ℤ) (w : Fin d → ℤ) : Book.Ch02.Domain d

The standard aligned cube as a Chapter-2 domain.

Equations

• HCPolySupport.HighContrast.Quenched.standardCellDomain d k w = { carrier := HCPolySupport.HighContrast.standardCell d k w, isDomain := ⋯, nonempty := ⋯ }

theorem HCPolySupport.HighContrast.Quenched.coarseBlock_standardCell_subSkew {d : ℕ} (k : ℤ) (w : Fin d → ℤ) (a : CoeffSpace d) {g : Mat d} (hg : IsSkewMat g) : coarseBlock (standardCell d k w) (a.subSkew g hg) = Response.skewBlockCongr g (coarseBlock (standardCell d k w) a)

Constant-skew covariance of the coarse response on a standard cell.

noncomputable def HCPolySupport.HighContrast.Quenched.recenteredSource {d : ℕ} (S : CoeffSpace d → ℝ) {g : Mat d} (hg : IsSkewMat g) : CoeffSpace d → ℝ

The recentered source field: the original source read at the un-recentered sample.

Equations

• HCPolySupport.HighContrast.Quenched.recenteredSource S hg a = S (a.subSkew (-g) ⋯)

theorem HCPolySupport.HighContrast.Quenched.recenteredSource_subSkew {d : ℕ} (S : CoeffSpace d → ℝ) {g : Mat d} (hg : IsSkewMat g) (a : CoeffSpace d) : recenteredSource S hg (a.subSkew g hg) = S a

theorem HCPolySupport.HighContrast.Quenched.coarseEllipticityDagger_recenteredLaw {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {gexp : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P gexp E Ψ K S) {g : Mat d} (hg : IsSkewMat g) : CoarseEllipticityDagger (recenteredLaw P hg) gexp (Response.skewBlockCongr g E) Ψ K (recenteredSource S hg)

Coarse ellipticity survives the recentering. The reference block picks up the shear congruence; the gauge, growth witness and exponent are unchanged; the source field is composed with the inverse recentering.