Documentation

LeanPool.HighContrastHomogenization.Provider.PolynomialHomogenization.FractionalMeanJump

High-contrast homogenization: Provider.PolynomialHomogenization.FractionalMeanJump #

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

Fractional control of jumps between volume averages #

The difference of the volume averages on two positive finite sets is the average of the cross differences. Jensen's inequality on the two normalized volume measures therefore controls the squared mean jump by the cross Gagliardo energy. A union estimate records the volume factor in a form suited to chains of comparable cells.

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

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

Equations
Instances For
    source
    theorem HCPolySupport.HighContrast.ofReal_vecNormSq_sub_volumeAverageVec_le_crossAverage {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)) :
    ENNReal.ofReal (vecNormSq (volumeAverageVec E G - volumeAverageVec F G)) ≤ (MeasureTheory.volume E)⁻¹ * (MeasureTheory.volume F)⁻¹ * ∫⁻ (x : Vec d) in E, ∫⁻ (y : Vec d) in F, ENNReal.ofReal (vecNormSq (G x - G y))

    The squared jump between two volume averages is bounded by the normalized cross average of the pointwise squared differences.

    source
    theorem HCPolySupport.HighContrast.ofReal_vecNormSq_sub_volumeAverageVec_le_crossFracIntegral {d : ℕ} (hd : 1 ≤ d) {E F : Set (Vec d)} (hEmeas : MeasurableSet E) (hFmeas : MeasurableSet F) (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)) {s D : ℝ} (hs : 0 ≤ s) (hD : 0 < D) (hcrossDiam : ∀ x ∈ E, ∀ y ∈ F, √(vecNormSq (x - y)) ≤ D) :
    ENNReal.ofReal (vecNormSq (volumeAverageVec E G - volumeAverageVec F G)) ≤ (MeasureTheory.volume E)⁻¹ * (MeasureTheory.volume F)⁻¹ * ENNReal.ofReal (D ^ (↑d + 2 * s)) * ∫⁻ (x : Vec d) in E, ∫⁻ (y : Vec d) in F, ENNReal.ofReal (vecNormSq (G x - G y) / √(vecNormSq (x - y)) ^ (↑d + 2 * s))

    A cross-diameter bound inserts the fractional Gagliardo kernel into the mean-jump estimate.

    source
    theorem HCPolySupport.HighContrast.ofReal_vecNormSq_sub_volumeAverageVec_le_unionFracSeminormSq {d : ℕ} (hd : 1 ≤ d) {E F : Set (Vec d)} (hEmeas : MeasurableSet E) (hFmeas : MeasurableSet F) (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)) {s D : ℝ} (hs : 0 ≤ s) (hD : 0 < D) (hcrossDiam : ∀ x ∈ E, ∀ y ∈ F, √(vecNormSq (x - y)) ≤ D) :
    ENNReal.ofReal (vecNormSq (volumeAverageVec E G - volumeAverageVec F G)) ≤ ((MeasureTheory.volume E)⁻¹ + (MeasureTheory.volume F)⁻¹) * ENNReal.ofReal (D ^ (↑d + 2 * s)) * fracSeminormSq (E ∪ F) s G

    On the union of two sets, the cross mean jump is controlled by the fractional seminorm with the exact symmetric volume factor volume(E)⁻¹ + volume(F)⁻¹.