CubeEmbedding

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

The cube Sobolev embedding

The single theorem below, cube_sobolev_embedding, is the cube Sobolev embedding at the critical exponent 2* = 2d/(d−2), stated against the ambient H1Function / volumeMeasureOn / axisCube types and proved via cubeSobolevEmbedding.

For u ∈ H¹(U) on an open axis cube U = axisCube z L (no boundary vanishing assumed), the route is: even-reflection extension across each face, a smooth cutoff to compact support inside the tripled box, mathlib's Gagliardo–Nirenberg–Sobolev inequality on each smooth compactly supported approximant, and passage to the limit, with the reflection/cutoff constants and the L⁻¹ factor collected into a single dimensional constant.

Norms are in eLpNorm house style against volumeMeasureOn U, critical exponent twoStar d = 2d/(d−2), and gradient term the sum of the coordinate L² norms ∑ i ‖∂ᵢu‖_{L²(U)}.

theorem HCPolySupport.cube_sobolev_embedding {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)))

E1 (cube Sobolev embedding, critical exponent 2* = 2d/(d−2)).

For d ≥ 3 there is a constant C = C(d) > 0 such that for every open axis cube U = axisCube z L of side L > 0 and every u ∈ H¹(U) (the library's H1Function U, no boundary vanishing), ‖u‖_{L^{2*}(U)} ≤ C (‖∇u‖_{L²(U)} + L⁻¹ ‖u‖_{L²(U)}), with ‖u‖_{L^{2*}(U)} = eLpNorm u.toFun (twoStar d) (volumeMeasureOn U) and the gradient term the sum of the coordinate L²(U) norms of u.grad.

Proved via cubeSobolevEmbedding (CubeEmbedding/Limit.lean).