Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.W1p.GlobalAffineLp

Coarse-graining support: Support.Sobolev.W1p.GlobalAffineLp #

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Global affine expansion in finite Lᵖ #

This file isolates the volume transport and strong finite-Lᵖ continuity of the outward affine map used by inward mollification.

source
def HCPolySupport.globalAffineExpansion {d : ℕ} (x0 : Vec d) (ε : ℝ) :
Vec d → Vec d

The outward affine map based at x0 with expansion parameter ε.

Equations
Instances For
    source
    @[simp]
    theorem HCPolySupport.globalAffineExpansion_apply {d : ℕ} (x0 x : Vec d) (ε : ℝ) :
    globalAffineExpansion x0 ε x = (1 + ε) • x - ε • x0
    source
    theorem HCPolySupport.map_globalAffineExpansion_volume {d : ℕ} (x0 : Vec d) {ε : ℝ} (hε : 0 ≤ ε) :
    MeasureTheory.Measure.map (globalAffineExpansion x0 ε) MeasureTheory.volume = ENNReal.ofReal ((1 + ε) ^ d)⁻¹ • MeasureTheory.volume

    The outward affine expansion pushes Lebesgue measure forward by the Jacobian factor of its scalar linear part.

    source
    theorem HCPolySupport.quasiMeasurePreserving_globalAffineExpansion {d : ℕ} (x0 : Vec d) {ε : ℝ} (hε : 0 ≤ ε) :
    MeasureTheory.QuasiMeasurePreserving (globalAffineExpansion x0 ε) MeasureTheory.volume MeasureTheory.volume

    The outward affine expansion is quasi-measure-preserving for Lebesgue measure whenever its scalar factor is positive.

    source
    theorem HCPolySupport.Filter.EventuallyEq.comp_globalAffineExpansion {d : ℕ} {f g : Vec d → ℝ} (hfg : f =ᵐ[MeasureTheory.volume] g) (x0 : Vec d) {ε : ℝ} (hε : 0 ≤ ε) :
    f ∘ globalAffineExpansion x0 ε =ᵐ[MeasureTheory.volume] g ∘ globalAffineExpansion x0 ε

    Almost-everywhere equal fields remain almost-everywhere equal after an outward affine expansion.

    source
    theorem HCPolySupport.MemLp.comp_globalAffineExpansion {d : ℕ} {g : Vec d → ℝ} {p : ENNReal} (hg : MeasureTheory.MemLp g p MeasureTheory.volume) (x0 : Vec d) {ε : ℝ} (hε : 0 ≤ ε) :
    MeasureTheory.MemLp (g ∘ globalAffineExpansion x0 ε) p MeasureTheory.volume

    Finite Lᵖ functions remain in Lᵖ after an outward affine expansion.

    source
    theorem HCPolySupport.eLpNorm_comp_globalAffineExpansion {d : ℕ} {g : Vec d → ℝ} {p : ENNReal} (hp : p ≠ ⊤) (hg : MeasureTheory.MemLp g p MeasureTheory.volume) (x0 : Vec d) {ε : ℝ} (hε : 0 ≤ ε) :
    MeasureTheory.eLpNorm (g ∘ globalAffineExpansion x0 ε) p MeasureTheory.volume = ENNReal.ofReal ((1 + ε) ^ d)⁻¹ ^ (1 / p).toReal * MeasureTheory.eLpNorm g p MeasureTheory.volume

    Exact finite-Lᵖ norm transport under an outward affine expansion.

    source
    theorem HCPolySupport.tendsto_eLpNorm_comp_globalAffineExpansion_sub_zero {d : ℕ} {g : Vec d → ℝ} {p : ENNReal} (hp : 1 ≤ p) (hp_top : p ≠ ⊤) (hg : MeasureTheory.MemLp g p MeasureTheory.volume) (x0 : Vec d) {ε : ℕ → ℝ} (hε : Filter.Tendsto ε Filter.atTop (nhds 0)) (hε_nonneg : ∀ (n : ℕ), 0 ≤ ε n) :
    Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (g ∘ globalAffineExpansion x0 (ε n) - g) p MeasureTheory.volume) Filter.atTop (nhds 0)

    Outward affine expansions are strongly continuous on global finite Lᵖ. The conclusion is stated for scalar fields; downstream weak-gradient arguments apply it coordinatewise.