Coarse-graining support: Support.Deterministic.WeakNormInterfaces.Localization

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

Localization for the concrete vector negative q = 2 seminorm

This file proves the finite-energy localization estimate for the concrete negative Besov seminorm used in the Ch3.3 Hodge-projection input. The full seminorm is an sSup of finite partial seminorms, so the final full-seminorm statement assumes the local partial seminorms are bounded above; this is the same sSup well-posedness hypothesis used throughout the deterministic Ch3 files when a finite partial norm is compared to the full norm.

theorem HCPolySupport.descendantsAverage_sq_le_descendantsAverage_sq {d : ℕ} (Q : TriadicCube d) (j : ℕ) (F : TriadicCube d → ℝ) : descendantsAverage Q j F ^ 2 ≤ descendantsAverage Q j fun (R : TriadicCube d) => F R ^ 2

theorem HCPolySupport.vecNormSq_cubeAverageVec_le_descendantsAverage_vecNormSq_cubeAverageVec_one_of_memLp {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) : vecNormSq (cubeAverageVec Q u) ≤ descendantsAverage Q 1 fun (R : TriadicCube d) => vecNormSq (cubeAverageVec R u)

theorem HCPolySupport.sq_cubeBesovNegativeVectorPartialSeminormTwo_le_descendantsAverage_one_same_depth_of_memLp {d : ℕ} (Q : TriadicCube d) {s : ℝ} (_hs : 0 < s) (u : Vec d → Vec d) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (N : ℕ) : cubeBesovNegativeVectorPartialSeminormTwo Q s N u ^ 2 ≤ descendantsAverage Q 1 fun (R : TriadicCube d) => cubeBesovNegativeVectorPartialSeminormTwo R s N u ^ 2

theorem HCPolySupport.sq_cubeBesovNegativeVectorPartialSeminormTwo_le_descendantsAverage_same_depth_of_memLp {d : ℕ} (Q : TriadicCube d) {s : ℝ} (hs : 0 < s) (u : Vec d → Vec d) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (j N : ℕ) : cubeBesovNegativeVectorPartialSeminormTwo Q s N u ^ 2 ≤ descendantsAverage Q j fun (R : TriadicCube d) => cubeBesovNegativeVectorPartialSeminormTwo R s N u ^ 2

theorem HCPolySupport.negativeVectorBesov_le_descendantMeanSquare_of_bounded {d : ℕ} (Q : TriadicCube d) {s : ℝ} (hs : 0 < s) (u : Vec d → Vec d) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (j : ℕ) (hBdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N u)) : cubeBesovNegativeVectorSeminormTwo Q s u ≤ √(descendantsAverage Q j fun (R : TriadicCube d) => cubeBesovNegativeVectorSeminormTwo R s u ^ 2)