Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch03.ABK26.LocalCoarseGrainingAggregation

Coarse-graining support: Support.Book.Ch03.ABK26.LocalCoarseGrainingAggregation #

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

Finite-p local coarse-graining aggregation algebra #

This file contains the elementary ENNReal power identities used to assemble the finite-p local coarse-graining estimate. It has no PDE content.

source
noncomputable def HCPolySupport.Book.Ch03.ABK26.descendantsAtScaleENNAverage {d : ℕ} (Q : TriadicCube d) (k : ℤ) (F : TriadicCube d → ENNReal) :
ENNReal

The normalized ENNReal average over descendants at a prescribed physical triadic scale.

Equations
Instances For
    source
    theorem HCPolySupport.Book.Ch03.ABK26.descendantsAtScaleENNAverage_eq_descendantsENNAverage {d : ℕ} (Q : TriadicCube d) (k : ℤ) (hk : k ≤ Q.scale) (F : TriadicCube d → ENNReal) :
    descendantsAtScaleENNAverage Q k F = descendantsENNAverage Q (Q.scale - k).toNat F

    At an admissible physical scale, the physical-scale average is precisely the canonical depth-descendant average.

    source
    theorem HCPolySupport.Book.Ch03.ABK26.cubeEuclideanNegativeBesovESeminorm_rpow_eq_tsum_depthEnergy {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : CubeEuclideanLpField Q FiniteLpExponent.two) :
    cubeEuclideanNegativeBesovESeminorm Q s p F ^ p.exponent.toReal = ∑' (j : ℕ), cubeEuclideanNegativeBesovDepthEnergy Q s p F j

    Raising the running-scale negative Besov seminorm to the finite exponent recovers its unrooted depth-energy series.

    source
    theorem HCPolySupport.Book.Ch03.ABK26.weightedLocalSymmetricEnergyLp_rpow_eq_tsum {d : ℕ} (Q : TriadicCube d) (n : ℤ) (hn : n ≤ Q.scale) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (u : H1Function (openCubeSet Q)) (s1 s : ↑FractionalOrder) (p : FiniteLpExponent) :
    weightedLocalSymmetricEnergyLp Q n hn a u s1 s p ^ p.exponent.toReal = ∑' (j : ℕ), ENNReal.ofReal (Real.rpow 3 (-((↑s - ↑s1) * p.exponent.toReal * ↑j))) * (↑(descendantsAtScale Q (n - ↑j)).card)⁻¹ * ∑ R ∈ (descendantsAtScale Q (n - ↑j)).attach, localSymmetricEnergyENorm (↑R) (a.restrictToSubcube ⋯) (restrictH1ToSubcube u ⋯) ^ p.exponent.toReal

    Raising the weighted local symmetric-energy aggregation to the finite exponent exposes its exact running physical-scale series.

    source
    theorem HCPolySupport.Book.Ch03.ABK26.descendantsENNAverage_succ_eq_descendantsENNAverage_descendantsENNAverage {d : ℕ} (Q : TriadicCube d) (j : ℕ) (F : TriadicCube d → ENNReal) :
    descendantsENNAverage Q (j + 1) F = descendantsENNAverage Q j fun (R : TriadicCube d) => descendantsENNAverage R 1 F

    Normalized ENNReal descendant averages compose exactly across one triadic generation.

    source
    theorem HCPolySupport.Book.Ch03.ABK26.descendantsENNAverage_add_eq_descendantsENNAverage_descendantsENNAverage {d : ℕ} (Q : TriadicCube d) (j n : ℕ) (F : TriadicCube d → ENNReal) :
    descendantsENNAverage Q (j + n) F = descendantsENNAverage Q j fun (R : TriadicCube d) => descendantsENNAverage R n F

    Normalized ENNReal descendant averages compose at arbitrary finite depths.

    source
    theorem HCPolySupport.Book.Ch03.ABK26.geometricDiscount_rpow_neg_inv_le_twentyFive_mul_inv {delta alpha : ℝ} (hdelta : 0 < delta) (hdelta_le : delta ≤ 1) (halpha : 2 ≤ alpha) :
    (Ch02.geometricDiscount delta alpha).rpow (-1 / alpha) ≤ 25 * delta⁻¹

    The rooted geometric-tail loss is bounded by a single inverse gap, with a constant independent of the finite exponent.

    source
    theorem HCPolySupport.Book.Ch03.ABK26.geometricDiscount_rpow_neg_inv_le_twentyFive_mul_inv_finiteLp {delta : ℝ} (hdelta : 0 < delta) (hdelta_le : delta ≤ 1) (p : FiniteLpExponent) (hp : 2 ≤ p.exponent.toReal) :
    (Ch02.geometricDiscount delta p.exponent.toReal).rpow (-1 / p.exponent.toReal) ≤ 25 * delta⁻¹

    The preceding uniform tail bound specialized to a finite Lp exponent.

    source
    theorem HCPolySupport.Book.Ch03.ABK26.ENNReal_tsum_triadic_rpow_root_le_twentyFive_mul_inv {delta alpha : ℝ} (hdelta : 0 < delta) (hdelta_le : delta ≤ 1) (halpha : 2 ≤ alpha) :
    (∑' (j : ℕ), ENNReal.ofReal (Real.rpow 3 (-delta * alpha)) ^ j) ^ (1 / alpha) ≤ ENNReal.ofReal (25 * delta⁻¹)

    ENNReal geometric-series form of the exponent-uniform rooted tail bound. The ratio is the triadic decay at gap delta.

    source
    theorem HCPolySupport.Book.Ch03.ABK26.ENNReal_tsum_triadic_rpow_root_le_twentyFive_mul_inv_finiteLp {delta : ℝ} (hdelta : 0 < delta) (hdelta_le : delta ≤ 1) (p : FiniteLpExponent) (hp : 2 ≤ p.exponent.toReal) :
    (∑' (j : ℕ), ENNReal.ofReal (Real.rpow 3 (-delta * p.exponent.toReal)) ^ j) ^ (1 / p.exponent.toReal) ≤ ENNReal.ofReal (25 * delta⁻¹)

    Finite-Lp specialization of the ENNReal triadic tail bound.