Coarse-graining support: Support.Besov.Negative.ExactCircDominationQOne #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Exact circ domination at the negative q = 1 endpoint #
This module proves the source-facing comparison between the exact dual
negative Besov kernel and the exact concrete circ kernel in the q = 1
branch. All local integrability and finite-truncation premises are derived
inside the proof from the single parent MemLp certificate.
theorem
HCPolySupport.exactDualQOneHattedSeminorm_le_exactCircFiniteSeminorm
{d : ℕ}
(P : ExactDualQOneParameters)
(Q : TriadicCube d)
(f : Vec d → ℝ)
(hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q))
:
exactDualQOneHattedSeminorm P Q f hf ≤ 3 ^ (↑d + P.s) * exactCircFiniteSeminorm P.circParameters Q f ⋯
At the negative q = 1 endpoint, the exact hatted dual seminorm is
controlled by the exact finite-q circ seminorm with the manuscript loss.
The only analytic premise is the canonical parent MemLp certificate.
theorem
HCPolySupport.exactDualQOneFullNorm_le_exactCircFiniteSeminorm_add_root
{d : ℕ}
(P : ExactDualQOneParameters)
(Q : TriadicCube d)
(f : Vec d → ℝ)
(hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q))
:
exactDualQOneFullNorm P Q f hf ≤ 3 ^ (↑d + P.s) * exactCircFiniteSeminorm P.circParameters Q f ⋯ + exactCircDepthWeight Q P.s 0 * ENNReal.ofReal |cubeAverage Q f|
At the negative q = 1 endpoint, the exact full dual norm satisfies the
manuscript comparison, including its explicit depth-zero root term.