Documentation

LeanPool.HighContrastHomogenization.Support.Besov.Negative.ExactAggregationBridge

Coarse-graining support: Support.Besov.Negative.ExactAggregationBridge #

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

Finite aggregation transport for exact negative Besov kernels #

Source-neutral ENNReal transport lemmas for passing from finite real aggregations to the extended finite and infinite aggregations used by the exact Chapter 1 kernels. They retain extended-value behavior without analytic convergence or real-valued upper-bound hypotheses.

source
theorem HCPolySupport.exactAggregation_ofReal_finiteLq (a : ℕ → ℝ) (N : ℕ) (q : ℝ) (ha : ∀ i ∈ Finset.range (N + 1), 0 ≤ a i) (hq : 0 ≤ q) :
ENNReal.ofReal ((∑ i ∈ Finset.range (N + 1), a i ^ q) ^ q⁻¹) = (∑ i ∈ Finset.range (N + 1), ENNReal.ofReal (a i) ^ q) ^ q⁻¹

The ENNReal embedding of a nonnegative finite real ℓ^q expression is the corresponding finite extended expression.

source
theorem HCPolySupport.exactAggregation_finiteLq_le_tsum (a : ℕ → ENNReal) (N : ℕ) (q : ℝ) (hq : 0 ≤ q) :
(∑ i ∈ Finset.range (N + 1), a i ^ q) ^ q⁻¹ ≤ (∑' (i : ℕ), a i ^ q) ^ q⁻¹

A finite extended ℓ^q aggregation is bounded by its infinite tsum aggregation. This deliberately remains valid when the right side is ∞.

source
def HCPolySupport.exactAggregationOfRealSupHom :
SupHom ℝ ENNReal

The maximum-preserving map from real numbers to extended nonnegative reals given by ENNReal.ofReal.

Equations
Instances For
    source
    theorem HCPolySupport.exactAggregation_ofReal_finiteSup_le_iSup (a : ℕ → ℝ) (N : ℕ) :
    ENNReal.ofReal ((Finset.range (N + 1)).sup' ⋯ a) ≤ ⨆ (i : ℕ), ENNReal.ofReal (a i)

    The ENNReal embedding of a finite real maximum is bounded by the extended iSup of the embedded terms.

    source
    theorem HCPolySupport.exactAggregation_ofReal_finiteLq_le_tsum_of_term_eq (a : ℕ → ℝ) (b : ℕ → ENNReal) (N : ℕ) (q : ℝ) (ha : ∀ i ∈ Finset.range (N + 1), 0 ≤ a i) (hq : 0 ≤ q) (hterm : ∀ i ∈ Finset.range (N + 1), ENNReal.ofReal (a i) = b i) :
    ENNReal.ofReal ((∑ i ∈ Finset.range (N + 1), a i ^ q) ^ q⁻¹) ≤ (∑' (i : ℕ), b i ^ q) ^ q⁻¹

    A pointwise finite-term bridge transports a legacy finite real ℓ^q aggregation directly into an infinite exact tsum aggregation.

    source
    theorem HCPolySupport.exactAggregation_ofReal_finiteSup_le_iSup_of_term_eq (a : ℕ → ℝ) (b : ℕ → ENNReal) (N : ℕ) (hterm : ∀ i ∈ Finset.range (N + 1), ENNReal.ofReal (a i) = b i) :
    ENNReal.ofReal ((Finset.range (N + 1)).sup' ⋯ a) ≤ ⨆ (i : ℕ), b i

    A pointwise finite-term bridge transports a legacy finite real maximum directly into an exact extended iSup.

    source
    theorem HCPolySupport.exactAggregation_overlapPartialSeminorm_le_exactOverlapFiniteSeminorm {d : ℕ} (P : ExactOverlapFiniteParameters) (Q : TriadicCube d) (u : Vec d → ℝ) (hmem : MeasureTheory.MemLp u (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) (N : ℕ) :
    ENNReal.ofReal (cubeBesovOverlapPartialSeminorm Q P.s (ENNReal.ofReal P.p) (ENNReal.ofReal P.q) N u) ≤ exactOverlapFiniteSeminorm P Q u ⋯

    A finite legacy overlap-positive ℓ^q truncation is dominated by the exact extended overlap seminorm, with the parent MemLp data supplying the canonical local-integrability witness.

    source
    theorem HCPolySupport.exactAggregation_overlapPartialSeminormTop_le_exactOverlapTopSeminorm {d : ℕ} (P : ExactOverlapTopParameters) (Q : TriadicCube d) (u : Vec d → ℝ) (hmem : MeasureTheory.MemLp u (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) (N : ℕ) :
    ENNReal.ofReal (cubeBesovOverlapPartialSeminormTop Q P.s (ENNReal.ofReal P.p) N u) ≤ exactOverlapTopSeminorm P Q u ⋯

    A finite legacy overlap-positive supremum truncation is dominated by the exact extended overlap endpoint seminorm.

    source
    theorem HCPolySupport.exactAggregation_overlapPartialNorm_le_exactOverlapFiniteNorm {d : ℕ} (P : ExactOverlapFiniteParameters) (Q : TriadicCube d) (u : Vec d → ℝ) (hmem : MeasureTheory.MemLp u (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) (N : ℕ) :
    ENNReal.ofReal (cubeBesovOverlapPartialNorm Q P.s (ENNReal.ofReal P.p) (ENNReal.ofReal P.q) N u) ≤ exactOverlapFiniteNorm P Q u ⋯

    The finite inhomogeneous overlap-positive truncation is dominated by the exact extended norm; its root mean transports exactly.

    source
    theorem HCPolySupport.exactAggregation_overlapPartialNormTop_le_exactOverlapTopNorm {d : ℕ} (P : ExactOverlapTopParameters) (Q : TriadicCube d) (u : Vec d → ℝ) (hmem : MeasureTheory.MemLp u (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) (N : ℕ) :
    ENNReal.ofReal (cubeBesovOverlapPartialNormTop Q P.s (ENNReal.ofReal P.p) N u) ≤ exactOverlapTopNorm P Q u ⋯

    The finite inhomogeneous overlap-positive endpoint truncation is dominated by the exact extended endpoint norm.

    source
    theorem HCPolySupport.exactAggregation_circPartialNorm_le_exactCircFiniteSeminorm {d : ℕ} (P : ExactCircFiniteParameters) (Q : TriadicCube d) (f : Vec d → ℝ) (hmem : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) (N : ℕ) :
    ENNReal.ofReal (cubeBesovCircPartialNorm Q P.s (ENNReal.ofReal P.p) (ENNReal.ofReal P.q) N f) ≤ exactCircFiniteSeminorm P Q f ⋯

    A finite legacy circ ℓ^q truncation is dominated by the exact extended circ seminorm, under the canonical block-integrability witness.

    source
    theorem HCPolySupport.exactAggregation_circPartialNormTop_le_exactCircTopSeminorm {d : ℕ} (P : ExactCircTopParameters) (Q : TriadicCube d) (f : Vec d → ℝ) (hmem : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) (N : ℕ) :
    ENNReal.ofReal (cubeBesovCircPartialNormTop Q P.s (ENNReal.ofReal P.p) N f) ≤ exactCircTopSeminorm P Q f ⋯

    A finite legacy circ supremum truncation is dominated by the exact extended circ endpoint seminorm.