Documentation

LeanPool.HighContrastHomogenization.Support.Besov.Positive.ExactOverlapScalarP

Coarse-graining support: Support.Besov.Positive.ExactOverlapScalarP #

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

Exact scalar overlap aggregation at arbitrary finite p #

This additive finite-p module identifies the diagonal q = p exact overlap seminorm with the complete source depth-energy series and with the established finite-depth scalar-overlap truncations.

source
theorem HCPolySupport.FiniteLpExponent.one_le_toReal (p : FiniteLpExponent) :
1 ≤ p.exponent.toReal
source
noncomputable def HCPolySupport.exactOverlapScalarPParameters (s : ↑FractionalOrder) (p : FiniteLpExponent) :
ExactOverlapFiniteParameters

Exact scalar-overlap parameters in the diagonal finite case q = p.

Equations
Instances For
    source
    theorem HCPolySupport.exactOverlapScalarPSeminorm_rpow_eq_tsum_depthEnergy {d : ℕ} (s : ↑FractionalOrder) (p : FiniteLpExponent) (Q : TriadicCube d) (u : Vec d → ℝ) (hu : ExactOverlapIntegrable Q u) :
    exactOverlapFiniteSeminorm (exactOverlapScalarPParameters s p) Q u hu ^ p.exponent.toReal = ∑' (j : ℕ), exactOverlapDepthWeight Q (↑s) j ^ p.exponent.toReal * exactOverlapDepthAverage Q p.exponent.toReal u hu j

    The diagonal exact scalar seminorm has no hidden root inside its depth energies: its p-th power is the complete weighted depth-energy series.

    source
    theorem HCPolySupport.exactOverlapScalarPSeminorm_rpow_eq_iSup_partial {d : ℕ} (s : ↑FractionalOrder) (p : FiniteLpExponent) (Q : TriadicCube d) (u : Vec d → ℝ) (hu : ExactOverlapIntegrable Q u) (hmem : MeasureTheory.MemLp u p.exponent (normalizedCubeMeasure Q)) :
    exactOverlapFiniteSeminorm (exactOverlapScalarPParameters s p) Q u hu ^ p.exponent.toReal = ⨆ (N : ℕ), ENNReal.ofReal (cubeBesovOverlapPartialSeminorm Q (↑s) p.exponent p.exponent N u) ^ p.exponent.toReal

    Under parent-cube L^p membership, the exact diagonal scalar-overlap seminorm is the supremum of all finite-depth partial scalar-overlap seminorms after taking the exact p-th power.