Coarse-graining support: Support.Book.Ch03.Theorems.EnergyRHS.Basic #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Energy RHS: Basic L2 and Besov controls #
theorem
HCPolySupport.Book.Ch03.cubeAverage_vecNormSq_le_card_mul_cubeLpNorm_two_sq
{d : ℕ}
{Q : TriadicCube d}
{F : Vec d → Vec d}
(hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q))
:
The Euclidean square average of a vector field is controlled by the L²
cube norm coming from the ambient sup norm, with the expected dimension factor.
theorem
HCPolySupport.Book.Ch03.cubeLpNorm_two_cubeFluctuationVec_le_scaleNormalizedPositiveBesovVectorSeminormTwo
{d : ℕ}
{Q : TriadicCube d}
{s : ℝ}
{F : Vec d → Vec d}
(hF : ForceBesovRegularity Q s F)
:
The depth-zero positive Besov seminorm controls the top-scale fluctuation
L² norm.
theorem
HCPolySupport.Book.Ch03.cubeLpNorm_two_le_scaleNormalizedPositiveBesovVectorNormTwo
{d : ℕ}
{Q : TriadicCube d}
{s : ℝ}
{F : Vec d → Vec d}
(hF : ForceBesovRegularity Q s F)
:
The full public positive Besov norm controls the top-scale cube L² norm.
theorem
HCPolySupport.Book.Ch03.sqrt_cubeAverage_vecNormSq_le_sqrt_card_mul_scaleNormalizedPositiveBesovVectorNormTwo
{d : ℕ}
{Q : TriadicCube d}
{s : ℝ}
{F : Vec d → Vec d}
(hF : ForceBesovRegularity Q s F)
:
√(cubeAverage Q fun (x : Vec d) => vecNormSq (F x)) ≤ √↑(Fintype.card (Fin d)) * scaleNormalizedPositiveBesovVectorNormTwo Q s F
Euclidean cube L² size is controlled by the public positive Besov norm,
with only the ambient dimension factor coming from the sup-norm model of
Vec d.