Coarse-graining support: Support.Besov.Negative.ExactCircDominationFinite

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

Exact finite-interior dual-to-circ comparison

This module proves the Chapter 1 comparison for 1 < q < ∞ directly on the exact extended-valued kernels. All local integrability, finite truncation, and projection-limit inputs are derived from the two parent MemLp certificates.

theorem HCPolySupport.exactDualFiniteHattedSeminorm_le_exactCircFiniteSeminorm {d : ℕ} (P : ExactDualFiniteParameters) (Q : TriadicCube d) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) : exactDualFiniteHattedSeminorm P Q f hf ≤ 3 ^ (↑d + P.s) * exactCircFiniteSeminorm P.circParameters Q f ⋯

Exact finite-interior hatted dual seminorm is controlled by the exact concrete circ seminorm with the manuscript coefficient.

theorem HCPolySupport.exactDualFiniteFullNorm_le_exactCircFiniteSeminorm_add_root {d : ℕ} (P : ExactDualFiniteParameters) (Q : TriadicCube d) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f (ENNReal.ofReal P.p) (normalizedCubeMeasure Q)) : exactDualFiniteFullNorm P Q f hf ≤ 3 ^ (↑d + P.s) * exactCircFiniteSeminorm P.circParameters Q f ⋯ + exactCircDepthWeight Q P.s 0 * ENNReal.ofReal |cubeAverage Q f|

Exact finite-interior full dual norm is controlled by the exact concrete circ seminorm, with the literal manuscript root term retained on the right.