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

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

Legacy fractional Sobolev versus Besov seminorms (CG Lemma 1.3)

Legacy, restricted real-valued overlap-comparison lane. On every triadic cube, its volume-normalized fractional Sobolev (Gagliardo) seminorm and older overlapping triadic Besov presentation B^s_{p,p} are equivalent, with a constant depending only on the dimension — uniformly in s ∈ (0,1], p ∈ [1,∞), and the cube scale.

Constant accounting (each factor uniform in s, p):

• upper bound (B ≤ C·W): overlap multiplicity 3^d and the backwards geometric pair tail ≤ 2, total 2·3^d at power p;
• lower bound (W ≤ C·B): triangle split 2·2^p ≤ 4^p, shell-versus-depth kernel slack 9^{sp+d} ≤ (9^{d+1})^p (uses s ≤ 1), center count 3^d ≤ (3^d)^p, shell reindexing 2 ≤ 2^p; total (2^3·3^{3d+2})^p;
• both collapse to the single constant wspVsBsppConstant d = 2^3·3^{3d+2} after the p-th root, since (X^p)^{1/p} = X and Y^{1/p} ≤ Y for Y ≥ 1.

The Lean proof replaces the manuscript's partition-of-unity argument by a discrete-annulus argument. Within this restricted lane the comparison shape is unchanged, but its Gagliardo kernel uses the ambient sup-distance, absorbed into C(d). Its overlap Besov side is the older finite-truncation / real-sSup presentation. This is not the new exact Euclidean / ENNReal manuscript API.

The packaged hypothesis MemFractionalSobolev (MemLp + MemWsp) is the legacy analogue of u ∈ W^{s,p}(□) for this ambient-sup-distance kernel. No measurability of the representative is assumed in the packaged theorem (the statement is a.e.-invariant, and a measurable representative is transported through CongruenceAE). The BddAbove side condition of the infinite-scale Besov seminorm is derived, not assumed.

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.Legacy.fractionalSobolevSeminorm {d : ℕ} (Q : Cube d) (s : ℝ) (p : ENNReal) (u : Vec d → ℝ) : ℝ

The legacy/restricted fractional Sobolev seminorm [u]_{W_underlined^{s,p}(□)}, using the ambient sup-distance Gagliardo kernel.

Equations

• HCPolySupport.Book.Ch01.Legacy.fractionalSobolevSeminorm Q s p u = HCPolySupport.Gagliardo.cubeGagliardoSeminorm Q s p u

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.Legacy.positiveBesovOverlapSeminormDiagonal {d : ℕ} (Q : Cube d) (s : ℝ) (p : ENNReal) (u : Vec d → ℝ) : ℝ

The legacy/restricted overlapping Besov seminorm [u]_{B_underlined^s_{p,p}(□)} in the finite-truncation / real-sSup presentation.

Equations

• HCPolySupport.Book.Ch01.Legacy.positiveBesovOverlapSeminormDiagonal Q s p u = HCPolySupport.cubeBesovOverlapSeminorm Q s p p u

def HCPolySupport.Book.Ch01.Legacy.MemFractionalSobolev {d : ℕ} (Q : Cube d) (s : ℝ) (p : ENNReal) (u : Vec d → ℝ) : Prop

Legacy/restricted packaged membership: L^p on the cube with finite ambient-sup-distance Gagliardo seminorm. This is not the exact Euclidean / ENNReal manuscript u ∈ W^{s,p}(□_m) API; no measurability of the representative is assumed (it is recovered a.e. from MemLp).

Equations

• HCPolySupport.Book.Ch01.Legacy.MemFractionalSobolev Q s p u = (MeasureTheory.MemLp u p (HCPolySupport.normalizedCubeMeasure Q) ∧ HCPolySupport.Gagliardo.MemWsp Q s p u)

theorem HCPolySupport.Book.Ch01.Legacy.MemFractionalSobolev.memLp {d : ℕ} {Q : Cube d} {s : ℝ} {p : ENNReal} {u : Vec d → ℝ} (h : MemFractionalSobolev Q s p u) : MeasureTheory.MemLp u p (normalizedCubeMeasure Q)

theorem HCPolySupport.Book.Ch01.Legacy.MemFractionalSobolev.memWsp {d : ℕ} {Q : Cube d} {s : ℝ} {p : ENNReal} {u : Vec d → ℝ} (h : MemFractionalSobolev Q s p u) : Gagliardo.MemWsp Q s p u

noncomputable def HCPolySupport.Book.Ch01.Legacy.wspVsBsppConstant (d : ℕ) : ℝ

The legacy/restricted overlap-comparison constant; it depends on the dimension only and is fixed before every other quantifier.

Equations

• HCPolySupport.Book.Ch01.Legacy.wspVsBsppConstant d = 2 ^ 3 * 3 ^ (3 * d + 2)

theorem HCPolySupport.Book.Ch01.Legacy.one_le_wspVsBsppConstant (d : ℕ) : 1 ≤ wspVsBsppConstant d

theorem HCPolySupport.Book.Ch01.Legacy.wspVsBsppConstant_pos (d : ℕ) : 0 < wspVsBsppConstant d

theorem HCPolySupport.Book.Ch01.Legacy.gagliardoBesovLowerConstant_toReal (d : ℕ) : (Gagliardo.gagliardoBesovLowerConstant d).toReal = wspVsBsppConstant d

toReal of the L-direction ℝ≥0∞ constant is the note constant.

theorem HCPolySupport.Book.Ch01.Legacy.besovOverlapPartial_le_const_mul_gagliardo {d : ℕ} [NeZero d] (Q : Cube d) {s : ℝ} {p : ENNReal} {u : Vec d → ℝ} (hs : 0 < s) (hp : 1 ≤ p) (hpt : p ≠ ⊤) (humeas : Measurable u) (hu : MeasureTheory.MemLp u p (normalizedCubeMeasure Q)) (hW : Gagliardo.MemWsp Q s p u) (N : ℕ) : cubeBesovOverlapPartialSeminorm Q s p p N u ≤ wspVsBsppConstant d * fractionalSobolevSeminorm Q s p u

Legacy upper bound: every finite-depth overlap-Besov partial seminorm is controlled by the ambient-sup-distance Gagliardo seminorm.

theorem HCPolySupport.Book.Ch01.Legacy.fractionalSobolevVsBesovSeminorms {d : ℕ} [NeZero d] (Q : Cube d) {s : ℝ} {p : ENNReal} {u : Vec d → ℝ} (hs : 0 < s) (hs1 : s ≤ 1) (hp : 1 ≤ p) (hpt : p ≠ ⊤) (humeas : Measurable u) (hu : MeasureTheory.MemLp u p (normalizedCubeMeasure Q)) (hW : Gagliardo.MemWsp Q s p u) : (wspVsBsppConstant d)⁻¹ * fractionalSobolevSeminorm Q s p u ≤ positiveBesovOverlapSeminormDiagonal Q s p u ∧ positiveBesovOverlapSeminormDiagonal Q s p u ≤ wspVsBsppConstant d * fractionalSobolevSeminorm Q s p u

Legacy/restricted two-sided overlap comparison: C(d)⁻¹·[u]_{W_underlined^{s,p}} ≤ [u]_{B_underlined^s_{p,p}} ≤ C(d)·[u]_{W_underlined^{s,p}} on every triadic cube, with C(d) = wspVsBsppConstant d fixed before all other quantifiers, uniformly in s ∈ (0,1], p ∈ [1,∞), and the cube.

theorem HCPolySupport.Book.Ch01.Legacy.fractionalSobolevVsBesovSeminorms_of_memFractionalSobolev {d : ℕ} [NeZero d] (Q : Cube d) {s : ℝ} {p : ENNReal} {u : Vec d → ℝ} (hs : 0 < s) (hs1 : s ≤ 1) (hp : 1 ≤ p) (hpt : p ≠ ⊤) (hu : MemFractionalSobolev Q s p u) : (wspVsBsppConstant d)⁻¹ * fractionalSobolevSeminorm Q s p u ≤ positiveBesovOverlapSeminormDiagonal Q s p u ∧ positiveBesovOverlapSeminormDiagonal Q s p u ≤ wspVsBsppConstant d * fractionalSobolevSeminorm Q s p u

The legacy/restricted two-sided overlap comparison with its packaged membership hypothesis. No measurability hypothesis: the statement is invariant under a.e.-modification, and a measurable representative is extracted from MemLp and transported back through the congruence lemmas.