High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorDecay.AffineNegOneTransport

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

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

The distortion of the normalized H¹ test norm under x = L y.

Equations

• HCPolySupport.HighContrast.h1AffineFactor L = max (|Matrix.det L| ^ (2 / ↑d)) (‖HCPolySupport.matTranspose L‖ ^ 2)

theorem HCPolySupport.HighContrast.h1AffineFactor_pos {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) : 0 < h1AffineFactor L

theorem HCPolySupport.HighContrast.h1NormSq_comp_matVecMul_le {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) {U : Set (Vec d)} (hU : MeasurableSet U) (hU0 : MeasureTheory.volume U ≠ 0) (psi : Vec d → Vec d) (hpsi : ContDiff ℝ (↑⊤) psi) : (h1NormSq U fun (y : Vec d) => psi (matVecMul L y)) ≤ ENNReal.ofReal (h1AffineFactor L) * h1NormSq (matImage L U) psi

Pulling an image-domain test back by L costs the explicit normalized H¹ affine factor.

theorem HCPolySupport.HighContrast.negOneNorm_matImage_le {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) {U : Set (Vec d)} (hU : MeasurableSet U) (hU0 : MeasureTheory.volume U ≠ 0) (F : Vec d → Vec d) : negOneNorm (matImage L U) F ≤ ENNReal.ofReal √(h1AffineFactor L) * negOneNorm U fun (y : Vec d) => F (matVecMul L y)

The normalized negative-one norm under an invertible affine image.