High-contrast homogenization: Provider.PolynomialHomogenization.FractionalMeanJumpLinear

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

Linear cross-average control of mean jumps

noncomputable def HCPolySupport.HighContrast.normalizedJumpMeasure {d : ℕ} (E : Set (Vec d)) : MeasureTheory.Measure (Vec d)

Volume restricted to E and rescaled by the inverse of volume E for mean jumps.

Equations

• HCPolySupport.HighContrast.normalizedJumpMeasure E = (MeasureTheory.volume E)⁻¹ • MeasureTheory.volume.restrict E

theorem HCPolySupport.HighContrast.edist_volumeAverageVec_le_crossDistanceAverage {d : ℕ} {E F : Set (Vec d)} (hEpos : 0 < MeasureTheory.volume E) (hEtop : MeasureTheory.volume E ≠ ⊤) (hFpos : 0 < MeasureTheory.volume F) (hFtop : MeasureTheory.volume F ≠ ⊤) {G : Vec d → Vec d} (hGE : MeasureTheory.Integrable G (MeasureTheory.volume.restrict E)) (hGF : MeasureTheory.Integrable G (MeasureTheory.volume.restrict F)) : edist (HilbertVec.ofVec (volumeAverageVec E G)) (HilbertVec.ofVec (volumeAverageVec F G)) ≤ (MeasureTheory.volume E)⁻¹ * (MeasureTheory.volume F)⁻¹ * ∫⁻ (x : Vec d) in E, ∫⁻ (y : Vec d) in F, ENNReal.ofReal (euclideanDist (G x) (G y))

The distance between two vector-valued volume averages is bounded by the normalized cross average of pointwise distances.