Coarse-graining support: Support.Besov.Duality.GlobalComparison

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

theorem HCPolySupport.finset_Lq_norm_le_sum_of_nonneg {ι : Type u_1} (s : Finset ι) {q : ℝ} (hq : 1 ≤ q) {f : ι → ℝ} (hf : ∀ i ∈ s, 0 ≤ f i) : (∑ i ∈ s, f i ^ q) ^ (1 / q) ≤ ∑ i ∈ s, f i

theorem HCPolySupport.cubeBesovCircDepthWeight_succ {d : ℕ} (Q : TriadicCube d) (s : ℝ) (j : ℕ) : cubeBesovCircDepthWeight Q s (j + 1) = 3 ^ (-s) * cubeBesovCircDepthWeight Q s j

theorem HCPolySupport.cubeBesovCircDepthWeight_eq_scaleWeight_neg_mul_geom {d : ℕ} (Q : TriadicCube d) (s : ℝ) (j : ℕ) : cubeBesovCircDepthWeight Q s j = cubeBesovScaleWeight (-s) Q * (3 ^ (-s)) ^ j

theorem HCPolySupport.cubeBesovCircDepthSeminorm_le_scaleWeight_neg_mul_geom_mul_cubeLpNorm {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (u : Vec d → ℝ) (j : ℕ) (hp : 1 ≤ p) (hpTop : p ≠ ⊤) (hu : MeasureTheory.MemLp u p (normalizedCubeMeasure Q)) : cubeBesovCircDepthSeminorm Q s p u j ≤ cubeBesovScaleWeight (-s) Q * (3 ^ (-s)) ^ j * cubeLpNorm Q p u

theorem HCPolySupport.cubeBesovCircPartialNorm_le_geometric_constant_of_memLp {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (u : Vec d → ℝ) (hs : 0 < s) (hu : MeasureTheory.MemLp u p (normalizedCubeMeasure Q)) (hp : 1 ≤ p) (hpTop : p ≠ ⊤) (hq : 1 ≤ q) (hqTop : q ≠ ⊤) : cubeBesovCircPartialNorm Q s p q N u ≤ cubeBesovScaleWeight (-s) Q * cubeLpNorm Q p u * (1 - 3 ^ (-s))⁻¹

theorem HCPolySupport.cubeBesovCircPartialNormTop_le_geometric_constant_of_memLp {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (N : ℕ) (u : Vec d → ℝ) (hs : 0 < s) (hu : MeasureTheory.MemLp u p (normalizedCubeMeasure Q)) (hp : 1 ≤ p) (hpTop : p ≠ ⊤) : cubeBesovCircPartialNormTop Q s p N u ≤ cubeBesovScaleWeight (-s) Q * cubeLpNorm Q p u * (1 - 3 ^ (-s))⁻¹

theorem HCPolySupport.cubeBesovCircNormEntry_le_geometric_constant_of_memLp {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (u : Vec d → ℝ) (hs : 0 < s) (hu : MeasureTheory.MemLp u p (normalizedCubeMeasure Q)) (hp : 1 ≤ p) (hpTop : p ≠ ⊤) (hq : 1 ≤ q) : cubeBesovCircNormEntry Q s p q N u ≤ cubeBesovScaleWeight (-s) Q * cubeLpNorm Q p u * (1 - 3 ^ (-s))⁻¹

theorem HCPolySupport.cubeBesovCircNormValueSet_bddAbove_of_memLp {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (u : Vec d → ℝ) (hs : 0 < s) (hu : MeasureTheory.MemLp u p (normalizedCubeMeasure Q)) (hp : 1 ≤ p) (hpTop : p ≠ ⊤) (hq : 1 ≤ q) : BddAbove (cubeBesovCircNormValueSet Q s p q u)

theorem HCPolySupport.cubeBesovCircNorm_le_geometric_constant_of_memLp {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (u : Vec d → ℝ) (hs : 0 < s) (hu : MeasureTheory.MemLp u p (normalizedCubeMeasure Q)) (hp : 1 ≤ p) (hpTop : p ≠ ⊤) (hq : 1 ≤ q) : cubeBesovCircNorm Q s p q u ≤ cubeBesovScaleWeight (-s) Q * cubeLpNorm Q p u * (1 - 3 ^ (-s))⁻¹

The full positive circ norm is controlled by the geometric Lᵖ bound used for each finite entry. This is a direct sSup wrapper around cubeBesovCircNormEntry_le_geometric_constant_of_memLp.

theorem HCPolySupport.CubeBesovDualMeanZeroTestGlobal.memLp {d : ℕ} {Q : TriadicCube d} {s : ℝ} {p q : ENNReal} {g : Vec d → ℝ} (hg : CubeBesovDualMeanZeroTestGlobal Q s p q g) : MeasureTheory.MemLp g (cubeBesovConjExponent p) (normalizedCubeMeasure Q)

theorem HCPolySupport.CubeBesovDualLocalMemLpGlobal.memLp {d : ℕ} {Q : TriadicCube d} {p : ENNReal} {g : Vec d → ℝ} (hg : CubeBesovDualLocalMemLpGlobal Q p g) : MeasureTheory.MemLp g (cubeBesovConjExponent p) (normalizedCubeMeasure Q)

theorem HCPolySupport.CubeBesovDualLocalMemLpGlobal.of_memLp_parent {d : ℕ} {Q : TriadicCube d} {p : ENNReal} {g : Vec d → ℝ} (hg : MeasureTheory.MemLp g (cubeBesovConjExponent p) (normalizedCubeMeasure Q)) : CubeBesovDualLocalMemLpGlobal Q p g

theorem HCPolySupport.CubeBesovDualFullTest.memLp {d : ℕ} {Q : TriadicCube d} {s : ℝ} {p q : ENNReal} {g : Vec d → ℝ} (hg : CubeBesovDualFullTest Q s p q g) : MeasureTheory.MemLp g (cubeBesovConjExponent p) (normalizedCubeMeasure Q)

theorem HCPolySupport.abs_cubeBesovPairing_le_max_mul_cubeBesovCircNorm_of_mean_zero_test {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (u g : Vec d → ℝ) (hBddCirc : BddAbove (cubeBesovCircNormValueSet Q s p q u)) (hu : MeasureTheory.MemLp u p (normalizedCubeMeasure Q)) (hp : 1 ≤ p) (hpTop : p ≠ ⊤) (hpConjTop : cubeBesovConjExponent p ≠ ⊤) (hq : 1 ≤ q) (hg : CubeBesovDualMeanZeroTestGlobal Q s p q g) : |cubeBesovPairing Q u g| ≤ max 1 (3 ^ s) * cubeBesovCircNorm Q s p q u

theorem HCPolySupport.cubeBesovDualMeanZeroSeminormValueSet_bddAbove {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (u : Vec d → ℝ) (hBddCirc : BddAbove (cubeBesovCircNormValueSet Q s p q u)) (hu : MeasureTheory.MemLp u p (normalizedCubeMeasure Q)) (hp : 1 ≤ p) (hpTop : p ≠ ⊤) (hpConjTop : cubeBesovConjExponent p ≠ ⊤) (hq : 1 ≤ q) : BddAbove (cubeBesovDualMeanZeroSeminormValueSet Q s p q u)

theorem HCPolySupport.cubeBesovDualMeanZeroSeminorm_le_max_mul_cubeBesovCircNorm {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (u : Vec d → ℝ) (hBddCirc : BddAbove (cubeBesovCircNormValueSet Q s p q u)) (hu : MeasureTheory.MemLp u p (normalizedCubeMeasure Q)) (hp : 1 ≤ p) (hpTop : p ≠ ⊤) (hpConjTop : cubeBesovConjExponent p ≠ ⊤) (hq : 1 ≤ q) : cubeBesovDualMeanZeroSeminorm Q s p q u ≤ max 1 (3 ^ s) * cubeBesovCircNorm Q s p q u

theorem HCPolySupport.abs_cubeBesovPairing_le_max_mul_cubeBesovCircNorm_of_full_test {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (u g : Vec d → ℝ) (hBddCirc : BddAbove (cubeBesovCircNormValueSet Q s p q u)) (hu : MeasureTheory.MemLp u p (normalizedCubeMeasure Q)) (hp : 1 ≤ p) (hpTop : p ≠ ⊤) (hpConjTop : cubeBesovConjExponent p ≠ ⊤) (hq : 1 ≤ q) (hg : CubeBesovDualFullTest Q s p q g) : |cubeBesovPairing Q u g| ≤ max 1 (3 ^ s) * cubeBesovCircNorm Q s p q u

theorem HCPolySupport.cubeBesovDualFullNorm_le_max_mul_cubeBesovCircNorm {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (u : Vec d → ℝ) (hBddCirc : BddAbove (cubeBesovCircNormValueSet Q s p q u)) (hu : MeasureTheory.MemLp u p (normalizedCubeMeasure Q)) (hp : 1 ≤ p) (hpTop : p ≠ ⊤) (hpConjTop : cubeBesovConjExponent p ≠ ⊤) (hq : 1 ≤ q) : cubeBesovDualFullNorm Q s p q u ≤ max 1 (3 ^ s) * cubeBesovCircNorm Q s p q u

theorem HCPolySupport.max_one_three_rpow_le_three_rpow_nat_add (d : ℕ) (s : ℝ) (hs : 0 ≤ s) : max 1 (3 ^ s) ≤ 3 ^ (↑d + s)

theorem HCPolySupport.cubeBesovCircNorm_nonneg {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (u : Vec d → ℝ) (hBddCirc : BddAbove (cubeBesovCircNormValueSet Q s p q u)) : 0 ≤ cubeBesovCircNorm Q s p q u

theorem HCPolySupport.cubeBesovDualMeanZeroSeminorm_le_note_constant_mul_cubeBesovCircNorm {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (u : Vec d → ℝ) (hs : 0 < s) (hu : MeasureTheory.MemLp u p (normalizedCubeMeasure Q)) (hp : 1 ≤ p) (hpTop : p ≠ ⊤) (hpConjTop : cubeBesovConjExponent p ≠ ⊤) (hq : 1 ≤ q) : cubeBesovDualMeanZeroSeminorm Q s p q u ≤ 3 ^ (↑d + s) * cubeBesovCircNorm Q s p q u

theorem HCPolySupport.cubeBesovDualFullNorm_le_note_constant_mul_cubeBesovCircNorm {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (u : Vec d → ℝ) (hs : 0 < s) (hu : MeasureTheory.MemLp u p (normalizedCubeMeasure Q)) (hp : 1 ≤ p) (hpTop : p ≠ ⊤) (hpConjTop : cubeBesovConjExponent p ≠ ⊤) (hq : 1 ≤ q) : cubeBesovDualFullNorm Q s p q u ≤ 3 ^ (↑d + s) * cubeBesovCircNorm Q s p q u

The full negative Besov dual norm is controlled by the negative circ norm alone. This is the sharp average bookkeeping needed in the Caccioppoli single-cube estimate: the depth-zero circ term already carries the cubeBesovScaleWeight (-s) average contribution, so no extra positive Besov average tail is needed.

theorem HCPolySupport.cubeBesovDualFullNorm_le_note_rhs {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (u : Vec d → ℝ) (hs : 0 < s) (hu : MeasureTheory.MemLp u p (normalizedCubeMeasure Q)) (hp : 1 ≤ p) (hpTop : p ≠ ⊤) (hpConjTop : cubeBesovConjExponent p ≠ ⊤) (hq : 1 ≤ q) : cubeBesovDualFullNorm Q s p q u ≤ 3 ^ (↑d + s) * cubeBesovCircNorm Q s p q u + cubeBesovScaleWeight s Q * ‖cubeAverage Q u‖