Limit

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.

The cube Sobolev embedding endgame

Cut off the fold extension Eu of u ∈ H¹(axisCube) to compact support inside the tripled box, package χ · Eu as an H¹₀ function with smooth compactly supported approximants ψ_k, apply the Gagliardo–Nirenberg–Sobolev inequality to each ψ_k, and pass to the limit (L^{2*} lower semicontinuity of eLpNorm along an a.e.-convergent subsequence). The reflection/cutoff constants and the L⁻¹ factor are collected into a single dimensional constant.

Operator norm versus coordinate values

theorem HCPolySupport.clm_norm_le_sum_basisVec {n : ℕ} (T : Vec n →L[ℝ] ℝ) : ‖T‖ ≤ ∑ i : Fin n, ‖T (basisVec i)‖

theorem HCPolySupport.gns_coord {m : ℕ} (hd : 3 ≤ m + 1) {ψ : Vec (m + 1) → ℝ} (hψ : ContDiff ℝ 1 ψ) (hcs : HasCompactSupport ψ) : MeasureTheory.eLpNorm ψ (↑(twoStar (m + 1))) MeasureTheory.volume ≤ ↑(MeasureTheory.SNormLESNormFDerivOfEqConst ℝ MeasureTheory.volume 2) * ∑ i : Fin (m + 1), MeasureTheory.eLpNorm (fun (x : Vec (m + 1)) => (fderiv ℝ ψ x) (basisVec i)) 2 MeasureTheory.volume

GNS in coordinate form. For a C¹, compactly supported function on Vec (m+1) with d = m+1 ≥ 3, the L^{2*} norm is controlled by the sum of the coordinate gradient L² norms.

theorem HCPolySupport.tendsto_eLpNorm_of_tendsto_sub {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : ENNReal} (hp : 1 ≤ p) {f : ℕ → α → ℝ} {g : α → ℝ} (hfin : MeasureTheory.eLpNorm g p μ ≠ ⊤) (h : Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm (fun (x : α) => f k x - g x) p μ) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm (f k) p μ) Filter.atTop (nhds (MeasureTheory.eLpNorm g p μ))

eLpNorm is continuous along Lᵖ-convergent sequences (p ≥ 1, finite target norm).

The cube Sobolev embedding

theorem HCPolySupport.cubeSobolevEmbedding {d : ℕ} (hd : 3 ≤ d) : ∃ (C : NNReal), 0 < C ∧ ∀ (z : Vec d) (L : ℝ), 0 < L → ∀ (u : H1Function (axisCube z L)), MeasureTheory.eLpNorm u.toFun (↑(twoStar d)) (volumeMeasureOn (axisCube z L)) ≤ ↑C * (∑ i : Fin d, MeasureTheory.eLpNorm (fun (x : Vec d) => u.grad x i) 2 (volumeMeasureOn (axisCube z L)) + ENNReal.ofReal L⁻¹ * MeasureTheory.eLpNorm u.toFun 2 (volumeMeasureOn (axisCube z L)))

Cube Sobolev embedding. Full statement.