Coarse-graining support: Support.Besov.Negative.ExactCircDominationTop #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Exact circ domination at the negative q = ∞ endpoint #
This file proves the source-facing comparison between the exact dual-negative
endpoint and the exact concrete circ endpoint. All finite projected-pairing
premises are derived internally from the parent MemLp certificates carried
by the exact definitions.
theorem
HCPolySupport.exactDualTopHattedSeminorm_le_exactCircTopSeminorm
{d : ℕ}
(P : ExactDualTopParameters)
(Q : TriadicCube d)
(f : Vec d → ℝ)
(hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q))
:
The exact hatted negative q = ∞ seminorm is bounded by the exact
concrete circ endpoint with the Chapter 1 coefficient.
theorem
HCPolySupport.exactDualTopFullNorm_le_exactCircTopSeminorm_add_root
{d : ℕ}
(P : ExactDualTopParameters)
(Q : TriadicCube d)
(f : Vec d → ℝ)
(hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q))
:
exactDualTopFullNorm P Q f hf ≤ 3 ^ (↑d + P.s) * exactCircTopSeminorm P.circParameters Q f ⋯ + exactCircDepthWeight Q P.s 0 * ENNReal.ofReal |cubeAverage Q f|
The exact full negative q = ∞ norm obeys the manuscript comparison.
The depth-zero circ term already controls the root contribution; the explicit
nonnegative source root term is retained in the stated right-hand side.