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

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

theorem HCPolySupport.cubeBesovPairing_comm {d : ℕ} (Q : TriadicCube d) (f g : Vec d → ℝ) : cubeBesovPairing Q f g = cubeBesovPairing Q g f

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

@[simp]

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

theorem HCPolySupport.abs_cubeBesovPairing_const_left_le_of_dual_test {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (c : ℝ) (g : Vec d → ℝ) (hg : CubeBesovDualTest Q s p q N g) : |cubeBesovPairing Q (fun (x : Vec d) => c) g| ≤ cubeBesovScaleWeight (-s) Q * ‖c‖

theorem HCPolySupport.cubeBesovPairing_zero_left {d : ℕ} (Q : TriadicCube d) (g : Vec d → ℝ) : cubeBesovPairing Q (fun (x : Vec d) => 0) g = 0

theorem HCPolySupport.cubeBesovPairing_zero_right {d : ℕ} (Q : TriadicCube d) (f : Vec d → ℝ) : (cubeBesovPairing Q f fun (x : Vec d) => 0) = 0

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

@[simp]

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

theorem HCPolySupport.cubeBesovDualPartialNormValueSet_nonneg {d : ℕ} {Q : TriadicCube d} {s : ℝ} {p q : ENNReal} {N : ℕ} {f : Vec d → ℝ} {r : ℝ} (hr : r ∈ cubeBesovDualPartialNormValueSet Q s p q N f) : 0 ≤ r

theorem HCPolySupport.cubeBesovDualPartialSeminormValueSet_nonneg {d : ℕ} {Q : TriadicCube d} {s : ℝ} {p q : ENNReal} {N : ℕ} {f : Vec d → ℝ} {r : ℝ} (hr : r ∈ cubeBesovDualPartialSeminormValueSet Q s p q N f) : 0 ≤ r

@[simp]

theorem HCPolySupport.cubeBesovDualTestNorm_zero {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (hp0 : cubeBesovConjExponent p ≠ 0) (hpTop : cubeBesovConjExponent p ≠ ⊤) : (cubeBesovDualTestNorm Q s p q N fun (x : Vec d) => 0) = 0

@[simp]

theorem HCPolySupport.cubeBesovDualTestSeminorm_zero {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (hp0 : cubeBesovConjExponent p ≠ 0) (hpTop : cubeBesovConjExponent p ≠ ⊤) : (cubeBesovDualTestSeminorm Q s p q N fun (x : Vec d) => 0) = 0

theorem HCPolySupport.cubeBesovDualTest_zero {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (hp0 : cubeBesovConjExponent p ≠ 0) (hpTop : cubeBesovConjExponent p ≠ ⊤) : CubeBesovDualTest Q s p q N fun (x : Vec d) => 0

theorem HCPolySupport.cubeBesovDualMeanZeroTest_zero {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (hp0 : cubeBesovConjExponent p ≠ 0) (hpTop : cubeBesovConjExponent p ≠ ⊤) : CubeBesovDualMeanZeroTest Q s p q N fun (x : Vec d) => 0

theorem HCPolySupport.zero_mem_cubeBesovDualPartialNormValueSet {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (f : Vec d → ℝ) (hp0 : cubeBesovConjExponent p ≠ 0) (hpTop : cubeBesovConjExponent p ≠ ⊤) : 0 ∈ cubeBesovDualPartialNormValueSet Q s p q N f

theorem HCPolySupport.zero_mem_cubeBesovDualPartialSeminormValueSet {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (f : Vec d → ℝ) (hp0 : cubeBesovConjExponent p ≠ 0) (hpTop : cubeBesovConjExponent p ≠ ⊤) : 0 ∈ cubeBesovDualPartialSeminormValueSet Q s p q N f

theorem HCPolySupport.cubeBesovDualPartialNormValueSet_nonempty {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (f : Vec d → ℝ) (hp0 : cubeBesovConjExponent p ≠ 0) (hpTop : cubeBesovConjExponent p ≠ ⊤) : (cubeBesovDualPartialNormValueSet Q s p q N f).Nonempty

theorem HCPolySupport.cubeBesovDualPartialSeminormValueSet_nonempty {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (f : Vec d → ℝ) (hp0 : cubeBesovConjExponent p ≠ 0) (hpTop : cubeBesovConjExponent p ≠ ⊤) : (cubeBesovDualPartialSeminormValueSet Q s p q N f).Nonempty

theorem HCPolySupport.cubeBesovDualPartialNorm_nonneg_of_bddAbove {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (f : Vec d → ℝ) (hp0 : cubeBesovConjExponent p ≠ 0) (hpTop : cubeBesovConjExponent p ≠ ⊤) (hBdd : BddAbove (cubeBesovDualPartialNormValueSet Q s p q N f)) : 0 ≤ cubeBesovDualPartialNorm Q s p q N f

theorem HCPolySupport.cubeBesovDualPartialSeminorm_nonneg_of_bddAbove {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (f : Vec d → ℝ) (hp0 : cubeBesovConjExponent p ≠ 0) (hpTop : cubeBesovConjExponent p ≠ ⊤) (hBdd : BddAbove (cubeBesovDualPartialSeminormValueSet Q s p q N f)) : 0 ≤ cubeBesovDualPartialSeminorm Q s p q N f

theorem HCPolySupport.cubeBesovDualPartialNormValueSet_const_bddAbove {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (c : ℝ) : BddAbove (cubeBesovDualPartialNormValueSet Q s p q N fun (x : Vec d) => c)

theorem HCPolySupport.cubeBesovDualPartialNorm_const_le {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (c : ℝ) (hp0 : cubeBesovConjExponent p ≠ 0) (hpTop : cubeBesovConjExponent p ≠ ⊤) : (cubeBesovDualPartialNorm Q s p q N fun (x : Vec d) => c) ≤ cubeBesovScaleWeight (-s) Q * ‖c‖

theorem HCPolySupport.cubeBesovDualTest_const_scaleWeight_neg {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (hp0 : cubeBesovConjExponent p ≠ 0) (hpTop : cubeBesovConjExponent p ≠ ⊤) : CubeBesovDualTest Q s p q N fun (x : Vec d) => cubeBesovScaleWeight (-s) Q

@[simp]

theorem HCPolySupport.cubeBesovDualPartialNorm_const {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (c : ℝ) (hp0 : cubeBesovConjExponent p ≠ 0) (hpTop : cubeBesovConjExponent p ≠ ⊤) : (cubeBesovDualPartialNorm Q s p q N fun (x : Vec d) => c) = cubeBesovScaleWeight (-s) Q * ‖c‖

@[simp]

theorem HCPolySupport.cubeBesovDualPartialSeminormValueSet_const {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (c : ℝ) (hp0 : cubeBesovConjExponent p ≠ 0) (hpTop : cubeBesovConjExponent p ≠ ⊤) : (cubeBesovDualPartialSeminormValueSet Q s p q N fun (x : Vec d) => c) = {0}

@[simp]

theorem HCPolySupport.cubeBesovDualPartialSeminorm_const {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (c : ℝ) (hp0 : cubeBesovConjExponent p ≠ 0) (hpTop : cubeBesovConjExponent p ≠ ⊤) : (cubeBesovDualPartialSeminorm Q s p q N fun (x : Vec d) => c) = 0

@[simp]

theorem HCPolySupport.cubeBesovDualPartialNormValueSet_zero {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (hp0 : cubeBesovConjExponent p ≠ 0) (hpTop : cubeBesovConjExponent p ≠ ⊤) : (cubeBesovDualPartialNormValueSet Q s p q N fun (x : Vec d) => 0) = {0}

theorem HCPolySupport.cubeBesovDualPartialSeminormValueSet_zero {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (hp0 : cubeBesovConjExponent p ≠ 0) (hpTop : cubeBesovConjExponent p ≠ ⊤) : (cubeBesovDualPartialSeminormValueSet Q s p q N fun (x : Vec d) => 0) = {0}

theorem HCPolySupport.cubeBesovDualPartialNorm_zero {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (hp0 : cubeBesovConjExponent p ≠ 0) (hpTop : cubeBesovConjExponent p ≠ ⊤) : (cubeBesovDualPartialNorm Q s p q N fun (x : Vec d) => 0) = 0

theorem HCPolySupport.cubeBesovDualPartialSeminorm_zero {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (hp0 : cubeBesovConjExponent p ≠ 0) (hpTop : cubeBesovConjExponent p ≠ ⊤) : (cubeBesovDualPartialSeminorm Q s p q N fun (x : Vec d) => 0) = 0