Coarse-graining support: Support.Deterministic.CoarsePoincareRHS.TerminalBounds #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.memLp_normalizedCubeMeasure_of_memVectorL2_cubeSet
{d : ℕ}
(Q : TriadicCube d)
{f : Vec d → Vec d}
(hf : MemVectorL2 (cubeSet Q) f)
:
theorem
HCPolySupport.memVectorL2_cubeSet_of_memLp_normalizedCubeMeasure
{d : ℕ}
(Q : TriadicCube d)
{f : Vec d → Vec d}
(hf : MeasureTheory.MemLp f 2 (normalizedCubeMeasure Q))
:
MemVectorL2 (cubeSet Q) f
theorem
HCPolySupport.cubeBesovNegativeVectorDepthAverage_eq_sum_components
{d : ℕ}
(Q : TriadicCube d)
(u : Vec d → Vec d)
(j : ℕ)
:
cubeBesovNegativeVectorDepthAverage Q u j = ∑ i : Fin d, cubeBesovCircDepthAverage Q 2 (fun (x : Vec d) => u x i) j
theorem
HCPolySupport.cubeBesovNegativeVectorDepthAverage_le_cubeAverage_vecNormSq_of_memLp
{d : ℕ}
(Q : TriadicCube d)
(u : Vec d → Vec d)
(j : ℕ)
(hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q))
:
theorem
HCPolySupport.sq_cubeBesovNegativeVectorPartialSeminormTwo_le_l2Average_of_memLp
{d : ℕ}
(Q : TriadicCube d)
{s : ℝ}
(hs : 0 < s)
(u : Vec d → Vec d)
(N : ℕ)
(hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q))
:
cubeBesovNegativeVectorPartialSeminormTwo Q s N u ^ 2 ≤ (geometricDiscount s 2)⁻¹ * cubeAverage Q fun (x : Vec d) => vecNormSq (u x)
theorem
HCPolySupport.sq_cubeBesovNegativeVectorSeminormTwo_le_l2Average_of_memLp
{d : ℕ}
(Q : TriadicCube d)
{s : ℝ}
(hs : 0 < s)
(u : Vec d → Vec d)
(hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q))
:
cubeBesovNegativeVectorSeminormTwo Q s u ^ 2 ≤ (geometricDiscount s 2)⁻¹ * cubeAverage Q fun (x : Vec d) => vecNormSq (u x)
theorem
HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo_bddAbove_of_memLp
{d : ℕ}
(Q : TriadicCube d)
{s : ℝ}
(hs : 0 < s)
(u : Vec d → Vec d)
(hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q))
:
BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N u)
theorem
HCPolySupport.cubeBesovNegativeVectorPartialSeminorm_bddAbove_of_memLp
{d : ℕ}
(Q : TriadicCube d)
{s : ℝ}
(hs : 0 < s)
(u : Vec d → Vec d)
(hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q))
:
BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminorm Q s N u)
theorem
HCPolySupport.cubeBesovNegativeVectorSeminormTwo_nonneg_of_memLp
{d : ℕ}
(Q : TriadicCube d)
{s : ℝ}
(hs : 0 < s)
(u : Vec d → Vec d)
(hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q))
:
theorem
HCPolySupport.cubeBesovNegativeVectorSeminorm_nonneg_of_memLp
{d : ℕ}
(Q : TriadicCube d)
{s : ℝ}
(hs : 0 < s)
(u : Vec d → Vec d)
(hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q))
:
theorem
HCPolySupport.cubeBesovNegativeVectorPartialSeminorm_le_seminorm_of_memLp
{d : ℕ}
(Q : TriadicCube d)
{s : ℝ}
(hs : 0 < s)
(u : Vec d → Vec d)
(N : ℕ)
(hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q))
:
theorem
HCPolySupport.cubeBesovScaleWeight_mul_negativePartialSeminorm_le_mul_negativeSeminorm
{d : ℕ}
(Q : TriadicCube d)
{s : ℝ}
(hs : 0 < s)
(w : ℝ)
(u : Vec d → Vec d)
(N : ℕ)
(hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q))
:
cubeBesovScaleWeight w Q * cubeBesovNegativeVectorPartialSeminorm Q s N u ≤ cubeBesovScaleWeight w Q * cubeBesovNegativeVectorSeminorm Q s u
theorem
HCPolySupport.coarsePoincareRHSSn_le_l2Average_of_memLp
{d : ℕ}
(Q : TriadicCube d)
{s : ℝ}
(hs : 0 < s)
(u : Vec d → Vec d)
(n : ℕ)
(hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q))
:
coarsePoincareRHSSn Q s u n ≤ (geometricDiscount s 2)⁻¹ * cubeAverage Q fun (x : Vec d) => vecNormSq (u x)
theorem
HCPolySupport.coarsePoincareRHSSn_bddAbove_of_memLp
{d : ℕ}
(Q : TriadicCube d)
{s : ℝ}
(hs : 0 < s)
(u : Vec d → Vec d)
(hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q))
:
BddAbove (Set.range fun (n : ℕ) => coarsePoincareRHSSn Q s u n)