Coarse-graining support: Support.Book.Ch01.Theorems.PositiveBesovLocalize

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

Legacy finite positive Besov localization

This file records bounded scalar q = 2 localization helpers for the legacy disjoint, finite-truncation/real-sSup compatibility lane. They are not statements about the manuscript's exact overlapping ENNReal definitions. The unscaled full finite norm contains a cube-average term, so its unscaled localization statement is stated for the finite seminorm part. The scaled form controls the full finite norm by the parent positiveBesovPartialNormTwo.

theorem HCPolySupport.Book.Ch01.Legacy.positiveBesovPartialSeminormTwo_nonneg {d : ℕ} (Q : Cube d) (s : ℝ) (N : ℕ) (u : Vec d → ℝ) : 0 ≤ positiveBesovPartialSeminormTwo Q s N u

theorem HCPolySupport.Book.Ch01.Legacy.positiveBesovPartialSeminormTwo_le_succ {d : ℕ} (Q : Cube d) (s : ℝ) (u : Vec d → ℝ) (N : ℕ) : positiveBesovPartialSeminormTwo Q s N u ≤ positiveBesovPartialSeminormTwo Q s (N + 1) u

theorem HCPolySupport.Book.Ch01.Legacy.descendantsAverage_sq_cubeBesovPartialSeminormTwo_le {d : ℕ} (Q : Cube d) (s : ℝ) (u : Vec d → ℝ) (j N : ℕ) : (descendantsAverage Q j fun (R : TriadicCube d) => cubeBesovPartialSeminorm R s 2 2 N u ^ 2) ≤ cubeBesovPartialSeminorm Q s 2 2 (j + N) u ^ 2

Legacy disjoint finite scalar q = 2 positive Besov seminorms localize over descendants.

theorem HCPolySupport.Book.Ch01.Legacy.descendantsAverage_sq_positiveBesovPartialSeminormTwo_le {d : ℕ} (Q : Cube d) (s : ℝ) (u : Vec d → ℝ) (j N : ℕ) : (descendantsAverage Q j fun (R : TriadicCube d) => positiveBesovPartialSeminormTwo R s N u ^ 2) ≤ positiveBesovPartialSeminormTwo Q s (j + N) u ^ 2

theorem HCPolySupport.Book.Ch01.Legacy.positiveBesovPartialSeminormTwo_le_positiveBesovPartialNormTwo {d : ℕ} (Q : Cube d) (s : ℝ) (N : ℕ) (u : Vec d → ℝ) : positiveBesovPartialSeminormTwo Q s N u ≤ positiveBesovPartialNormTwo Q s N u

theorem HCPolySupport.Book.Ch01.Legacy.positiveBesovPartialNormTwo_nonneg {d : ℕ} (Q : Cube d) (s : ℝ) (N : ℕ) (u : Vec d → ℝ) : 0 ≤ positiveBesovPartialNormTwo Q s N u

theorem HCPolySupport.Book.Ch01.Legacy.positiveBesovPartialNormTwo_le_succ {d : ℕ} (Q : Cube d) (s : ℝ) (u : Vec d → ℝ) (N : ℕ) : positiveBesovPartialNormTwo Q s N u ≤ positiveBesovPartialNormTwo Q s (N + 1) u

theorem HCPolySupport.Book.Ch01.Legacy.descendantsAverage_sq_cubeBesovPartialSeminormTwo_le_positiveBesovPartialNormTwo {d : ℕ} (Q : Cube d) (s : ℝ) (u : Vec d → ℝ) (j N : ℕ) : (descendantsAverage Q j fun (R : TriadicCube d) => cubeBesovPartialSeminorm R s 2 2 N u ^ 2) ≤ positiveBesovPartialNormTwo Q s (j + N) u ^ 2

Legacy compatibility form: the localized finite scalar seminorm is bounded by the parent finite positive Besov norm. The corresponding unscaled statement with local positiveBesovPartialNormTwo on the left is false for this normalization; see the scaled full-norm localization below.

theorem HCPolySupport.Book.Ch01.Legacy.descendantsAverage_sq_positiveBesovPartialSeminormTwo_le_positiveBesovPartialNormTwo {d : ℕ} (Q : Cube d) (s : ℝ) (u : Vec d → ℝ) (j N : ℕ) : (descendantsAverage Q j fun (R : TriadicCube d) => positiveBesovPartialSeminormTwo R s N u ^ 2) ≤ positiveBesovPartialNormTwo Q s (j + N) u ^ 2

theorem HCPolySupport.Book.Ch01.Legacy.descendantsAverage_sq_scaled_positiveBesovMeanTerm_le_weighted_l2 {d : ℕ} (Q : Cube d) (s : ℝ) (u : Vec d → ℝ) (j : ℕ) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) : (descendantsAverage Q j fun (R : TriadicCube d) => (Real.rpow 3 (-(s * ↑j)) * (cubeBesovScaleWeight s R * ‖cubeAverage R u‖)) ^ 2) ≤ (cubeBesovScaleWeight s Q * cubeLpNorm Q 2 u) ^ 2

In the legacy lane, the scaled descendant cube-average term is controlled by the parent weighted L² norm.

theorem HCPolySupport.Book.Ch01.Legacy.descendantsAverage_sq_scaled_positiveBesovMeanTerm_le_positiveBesovPartialNormTwo {d : ℕ} (Q : Cube d) (s : ℝ) (u : Vec d → ℝ) (j M : ℕ) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) : (descendantsAverage Q j fun (R : TriadicCube d) => (Real.rpow 3 (-(s * ↑j)) * (cubeBesovScaleWeight s R * ‖cubeAverage R u‖)) ^ 2) ≤ positiveBesovPartialNormTwo Q s M u ^ 2

theorem HCPolySupport.Book.Ch01.Legacy.descendantsAverage_sq_scaled_positiveBesovPartialSeminormTwo_le_positiveBesovPartialNormTwo {d : ℕ} (Q : Cube d) (s : ℝ) (u : Vec d → ℝ) (j N : ℕ) (hs : 0 ≤ s) : (descendantsAverage Q j fun (R : TriadicCube d) => (Real.rpow 3 (-(s * ↑j)) * positiveBesovPartialSeminormTwo R s N u) ^ 2) ≤ positiveBesovPartialNormTwo Q s (j + N) u ^ 2

theorem HCPolySupport.Book.Ch01.Legacy.descendantsAverage_sq_scaled_positiveBesovPartialNormTwo_le {d : ℕ} (Q : Cube d) (s : ℝ) (u : Vec d → ℝ) (j N : ℕ) (hs : 0 ≤ s) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) : (descendantsAverage Q j fun (R : TriadicCube d) => (Real.rpow 3 (-(s * ↑j)) * positiveBesovPartialNormTwo R s N u) ^ 2) ≤ (2 * positiveBesovPartialNormTwo Q s (j + N) u) ^ 2

Legacy scaled finite positive q = 2 Besov norms localize over descendants.

theorem HCPolySupport.Book.Ch01.Legacy.positiveBesovPartialNormTwo_le_normTwo_of_bddAbove {d : ℕ} (Q : Cube d) (s : ℝ) (u : Vec d → ℝ) (hBdd : BddAbove (Set.range fun (N : ℕ) => positiveBesovPartialNormTwo Q s (N + 1) u)) (N : ℕ) : positiveBesovPartialNormTwo Q s N u ≤ positiveBesovNormTwo Q s u

theorem HCPolySupport.Book.Ch01.Legacy.positiveBesovNormTwo_nonneg_of_bddAbove {d : ℕ} (Q : Cube d) (s : ℝ) (u : Vec d → ℝ) (hBdd : BddAbove (Set.range fun (N : ℕ) => positiveBesovPartialNormTwo Q s (N + 1) u)) : 0 ≤ positiveBesovNormTwo Q s u

theorem HCPolySupport.Book.Ch01.Legacy.tendsto_positiveBesovPartialNormTwo_succ_atTop {d : ℕ} (Q : Cube d) (s : ℝ) (u : Vec d → ℝ) (hBdd : BddAbove (Set.range fun (N : ℕ) => positiveBesovPartialNormTwo Q s (N + 1) u)) : Filter.Tendsto (fun (N : ℕ) => positiveBesovPartialNormTwo Q s (N + 1) u) Filter.atTop (nhds (positiveBesovNormTwo Q s u))

theorem HCPolySupport.Book.Ch01.Legacy.tendsto_descendantsAverage_sq_scaled_positiveBesovPartialNormTwo_succ_atTop {d : ℕ} (Q : Cube d) (s : ℝ) (u : Vec d → ℝ) (j : ℕ) (c : ℝ) (hLocalBdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => positiveBesovPartialNormTwo R s (N + 1) u)) : Filter.Tendsto (fun (N : ℕ) => descendantsAverage Q j fun (R : TriadicCube d) => (c * positiveBesovPartialNormTwo R s (N + 1) u) ^ 2) Filter.atTop (nhds (descendantsAverage Q j fun (R : TriadicCube d) => (c * positiveBesovNormTwo R s u) ^ 2))

theorem HCPolySupport.Book.Ch01.Legacy.descendantsAverage_sq_scaled_positiveBesovNormTwo_le {d : ℕ} (Q : Cube d) (s : ℝ) (u : Vec d → ℝ) (j : ℕ) (hs : 0 ≤ s) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hParentBdd : BddAbove (Set.range fun (N : ℕ) => positiveBesovPartialNormTwo Q s (N + 1) u)) (hLocalBdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => positiveBesovPartialNormTwo R s (N + 1) u)) : (descendantsAverage Q j fun (R : TriadicCube d) => (Real.rpow 3 (-(s * ↑j)) * positiveBesovNormTwo R s u) ^ 2) ≤ (2 * positiveBesovNormTwo Q s u) ^ 2

In the legacy real-sSup lane, infinite-depth scaled positive q = 2 Besov norms localize over descendants, provided the parent and local sSups are bounded above.

theorem HCPolySupport.Book.Ch01.Legacy.memLp_normalizedCubeMeasure_of_memScalarL2_cubeSet {d : ℕ} (Q : Cube d) {u : Vec d → ℝ} (hu : MemScalarL2 (cubeSet Q) u) : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)

A scalar L² function on a cube is in L² for the normalized cube measure.

theorem HCPolySupport.Book.Ch01.Legacy.positiveBesovLocalize_cube {d : ℕ} (Q : Cube d) (s : ℝ) (u : Vec d → ℝ) (j : ℕ) (hs : 0 < s) (hu : MemScalarL2 (cubeSet Q) u) (hParentBdd : BddAbove (Set.range fun (N : ℕ) => positiveBesovPartialNormTwo Q s (N + 1) u)) (hLocalBdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => positiveBesovPartialNormTwo R s (N + 1) u)) : √(descendantsAverage Q j fun (R : TriadicCube d) => (Real.rpow 3 (-(s * ↑j)) * positiveBesovNormTwo R s u) ^ 2) ≤ positiveBesovLocalizeConstant d * positiveBesovNormTwo Q s u

Cube-general form of the legacy positive Besov localization lemma.

theorem HCPolySupport.Book.Ch01.Legacy.positiveBesovLocalize {d : ℕ} {s : ℝ} {m n : ℤ} (_hd : 1 ≤ d) (hs_pos : 0 < s) (_hs_lt_one : s < 1) (hnm : n ≤ m) (u : Vec d → ℝ) (hu : MemScalarL2 (cubeSet (originCube d m)) u) (hParentBdd : BddAbove (Set.range fun (N : ℕ) => positiveBesovPartialNormTwo (originCube d m) s N u)) (hLocalBdd : ∀ R ∈ descendantsAtDepth (originCube d m) (m - n).toNat, BddAbove (Set.range fun (N : ℕ) => positiveBesovPartialNormTwo R s N u)) : √(descendantsAverage (originCube d m) (m - n).toNat fun (R : TriadicCube d) => (Real.rpow 3 (s * ↑(n - m)) * positiveBesovNormTwo R s u) ^ 2) ≤ positiveBesovLocalizeConstant d * positiveBesovNormTwo (originCube d m) s u

Legacy compatibility form associated with manuscript Lemma l.Besov.positive.localize.function.spaces. The normalized legacy positive Besov norm of u on the origin cube ⌈_m controls the geometrically weighted root-mean-square of normalized legacy positive Besov norms on each triadic descendant z + ⌈_n for n ≤ m.