Coarse-graining support: Support.Sobolev.CubeEmbedding.GagliardoNirenbergSobolev

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

Gagliardo–Nirenberg–Sobolev at the ambient Vec d

Instantiates mathlib's Gagliardo–Nirenberg–Sobolev inequality (MeasureTheory.eLpNorm_le_eLpNorm_fderiv_of_eq) at the ambient Vec d = Fin d → ℝ with Lebesgue volume, codomain ℝ, p = 2, and target the critical exponent 2* = 2d/(d−2). It records that Vec d carries every typeclass the inequality needs (finite-dimensional, Borel, Haar volume) without any detour through EuclideanSpace/PiLp, that Module.finrank ℝ (Vec d) = d, and the exponent bookkeeping 1/2* = 1/2 − 1/d for d ≥ 3.

This is the form fed to each smooth compactly supported approximant in the cube Sobolev embedding.

noncomputable def HCPolySupport.twoStar (d : ℕ) : NNReal

The critical Sobolev exponent 2* = 2d/(d−2), as an ℝ≥0. For d ≥ 3 this is a genuine exponent > 2.

Equations

• HCPolySupport.twoStar d = 2 * ↑d / (↑d - 2)

theorem HCPolySupport.finrank_vec (d : ℕ) : Module.finrank ℝ (Vec d) = d

Vec d has finite rank d (sanity fact used to discharge the GNS finrank side-conditions).

theorem HCPolySupport.gns_contDiff_compactSupport {d : ℕ} (hd : 3 ≤ d) {u : Vec d → ℝ} (hu : ContDiff ℝ 1 u) (h2u : HasCompactSupport u) : MeasureTheory.eLpNorm u (↑(twoStar d)) MeasureTheory.volume ≤ ↑(MeasureTheory.SNormLESNormFDerivOfEqConst ℝ MeasureTheory.volume ↑2) * MeasureTheory.eLpNorm (fderiv ℝ u) 2 MeasureTheory.volume

Gagliardo–Nirenberg–Sobolev at Vec d. For d ≥ 3 and a C¹, compactly supported real function u on Vec d, the L^{2*} norm of u (w.r.t. Lebesgue volume) is controlled by the L² norm of its Fréchet derivative, with the mathlib GNS constant.

This is the form invoked on each smooth compactly supported approximant in the reflection route. It certifies the exponent arithmetic 1/2* = 1/2 − 1/d and that Vec d satisfies every hypothesis of eLpNorm_le_eLpNorm_fderiv_of_eq with no EuclideanSpace routing.