High-contrast homogenization: Provider.PolynomialHomogenization.FractionalAmplitudeCrossEstimate

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

Cross-set distance control by the Gagliardo amplitude

theorem HCPolySupport.HighContrast.setLIntegral_fieldDistance_le_fractionalAmplitude {d : ℕ} {U F : Set (Vec d)} {x : Vec d} {s D : ℝ} {G : Vec d → Vec d} (hFmeas : MeasurableSet F) (hFsub : F ⊆ U) (hG : Measurable G) (hs : 0 ≤ ↑d + 2 * s) (hdist : ∀ y ∈ F, euclideanDist x y ≤ D) : ∫⁻ (y : Vec d) in F, ENNReal.ofReal (euclideanDist (G x) (G y)) ≤ fractionalGagliardoAmplitude U s G x * (MeasureTheory.volume F * ENNReal.ofReal (D ^ (↑d + 2 * s))) ^ (1 / 2)

On a set lying within distance D of x, the integral of field increments is bounded by the global fractional amplitude at x.