High-contrast homogenization:

Provider.PolynomialHomogenization.FractionalMeanJumpAmplitudeAssembly

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

Assembly of a linear fractional-amplitude mean-jump estimate

theorem HCPolySupport.HighContrast.edist_volumeAverageVec_le_amplitudeAverage_of_cross {d : ℕ} {U E F : Set (Vec d)} {s : ℝ} {G : Vec d → Vec d} (hEmeas : MeasurableSet E) (hEpos : 0 < MeasureTheory.volume E) (hEtop : MeasureTheory.volume E ≠ ⊤) (hFpos : 0 < MeasureTheory.volume F) (hFtop : MeasureTheory.volume F ≠ ⊤) (hGE : MeasureTheory.Integrable G (MeasureTheory.volume.restrict E)) (hGF : MeasureTheory.Integrable G (MeasureTheory.volume.restrict F)) {C : ENNReal} (hCtop : C ≠ ⊤) (hcross : ∀ x ∈ E, ∫⁻ (y : Vec d) in F, ENNReal.ofReal (euclideanDist (G x) (G y)) ≤ MeasureTheory.volume F * C * fractionalGagliardoAmplitude U s G x) : edist (HilbertVec.ofVec (volumeAverageVec E G)) (HilbertVec.ofVec (volumeAverageVec F G)) ≤ C * (MeasureTheory.volume E)⁻¹ * ∫⁻ (x : Vec d) in E, fractionalGagliardoAmplitude U s G x

A pointwise cross-ball estimate against the global Gagliardo amplitude integrates to a linear bound for the corresponding jump of volume averages.