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

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

Finite-p Gagliardo--Nirenberg--Sobolev on Vec d

This is the ambient compact-support form of the finite-exponent Sobolev inequality. The cube localization layer can use it without committing to a particular formula for the critical exponent.

theorem HCPolySupport.gns_contDiff_compactSupport_finiteLp {d : ℕ} (hd : 0 < d) (p q : FiniteLpExponent) (hp : p.exponent.toReal < ↑d) (hpq : q.exponent.toReal⁻¹ = p.exponent.toReal⁻¹ - (↑d)⁻¹) {u : Vec d → ℝ} (hu : ContDiff ℝ 1 u) (hcs : HasCompactSupport u) : MeasureTheory.eLpNorm u q.exponent MeasureTheory.volume ≤ ↑(MeasureTheory.SNormLESNormFDerivOfEqConst ℝ MeasureTheory.volume ↑p.exponent.toNNReal) * MeasureTheory.eLpNorm (fderiv ℝ u) p.exponent MeasureTheory.volume

Ambient finite-p Gagliardo--Nirenberg--Sobolev inequality, with the Sobolev relation between p and q supplied exactly in real exponents.