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

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

theorem HCPolySupport.cubeBesovDualPartialNorm_projection_le_max_mul_cubeBesovCircPartialNorm {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (u : Vec d → ℝ) (huInt : MeasureTheory.IntegrableOn u (cubeSet Q) MeasureTheory.volume) (hp : 1 ≤ p) (hpTop : p ≠ ⊤) (hpConjTop : cubeBesovConjExponent p ≠ ⊤) (hq : 1 ≤ q) (hqTop : q ≠ ⊤) (hqConjTop : cubeBesovConjExponent q ≠ ⊤) : cubeBesovDualPartialNorm Q s p q N (cubeProjection Q (N + 1) u) ≤ max 1 (3 ^ s) * cubeBesovCircPartialNorm Q s p q (N + 1) u

theorem HCPolySupport.abs_cubeBesovPairing_projection_le_max_mul_cubeBesovCircPartialNorm_of_dual_test {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (u g : Vec d → ℝ) (huInt : MeasureTheory.IntegrableOn u (cubeSet Q) MeasureTheory.volume) (hp : 1 ≤ p) (hpTop : p ≠ ⊤) (hpConjTop : cubeBesovConjExponent p ≠ ⊤) (hq : 1 ≤ q) (hqTop : q ≠ ⊤) (hqConjTop : cubeBesovConjExponent q ≠ ⊤) (hg : CubeBesovDualTest Q s p q N g) : |cubeBesovPairing Q (cubeProjection Q (N + 1) u) g| ≤ max 1 (3 ^ s) * cubeBesovCircPartialNorm Q s p q (N + 1) u

theorem HCPolySupport.abs_cubeBesovPairing_projection_le_max_mul_cubeBesovCircNormEntry_of_dual_test {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (u g : Vec d → ℝ) (huInt : MeasureTheory.IntegrableOn u (cubeSet Q) MeasureTheory.volume) (hp : 1 ≤ p) (hpTop : p ≠ ⊤) (hpConjTop : cubeBesovConjExponent p ≠ ⊤) (hq : 1 ≤ q) (hg : CubeBesovDualTest Q s p q N g) : |cubeBesovPairing Q (cubeProjection Q (N + 1) u) g| ≤ max 1 (3 ^ s) * cubeBesovCircNormEntry Q s p q N u

theorem HCPolySupport.cubeBesovDualPartialSeminorm_projection_le_max_mul_cubeBesovCircPartialNorm {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (u : Vec d → ℝ) (huInt : MeasureTheory.IntegrableOn u (cubeSet Q) MeasureTheory.volume) (hp : 1 ≤ p) (hpTop : p ≠ ⊤) (hpConjTop : cubeBesovConjExponent p ≠ ⊤) (hq : 1 ≤ q) (hqTop : q ≠ ⊤) (hqConjTop : cubeBesovConjExponent q ≠ ⊤) : cubeBesovDualPartialSeminorm Q s p q N (cubeProjection Q (N + 1) u) ≤ max 1 (3 ^ s) * cubeBesovCircPartialNorm Q s p q (N + 1) u