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

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

theorem HCPolySupport.cubeAverage_const_mul {d : ℕ} (Q : TriadicCube d) (c : ℝ) (f : Vec d → ℝ) : (cubeAverage Q fun (x : Vec d) => c * f x) = c * cubeAverage Q f

theorem HCPolySupport.cubeFluctuation_const_mul {d : ℕ} (Q : TriadicCube d) (c : ℝ) (f : Vec d → ℝ) : (cubeFluctuation Q fun (x : Vec d) => c * f x) = fun (x : Vec d) => c * cubeFluctuation Q f x

theorem HCPolySupport.cubeLpNorm_const_mul {d : ℕ} (Q : TriadicCube d) (p : ENNReal) (c : ℝ) (f : Vec d → ℝ) : (cubeLpNorm Q p fun (x : Vec d) => c * f x) = ‖c‖ * cubeLpNorm Q p f

theorem HCPolySupport.descendantsAverage_mul_left_local {d : ℕ} (Q : TriadicCube d) (j : ℕ) (c : ℝ) (F : TriadicCube d → ℝ) : (descendantsAverage Q j fun (R : TriadicCube d) => c * F R) = c * descendantsAverage Q j F

theorem HCPolySupport.cubeBesovOscillation_two_const_mul {d : ℕ} (Q : TriadicCube d) (c : ℝ) (u : Vec d → ℝ) : (cubeBesovOscillation Q 2 fun (x : Vec d) => c * u x) = ‖c‖ * cubeBesovOscillation Q 2 u

theorem HCPolySupport.cubeBesovDepthAverage_two_const_mul {d : ℕ} (Q : TriadicCube d) (c : ℝ) (u : Vec d → ℝ) (j : ℕ) : cubeBesovDepthAverage Q 2 (fun (x : Vec d) => c * u x) j = ‖c‖ ^ 2 * cubeBesovDepthAverage Q 2 u j

theorem HCPolySupport.cubeBesovDepthSeminorm_two_const_mul {d : ℕ} (Q : TriadicCube d) (s c : ℝ) (u : Vec d → ℝ) (j : ℕ) : cubeBesovDepthSeminorm Q s 2 (fun (x : Vec d) => c * u x) j = ‖c‖ * cubeBesovDepthSeminorm Q s 2 u j

theorem HCPolySupport.cubeBesovPartialSeminormTop_two_const_mul_le {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (c : ℝ) (u : Vec d → ℝ) : (cubeBesovPartialSeminormTop Q s 2 N fun (x : Vec d) => c * u x) ≤ ‖c‖ * cubeBesovPartialSeminormTop Q s 2 N u

theorem HCPolySupport.cubeBesovPartialNormTop_two_const_mul_le {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (c : ℝ) (u : Vec d → ℝ) : (cubeBesovPartialNormTop Q s 2 N fun (x : Vec d) => c * u x) ≤ ‖c‖ * cubeBesovPartialNormTop Q s 2 N u

theorem HCPolySupport.cubeBesovPartialSeminorm_two_const_mul_le {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (c : ℝ) (u : Vec d → ℝ) : (cubeBesovPartialSeminorm Q s 2 2 N fun (x : Vec d) => c * u x) ≤ ‖c‖ * cubeBesovPartialSeminorm Q s 2 2 N u

theorem HCPolySupport.cubeBesovPartialNorm_two_const_mul_le {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (c : ℝ) (u : Vec d → ℝ) : (cubeBesovPartialNorm Q s 2 2 N fun (x : Vec d) => c * u x) ≤ ‖c‖ * cubeBesovPartialNorm Q s 2 2 N u

theorem HCPolySupport.cubeBesovDualTestNorm_two_one_const_mul_le {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (c : ℝ) (g : Vec d → ℝ) : (cubeBesovDualTestNorm Q s 2 1 N fun (x : Vec d) => c * g x) ≤ ‖c‖ * cubeBesovDualTestNorm Q s 2 1 N g

theorem HCPolySupport.cubeBesovDualTestNorm_two_two_const_mul_le {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (c : ℝ) (g : Vec d → ℝ) : (cubeBesovDualTestNorm Q s 2 2 N fun (x : Vec d) => c * g x) ≤ ‖c‖ * cubeBesovDualTestNorm Q s 2 2 N g

theorem HCPolySupport.cubeBesovDualLocalMemLpGlobal_two_const_mul {d : ℕ} {Q : TriadicCube d} {g : Vec d → ℝ} (c : ℝ) (hg : CubeBesovDualLocalMemLpGlobal Q 2 g) : CubeBesovDualLocalMemLpGlobal Q 2 fun (x : Vec d) => c * g x

theorem HCPolySupport.cubeBesovPairing_const_mul_right {d : ℕ} (Q : TriadicCube d) (f g : Vec d → ℝ) (c : ℝ) : (cubeBesovPairing Q f fun (x : Vec d) => c * g x) = c * cubeBesovPairing Q f g

theorem HCPolySupport.cubeBesovDualFullNormValueSet_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 (cubeBesovDualFullNormValueSet Q s p q u)

theorem HCPolySupport.abs_cubeBesovPairing_le_cubeBesovDualFullNorm_of_full_test_of_memLp {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (u g : Vec d → ℝ) (hs : 0 < s) (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| ≤ cubeBesovDualFullNorm Q s p q u

theorem HCPolySupport.cubeBesovDualFullTest_two_one_of_uniform_bound {d : ℕ} (Q : TriadicCube d) (s : ℝ) (g : Vec d → ℝ) {B : ℝ} (hB : 0 < B) (hnorm : ∀ (N : ℕ), cubeBesovDualTestNorm Q s 2 1 N g ≤ B) (hmem : CubeBesovDualLocalMemLpGlobal Q 2 g) : CubeBesovDualFullTest Q s 2 1 fun (x : Vec d) => B⁻¹ * g x

theorem HCPolySupport.cubeBesovDualFullTest_two_two_of_uniform_bound {d : ℕ} (Q : TriadicCube d) (s : ℝ) (g : Vec d → ℝ) {B : ℝ} (hB : 0 < B) (hnorm : ∀ (N : ℕ), cubeBesovDualTestNorm Q s 2 2 N g ≤ B) (hmem : CubeBesovDualLocalMemLpGlobal Q 2 g) : CubeBesovDualFullTest Q s 2 2 fun (x : Vec d) => B⁻¹ * g x

theorem HCPolySupport.abs_cubeBesovPairing_le_mul_cubeBesovDualFullNorm_of_uniform_bound_two_one {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u g : Vec d → ℝ) {B : ℝ} (hs : 0 < s) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hB : 0 < B) (hnorm : ∀ (N : ℕ), cubeBesovDualTestNorm Q s 2 1 N g ≤ B) (hmem : CubeBesovDualLocalMemLpGlobal Q 2 g) : |cubeBesovPairing Q u g| ≤ cubeBesovDualFullNorm Q s 2 1 u * B

theorem HCPolySupport.abs_cubeBesovPairing_le_mul_cubeBesovDualFullNorm_of_uniform_bound_two_two {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u g : Vec d → ℝ) {B : ℝ} (hs : 0 < s) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hB : 0 < B) (hnorm : ∀ (N : ℕ), cubeBesovDualTestNorm Q s 2 2 N g ≤ B) (hmem : CubeBesovDualLocalMemLpGlobal Q 2 g) : |cubeBesovPairing Q u g| ≤ cubeBesovDualFullNorm Q s 2 2 u * B

theorem HCPolySupport.abs_cubeBesovPairing_le_note_rhs_mul_of_uniform_bound_two_one {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u g : Vec d → ℝ) {B : ℝ} (hs : 0 < s) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hB : 0 < B) (hnorm : ∀ (N : ℕ), cubeBesovDualTestNorm Q s 2 1 N g ≤ B) (hmem : CubeBesovDualLocalMemLpGlobal Q 2 g) : |cubeBesovPairing Q u g| ≤ (3 ^ (↑d + s) * cubeBesovCircNorm Q s 2 1 u + cubeBesovScaleWeight s Q * ‖cubeAverage Q u‖) * B

theorem HCPolySupport.abs_cubeBesovPairing_le_note_constant_mul_of_uniform_bound_two_one {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u g : Vec d → ℝ) {B : ℝ} (hs : 0 < s) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hB : 0 < B) (hnorm : ∀ (N : ℕ), cubeBesovDualTestNorm Q s 2 1 N g ≤ B) (hmem : CubeBesovDualLocalMemLpGlobal Q 2 g) : |cubeBesovPairing Q u g| ≤ 3 ^ (↑d + s) * cubeBesovCircNorm Q s 2 1 u * B

Sharp version of abs_cubeBesovPairing_le_note_rhs_mul_of_uniform_bound_two_one. The depth-zero circ term already contains the average contribution, so this matches the LaTeX negative-Besov estimate without the extra positive average tail.

theorem HCPolySupport.abs_cubeBesovPairing_le_note_constant_mul_of_uniform_bound_two_one_of_nonneg {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u g : Vec d → ℝ) {B : ℝ} (hs : 0 < s) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hB : 0 ≤ B) (hnorm : ∀ (N : ℕ), cubeBesovDualTestNorm Q s 2 1 N g ≤ B) (hmem : CubeBesovDualLocalMemLpGlobal Q 2 g) : |cubeBesovPairing Q u g| ≤ 3 ^ (↑d + s) * cubeBesovCircNorm Q s 2 1 u * B

theorem HCPolySupport.abs_cubeBesovPairing_le_note_rhs_mul_of_uniform_bound_two_one_of_nonneg {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u g : Vec d → ℝ) {B : ℝ} (hs : 0 < s) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hB : 0 ≤ B) (hnorm : ∀ (N : ℕ), cubeBesovDualTestNorm Q s 2 1 N g ≤ B) (hmem : CubeBesovDualLocalMemLpGlobal Q 2 g) : |cubeBesovPairing Q u g| ≤ (3 ^ (↑d + s) * cubeBesovCircNorm Q s 2 1 u + cubeBesovScaleWeight s Q * ‖cubeAverage Q u‖) * B

theorem HCPolySupport.abs_cubeBesovPairing_le_note_rhs_mul_of_uniform_bound_two_two {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u g : Vec d → ℝ) {B : ℝ} (hs : 0 < s) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hB : 0 < B) (hnorm : ∀ (N : ℕ), cubeBesovDualTestNorm Q s 2 2 N g ≤ B) (hmem : CubeBesovDualLocalMemLpGlobal Q 2 g) : |cubeBesovPairing Q u g| ≤ (3 ^ (↑d + s) * cubeBesovCircNorm Q s 2 2 u + cubeBesovScaleWeight s Q * ‖cubeAverage Q u‖) * B

theorem HCPolySupport.abs_cubeBesovPairing_le_note_rhs_mul_of_uniform_bound_two_two_of_nonneg {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u g : Vec d → ℝ) {B : ℝ} (hs : 0 < s) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hB : 0 ≤ B) (hnorm : ∀ (N : ℕ), cubeBesovDualTestNorm Q s 2 2 N g ≤ B) (hmem : CubeBesovDualLocalMemLpGlobal Q 2 g) : |cubeBesovPairing Q u g| ≤ (3 ^ (↑d + s) * cubeBesovCircNorm Q s 2 2 u + cubeBesovScaleWeight s Q * ‖cubeAverage Q u‖) * B