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

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

Legacy negative Besov localization scaffolding

This file records the legacy totalized/disjoint-real negative Besov localization API retained for downstream compatibility. The proof pairs a parent mean-zero dual test against the descendants, applies the local full-dual bound on each descendant, and closes with the positive Besov localization estimate for the test.

theorem HCPolySupport.Book.Ch01.Legacy.cubeBesovDualMeanZeroSeminorm_le_of_forall_meanZeroTest_pairing_le {d : ℕ} (Q : Cube d) (s : ℝ) (p q : ENNReal) (f : Vec d → ℝ) {B : ℝ} (hp0 : cubeBesovConjExponent p ≠ 0) (hpTop : cubeBesovConjExponent p ≠ ⊤) (hB : ∀ (g : Vec d → ℝ), CubeBesovDualMeanZeroTestGlobal Q s p q g → |cubeBesovPairing Q f g| ≤ B) : dualNegativeBesovSeminorm Q s p q f ≤ B

Bound the mean-zero dual negative Besov seminorm by bounding its pairing against every global mean-zero unit test.

theorem HCPolySupport.Book.Ch01.Legacy.cubeBesovPairing_eq_descendantsAverage_pairing_of_integrableOn {d : ℕ} (Q : Cube d) (j : ℕ) (f g : Vec d → ℝ) (hfg : MeasureTheory.IntegrableOn (fun (x : Vec d) => f x * g x) (cubeSet Q) MeasureTheory.volume) : cubeBesovPairing Q f g = descendantsAverage Q j fun (R : TriadicCube d) => cubeBesovPairing R f g

Split a parent cube Besov pairing into the normalized average of descendant pairings.

theorem HCPolySupport.Book.Ch01.Legacy.abs_cubeBesovPairing_le_descendantsAverage_abs_pairing_of_integrableOn {d : ℕ} (Q : Cube d) (j : ℕ) (f g : Vec d → ℝ) (hfg : MeasureTheory.IntegrableOn (fun (x : Vec d) => f x * g x) (cubeSet Q) MeasureTheory.volume) : |cubeBesovPairing Q f g| ≤ descendantsAverage Q j fun (R : TriadicCube d) => |cubeBesovPairing R f g|

Triangle-inequality form of the descendant pairing split.

theorem HCPolySupport.Book.Ch01.Legacy.cubeBesovDualLocalMemLpGlobal_restrict_to_descendant {d : ℕ} {Q R : Cube d} {j : ℕ} {p : ENNReal} {g : Vec d → ℝ} (hg : CubeBesovDualLocalMemLpGlobal Q p g) (hR : R ∈ descendantsAtDepth Q j) : CubeBesovDualLocalMemLpGlobal R p g

A global dual-test local MemLp hypothesis restricts to descendants.

theorem HCPolySupport.Book.Ch01.Legacy.abs_cubeBesovPairing_le_dualFullNorm_mul_bound {d : ℕ} (Q : Cube d) (s : ℝ) (u g : Vec d → ℝ) {B : ℝ} (hs : 0 < s) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hB : 0 ≤ B) (hnorm : ∀ (N : ℕ), cubeBesovDualTestNorm Q s 2 2 N g ≤ B) (hmem : CubeBesovDualLocalMemLpGlobal Q 2 g) : |cubeBesovPairing Q u g| ≤ cubeBesovDualFullNorm Q s 2 2 u * B

theorem HCPolySupport.Book.Ch01.Legacy.abs_cubeBesovPairing_le_dualNegativeBesovNorm_mul_positiveBesovNormTwo {d : ℕ} (Q : Cube d) (s : ℝ) (u g : Vec d → ℝ) (hs : 0 < s) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hBdd : BddAbove (Set.range fun (N : ℕ) => positiveBesovPartialNormTwo Q s (N + 1) g)) (hmem : CubeBesovDualLocalMemLpGlobal Q 2 g) : |cubeBesovPairing Q u g| ≤ dualNegativeBesovNorm Q s 2 2 u * positiveBesovNormTwo Q s g

Local full-dual pairing bound with the Chapter 1 positive q = 2 norm as the test size.

theorem HCPolySupport.Book.Ch01.Legacy.negativeBesovLocalize_of_memLp {d : ℕ} (Q : Cube d) (s : ℝ) (f : Vec d → ℝ) (j : ℕ) (hs : 0 < s) (hf : MeasureTheory.MemLp f 2 (normalizedCubeMeasure Q)) : dualNegativeBesovSeminorm Q s 2 2 f ≤ negativeBesovLocalizeConstant d * √(descendantsAverage Q j fun (R : TriadicCube d) => (Real.rpow 3 (s * ↑j) * dualNegativeBesovNorm R s 2 2 f) ^ 2)

Manuscript negative Besov localization, with the parent L² hypothesis already converted to the normalized cube measure.

theorem HCPolySupport.Book.Ch01.Legacy.negativeBesovFullLocalize_of_memLp {d : ℕ} (Q : Cube d) (s : ℝ) (f : Vec d → ℝ) (j : ℕ) (hs : 0 < s) (hf : MeasureTheory.MemLp f 2 (normalizedCubeMeasure Q)) : dualNegativeBesovNorm Q s 2 2 f ≤ negativeBesovLocalizeConstant d * √(descendantsAverage Q j fun (R : TriadicCube d) => (Real.rpow 3 (s * ↑j) * dualNegativeBesovNorm R s 2 2 f) ^ 2)

Full-dual companion to the negative Besov localization theorem, with the parent L² hypothesis already converted to the normalized cube measure.

This is not the manuscript mean-zero statement, but it is the componentwise form used by downstream vector genuine-dual consumers.

theorem HCPolySupport.Book.Ch01.Legacy.negativeBesovFullLocalize {d : ℕ} (Q : Cube d) (s : ℝ) (f : Vec d → ℝ) (j : ℕ) (hs : 0 < s) (hf : MemScalarL2 (cubeSet Q) f) : dualNegativeBesovNorm Q s 2 2 f ≤ negativeBesovLocalizeConstant d * √(descendantsAverage Q j fun (R : TriadicCube d) => (Real.rpow 3 (s * ↑j) * dualNegativeBesovNorm R s 2 2 f) ^ 2)

Full-dual companion to negativeBesovLocalize, stated with the public MemScalarL2 hypothesis.

theorem HCPolySupport.Book.Ch01.Legacy.negativeBesovLocalize_cube {d : ℕ} (Q : Cube d) (s : ℝ) (f : Vec d → ℝ) (j : ℕ) (hs : 0 < s) (hf : MemScalarL2 (cubeSet Q) f) : dualNegativeBesovSeminorm Q s 2 2 f ≤ negativeBesovLocalizeConstant d * √(descendantsAverage Q j fun (R : TriadicCube d) => (Real.rpow 3 (s * ↑j) * dualNegativeBesovNorm R s 2 2 f) ^ 2)

Cube-general form of the negative Besov localization lemma.

theorem HCPolySupport.Book.Ch01.Legacy.negativeBesovLocalize {d : ℕ} {s : ℝ} {m n : ℤ} (_hd : 1 ≤ d) (hs_pos : 0 < s) (_hs_lt_one : s < 1) (hnm : n ≤ m) (f : Vec d → ℝ) (hf : MemScalarL2 (cubeSet (originCube d m)) f) : dualNegativeBesovSeminorm (originCube d m) s 2 2 f ≤ negativeBesovLocalizeConstant d * √(descendantsAverage (originCube d m) (m - n).toNat fun (R : TriadicCube d) => (Real.rpow 3 (-s * ↑(n - m)) * dualNegativeBesovNorm R s 2 2 f) ^ 2)

Manuscript Lemma l.Besov.negative.localize.function.spaces. The mean-zero dual negative Besov seminorm of f on the origin cube ⌈_m is bounded by the geometrically weighted root-mean-square of full local dual negative Besov norms on each triadic descendant z + ⌈_n for n ≤ m.