Documentation

LeanPool.HighContrastHomogenization.Provider.Regularity.CorrectorAnchoredMeanTelescope

High-contrast homogenization: Provider.Regularity.CorrectorAnchoredMeanTelescope #

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

Successive centered-cube mean control #

This module isolates the one-step estimate needed to telescope the means of a fixed-unit-normalized corrector. Its volume loss is dimension-only because only a parent cube and its central child are compared.

source
noncomputable def HCPolySupport.HighContrast.anchoredCorrectorMeanStepBound {d : ℕ} (z : NormalizedLocalH1Carrier d) (n : ℕ) :
ℝ

The scale-correct oscillation quantity controlling the jump from the nth centered-cube mean to the (n+1)st mean.

Equations
Instances For
    source
    theorem HCPolySupport.HighContrast.cubeLpNorm_originCube_pred_le_card_mul {d : ℕ} (k : ℤ) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f 2 (normalizedCubeMeasure (originCube d k))) :
    cubeLpNorm (originCube d (k - 1)) 2 f ≤ ↑(3 ^ d) * cubeLpNorm (originCube d k) 2 f

    Restricting a normalized L² norm from an origin cube to its central child costs at most the number of triadic children.

    source
    theorem HCPolySupport.HighContrast.abs_cubeAverage_originCube_pred_sub_le_card_mul_oscillation {d : ℕ} (k : ℤ) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f 2 (normalizedCubeMeasure (originCube d k))) :
    |cubeAverage (originCube d (k - 1)) f - cubeAverage (originCube d k) f| ≤ ↑(3 ^ d) * cubeBesovOscillation (originCube d k) 2 f

    The averages on a centered cube and its central child differ by at most a dimension-only multiple of the parent's normalized L² oscillation.

    source
    theorem HCPolySupport.HighContrast.NormalizedLocalH1Carrier.abs_cubeAverage_globalValueRepresentative_succ_sub_le_oscillation {d : ℕ} (z : NormalizedLocalH1Carrier d) (n : ℕ) :
    |cubeAverage (originCube d ↑n) z.globalValueRepresentative - cubeAverage (originCube d ↑(n + 1)) z.globalValueRepresentative| ≤ anchoredCorrectorMeanStepBound z n

    Successive averages of the global corrector representative satisfy the same one-step oscillation estimate, read through the outer canonical local H¹ representative.

    source
    theorem HCPolySupport.HighContrast.NormalizedLocalH1Carrier.abs_cubeAverage_globalValueRepresentative_zero_sub_le_sum {d : ℕ} (z : NormalizedLocalH1Carrier d) (n : ℕ) :
    |cubeAverage (originCube d 0) z.globalValueRepresentative - cubeAverage (originCube d ↑n) z.globalValueRepresentative| ≤ ∑ k ∈ Finset.range n, anchoredCorrectorMeanStepBound z k

    The displacement of the outer mean from the unit-cube mean is bounded by the finite sum of the scale-correct one-step oscillation quantities.

    source
    theorem HCPolySupport.HighContrast.NormalizedLocalH1Carrier.abs_cubeAverage_globalValueRepresentative_le_sum {d : ℕ} (z : NormalizedLocalH1Carrier d) (n : ℕ) :
    |cubeAverage (originCube d ↑n) z.globalValueRepresentative| ≤ ∑ k ∈ Finset.range n, anchoredCorrectorMeanStepBound z k

    Fixed-unit normalization turns the finite telescope into a direct bound for the absolute outer mean.