High-contrast homogenization: Provider.Response.ConstantSkewCoefficient

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

Constant-skew recentering of coefficient samples

Subtracting a constant skew matrix leaves the coercive quadratic form unchanged. Its action on vectors remains bounded by a finite-dimensional matrix norm, so the recentered field is again a member of the qualitative coefficient space.

noncomputable def HCPolySupport.HighContrast.Response.skewShiftUpper {d : ℕ} (lam Lam : ℝ) (g : Mat d) : ℝ

An upper ellipticity constant after subtracting a constant skew matrix.

Equations

• HCPolySupport.HighContrast.Response.skewShiftUpper lam Lam g = 2 * (Lam ^ 2 + HCPolySupport.Book.Ch02.matrixFrobeniusNormSq g) / lam

theorem HCPolySupport.HighContrast.Response.isSkewMat_neg {d : ℕ} {g : Mat d} (hg : IsSkewMat g) : IsSkewMat (-g)

theorem HCPolySupport.HighContrast.Response.le_skewShiftUpper {d : ℕ} {lam Lam : ℝ} (hlam : 0 < lam) (hle : lam ≤ Lam) (g : Mat d) : lam ≤ skewShiftUpper lam Lam g

theorem HCPolySupport.HighContrast.Response.isEllipticMatrix_sub_skew {d : ℕ} {lam Lam : ℝ} {A g : Mat d} (hA : IsEllipticMatrix lam Lam A) (hg : IsSkewMat g) : IsEllipticMatrix lam (skewShiftUpper lam Lam g) (A - g)

Uniform ellipticity is preserved when a constant skew matrix is subtracted.

noncomputable def HCPolySupport.HighContrast.CoeffSpace.subSkew {d : ℕ} (a : CoeffSpace d) (g : Mat d) (hg : IsSkewMat g) : CoeffSpace d

Recenter a coefficient sample by subtracting a constant skew matrix.

Equations

• a.subSkew g hg = ⟨MeasureTheory.AEEqFun.mk (fun (x : HCPolySupport.Vec d) => ↑↑a x - g) ⋯, ⋯⟩

theorem HCPolySupport.HighContrast.CoeffSpace.subSkew_ae {d : ℕ} (a : CoeffSpace d) (g : Mat d) (hg : IsSkewMat g) : ↑↑(a.subSkew g hg) =ᵐ[MeasureTheory.volume] fun (x : Vec d) => ↑↑a x - g

The recentered quotient sample has the expected pointwise representative almost everywhere.

theorem HCPolySupport.HighContrast.CoeffSpace.coeffOn_subSkew_ae {d : ℕ} (a : CoeffSpace d) (U : Book.Ch02.Domain d) (g : Mat d) (hg : IsSkewMat g) : ((a.subSkew g hg).coeffOn U).toCoeffField =ᵐ[volumeMeasureOn U.carrier] fun (x : Vec d) => (a.coeffOn U).toCoeffField x - g

On a Chapter 2 domain, recentering is represented by pointwise subtraction of the same constant skew matrix.

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

Transposition reverses the sign of a constant-skew recentering.