High-contrast homogenization:

Provider.PolynomialHomogenization.ScheduledLocalizationGaugeReduction

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

Gauge reduction data for the scheduled localization step

The Dirichlet estimate is consumed on the gauge-reduced domain Uhat = L⁻¹ U, where L is the square root of the symmetric part of the comparison matrix. This module supplies the four pieces of that reduction which are needed before any localization estimate can be asked for:

• a locally uniformly elliptic source representative of the gauge-reduced, skew-centered coefficient;
• positivity of the output distortion factor;
• finiteness of the transported boundary energy;
• the open bounded convex geometry and ball sandwich of Uhat.

Ellipticity under an invertible linear pullback

noncomputable def HCPolySupport.HighContrast.affineLowerEllipticity {d : ℕ} (L : Mat d) (lam : ℝ) : ℝ

The lower and upper ellipticity constants of a linear pullback.

Equations

• HCPolySupport.HighContrast.affineLowerEllipticity L lam = lam / max 1 (HCPolySupport.Book.Ch02.matrixFrobeniusNormSq (HCPolySupport.matTranspose L))

noncomputable def HCPolySupport.HighContrast.affineUpperEllipticity {d : ℕ} (L : Mat d) (Lam : ℝ) : ℝ

The upper ellipticity constant of a linear pullback.

Equations

• HCPolySupport.HighContrast.affineUpperEllipticity L Lam = max Lam (HCPolySupport.Book.Ch02.matrixFrobeniusNormSq L⁻¹ * Lam)

theorem HCPolySupport.HighContrast.affineLowerEllipticity_pos {d : ℕ} {L : Mat d} {lam : ℝ} (hlam : 0 < lam) : 0 < affineLowerEllipticity L lam

theorem HCPolySupport.HighContrast.affineLowerEllipticity_le_affineUpperEllipticity {d : ℕ} {L : Mat d} {lam Lam : ℝ} (hlam : 0 < lam) (hle : lam ≤ Lam) : affineLowerEllipticity L lam ≤ affineUpperEllipticity L Lam

theorem HCPolySupport.HighContrast.isEllipticMatrix_affineCoefficient {d : ℕ} (L : Mat d) (hL : IsUnit (Matrix.det L)) {b : CoeffField d} {lam Lam : ℝ} {y : Vec d} (hb : IsEllipticMatrix lam Lam (b (matVecMul L y))) : IsEllipticMatrix (affineLowerEllipticity L lam) (affineUpperEllipticity L Lam) (affineCoefficient L hL b y)

Uniform ellipticity is carried by an invertible linear pullback, with the distortion paid by the Frobenius norms of the matrix and of its inverse.

theorem HCPolySupport.HighContrast.aeElliptic_affineCoefficient {d : ℕ} (L : Mat d) (hL : IsUnit (Matrix.det L)) {b : CoeffField d} {lam Lam : ℝ} (hb : ∀ᵐ (x : Vec d), IsEllipticMatrix lam Lam (b x)) : ∀ᵐ (y : Vec d), IsEllipticMatrix (affineLowerEllipticity L lam) (affineUpperEllipticity L Lam) (affineCoefficient L hL b y)

The gauge-reduced source field

theorem HCPolySupport.HighContrast.isAELocallyUniformlyElliptic_affineCoefficient {d : ℕ} (L : Mat d) (hL : IsUnit (Matrix.det L)) {b : CoeffField d} (hb : IsAELocallyUniformlyElliptic b) : IsAELocallyUniformlyElliptic (affineCoefficient L hL b)

Local uniform ellipticity is carried by an invertible linear pullback: the ball of a given radius is served by the constants of a ball of proportional radius, with the distortion paid by the Frobenius norms.

theorem HCPolySupport.HighContrast.exists_affineCoefficientSource {d : ℕ} (L : Mat d) (hL : IsUnit (Matrix.det L)) {b : CoeffField d} (hbmeas : MeasureTheory.AEStronglyMeasurable b MeasureTheory.volume) (hbEll : IsAELocallyUniformlyElliptic b) : ∃ (aSource : Source.AKL.Field d), AEUniformlyEllipticField aSource ∧ ↑aSource =ᵐ[MeasureTheory.volume] affineCoefficient L hL b

A globally measurable, locally uniformly elliptic field has a locally uniformly elliptic source representative after any invertible linear pullback.

theorem HCPolySupport.HighContrast.exists_gaugeReducedSource {d : ℕ} {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) {epsilon : ℝ} (hEpsilon : 0 < epsilon) (aSample : CoeffSpace d) : ∃ (aSource : Source.AKL.Field d), AEUniformlyEllipticField aSource ∧ ↑aSource =ᵐ[MeasureTheory.volume] affineCoefficient (matSqrt (symmPart abar)) ⋯ fun (x : Vec d) => scaledCoeff epsilon aSample x - skewPart abar

The gauge-reduced, skew-centered rescaled coefficient of the scheduled estimate has a locally uniformly elliptic source representative.

Distortion factor and transported boundary energy

theorem HCPolySupport.HighContrast.hsNormSq_matVecMul_ne_top {d : ℕ} (M : Mat d) (V : Set (Vec d)) (s : ℝ) {F : Vec d → Vec d} (hF : hsNormSq V s F ≠ ⊤) : (hsNormSq V s fun (x : Vec d) => matVecMul M (F x)) ≠ ⊤

The boundary energy transported by a constant matrix stays finite.