Documentation

LeanPool.HighContrastHomogenization.Provider.Regularity.CorrectorNormalizedL2Bridge

High-contrast homogenization: Provider.Regularity.CorrectorNormalizedL2Bridge #

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

Bridge from cube L² norms to the frozen normalized ball norm #

The regularity chain uses the real-valued cubeLpNorm, while the frozen Liouville carrier uses the non-vacuous ENNReal-valued normalizedL2Norm. This module relates them without changing either public definition.

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

Probability-style normalization of volume on an arbitrary measurable set. No nonzero-volume assertion is built into the definition.

Equations
Instances For
    source
    theorem HCPolySupport.HighContrast.normalizedL2Norm_eq_eLpNorm_volumeNormalizedMeasure {d : ℕ} (V : Set (Vec d)) (f : Vec d → ℝ) (hf : MeasureTheory.AEStronglyMeasurable f (volumeNormalizedMeasure V)) :
    normalizedL2Norm V f = MeasureTheory.eLpNorm f 2 (volumeNormalizedMeasure V)

    The frozen normalized L² norm is exactly the ordinary eLpNorm for the explicitly volume-normalized restricted measure.

    source
    theorem HCPolySupport.HighContrast.normalizedL2Norm_mono_set_le_volumeRatio {d : ℕ} {U V : Set (Vec d)} (hUV : U ⊆ V) (hUzero : MeasureTheory.volume U ≠ 0) (hUtop : MeasureTheory.volume U ≠ ⊤) (hVzero : MeasureTheory.volume V ≠ 0) (hVtop : MeasureTheory.volume V ≠ ⊤) (f : Vec d → ℝ) :
    normalizedL2Norm U f ≤ (MeasureTheory.volume V / MeasureTheory.volume U) ^ (1 / 2) * normalizedL2Norm V f

    Restricting a normalized L² norm to a smaller positive finite-volume set costs the square root of the volume ratio.

    source
    theorem HCPolySupport.HighContrast.normalizedL2Norm_openCubeSet_eq_ofReal_cubeLpNorm {d : ℕ} (Q : TriadicCube d) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f 2 (normalizedCubeMeasure Q)) :
    normalizedL2Norm (openCubeSet Q) f = ENNReal.ofReal (cubeLpNorm Q 2 f)

    On an open triadic cube, the frozen normalized norm is the ENNReal lift of cubeLpNorm, provided the local L² norm is finite.

    source
    theorem HCPolySupport.HighContrast.NormalizedLocalH1Carrier.memLp_globalValueRepresentative_normalizedCubeMeasure {d : ℕ} (z : NormalizedLocalH1Carrier d) (q : ℕ) :
    MeasureTheory.MemLp z.globalValueRepresentative 2 (normalizedCubeMeasure (originCube d ↑q))

    The global representative of a normalized local carrier is square integrable for the normalized measure on every exhaustion cube.

    source
    theorem HCPolySupport.HighContrast.normalizedL2Norm_euclideanBall_le_outerCube {d : ℕ} [NeZero d] {r : ℝ} (hr : 0 < r) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f 2 (normalizedCubeMeasure (originCube d (outerTriadicGeneration (2 * r) ⋯)))) :
    normalizedL2Norm (euclideanBall d r) f ≤ ENNReal.ofReal ((3 * √↑d) ^ d) ^ (1 / 2) * ENNReal.ofReal (cubeLpNorm (originCube d (outerTriadicGeneration (2 * r) ⋯)) 2 f)

    The frozen normalized ball norm is controlled by the normalized norm on the canonical enclosing triadic cube with a dimension-only ENNReal factor.