Coarse-graining support: Support.Book.Ch03.Theorems.SobolevPublic

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

Legacy Sobolev/dual-Besov compatibility wrappers for the Chapter 3 comparison

This file supplies the compatibility layer used by Book.MainResults: positive data use the componentwise legacy fractional-Sobolev form from Ch01.Legacy, while the negative left-hand side is a legacy dual-Besov wrapper. The bridge lemmas convert these compatibility quantities to the Besov quantities consumed by the already-proved deterministic comparison theorem. The positive lane is the legacy ambient-sup-distance, finite-truncation / real-sSup overlap presentation, not the exact Euclidean / ENNReal manuscript API.

def HCPolySupport.Book.Ch03.Legacy.ForceSobolevRegularity {d : ℕ} (Q : TriadicCube d) (s : ℝ) (g : Vec d → Vec d) : Prop

Legacy componentwise fractional-Sobolev regularity for a vector force.

Equations

• HCPolySupport.Book.Ch03.Legacy.ForceSobolevRegularity Q s g = ∀ (i : Fin d), HCPolySupport.Book.Ch01.Legacy.MemFractionalSobolev Q s 2 fun (x : HCPolySupport.Book.Ch01.Vec d) => g x i

noncomputable def HCPolySupport.Book.Ch03.Legacy.scaleNormalizedPositiveSobolevVectorSeminormTwo {d : ℕ} (Q : TriadicCube d) (s : ℝ) (g : Vec d → Vec d) : ℝ

Legacy scale-normalized componentwise fractional-Sobolev seminorm.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch03.Legacy.scaleNormalizedNegativeSobolevVectorNormTwo {d : ℕ} (Q : TriadicCube d) (s : ℝ) (F : Vec d → Vec d) : ℝ

Legacy dual-Besov wrapper used by the Chapter 3 compatibility lane.

Its body is scaleNormalizedDualNegativeBesovVectorNormTwo; it is not an identification with either Chapter 1 negative-Sobolev primitive.

Equations

• HCPolySupport.Book.Ch03.Legacy.scaleNormalizedNegativeSobolevVectorNormTwo Q s F = HCPolySupport.Book.Ch03.scaleNormalizedDualNegativeBesovVectorNormTwo Q s F

noncomputable def HCPolySupport.Book.Ch03.Legacy.homogenizationComparisonNegativeSobolevLHS {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) (a0 : ConstantCoeffMatrix d) (s : ℝ) (u v : H1Function (Ch02.cubeDomain Q).carrier) : ℝ

Legacy dual-Besov compatibility left-hand side of the homogenization comparison.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.Book.Ch03.Legacy.scaleNormalizedPositiveSobolevVectorSeminormTwo_nonneg {d : ℕ} (Q : TriadicCube d) (s : ℝ) (g : Vec d → Vec d) : 0 ≤ scaleNormalizedPositiveSobolevVectorSeminormTwo Q s g

theorem HCPolySupport.Book.Ch03.Legacy.forceSobolevRegularity_memLp {d : ℕ} {Q : TriadicCube d} {s : ℝ} {g : Vec d → Vec d} (hg : ForceSobolevRegularity Q s g) : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)

theorem HCPolySupport.Book.Ch03.cubeLpNorm_two_vec_le_sum_components {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) : cubeLpNorm Q 2 u ≤ ∑ i : Fin d, cubeLpNorm Q 2 fun (x : Vec d) => u x i

theorem HCPolySupport.Book.Ch03.sqrt_cubeBesovPositiveVectorDepthAverage_le_sum_components {d : ℕ} (Q : TriadicCube d) (g : Vec d → Vec d) (j : ℕ) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) : √(cubeBesovPositiveVectorDepthAverage Q g j) ≤ ∑ i : Fin d, √(cubeBesovDepthAverage Q 2 (fun (x : Vec d) => g x i) j)

theorem HCPolySupport.Book.Ch03.cubeBesovPositiveVectorPartialSeminormTwo_le_scaleWeight_mul_sum_components {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (g : Vec d → Vec d) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) : cubeBesovPositiveVectorPartialSeminormTwo Q s N g ≤ cubeBesovScaleWeight (-s) Q * ∑ i : Fin d, cubeBesovPartialSeminorm Q s 2 2 N fun (x : Vec d) => g x i

theorem HCPolySupport.Book.Ch03.Legacy.cubeBesovPositiveVectorPartialSeminormTwo_le_const_mul_sobolev {d : ℕ} [NeZero d] (Q : TriadicCube d) {s : ℝ} (N : ℕ) (g : Vec d → Vec d) (hs : 0 < s) (_hs1 : s ≤ 1) (hg : ForceSobolevRegularity Q s g) : cubeBesovPositiveVectorPartialSeminormTwo Q s N g ≤ 3 ^ (↑d / 2) * Ch01.Legacy.wspVsBsppConstant d * scaleNormalizedPositiveSobolevVectorSeminormTwo Q s g

theorem HCPolySupport.Book.Ch03.Legacy.ForceSobolevRegularity.toForceBesovRegularity {d : ℕ} [NeZero d] {Q : TriadicCube d} {s : ℝ} {g : Vec d → Vec d} (hg : ForceSobolevRegularity Q s g) (hs : 0 < s) (hs1 : s ≤ 1) : ForceBesovRegularity Q s g

theorem HCPolySupport.Book.Ch03.Legacy.scaleNormalizedPositiveBesovVectorSeminormTwo_le_const_mul_sobolev {d : ℕ} [NeZero d] (Q : TriadicCube d) {s : ℝ} (g : Vec d → Vec d) (hs : 0 < s) (hs1 : s ≤ 1) (hg : ForceSobolevRegularity Q s g) : scaleNormalizedPositiveBesovVectorSeminormTwo Q s g ≤ 3 ^ (↑d / 2) * Ch01.Legacy.wspVsBsppConstant d * scaleNormalizedPositiveSobolevVectorSeminormTwo Q s g

theorem HCPolySupport.Book.Ch03.Legacy.homogenizationComparisonNegativeSobolevLHS_le_const_mul_negativeBesovLHS {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffFamily d) (a0 : ConstantCoeffMatrix d) (s : ℝ) (u v : H1Function (Ch02.cubeDomain Q).carrier) (hs : 0 < s) : homogenizationComparisonNegativeSobolevLHS Q a a0 s u v ≤ ↑d * Real.rpow 3 (↑d + s) * homogenizationComparisonNegativeBesovLHS Q a a0 s u v