The homogeneous `H¹ → L⁶` inequality on `ℝ³` #

Mathlib's Gagliardo–Nirenberg–Sobolev inequality eLpNorm_le_eLpNorm_fderiv_of_eq_inner bounds the L⁶ norm of a compactly supported C¹ function on ℝ³ by sobolevConstant times the L² norm of its derivative. This module fixes that constant once for both libraries and removes the support hypothesis: multiplying by the dilated cutoffs of NavierStokesAndEuler.SmoothCutoff costs a derivative error derivativeConstant 1 / R * ‖f‖₂ that vanishes as R → ∞, and Fatou's lemma (Lp.eLpNorm_lim_le_liminf_eLpNorm) passes to the limit. The result eLpNorm_six_le needs only f ∈ L²; when the derivative is also in L², memLp_six and the real-valued forms follow.

The exponents and spatial dimension are fixed, while the codomain is any real inner-product space. The compact-support, extended-norm, membership, and real-valued formulations share the same constant.

source

noncomputable def NavierStokesAndEuler.SobolevThreeDimensional.sobolevConstant :

NNReal

The fixed whole-space H¹ → L⁶ Sobolev constant in dimension three.

Equations

NavierStokesAndEuler.SobolevThreeDimensional.sobolevConstant = MeasureTheory.eLpNormLESNormFDerivOfEqInnerConst MeasureTheory.volume 2

Instances For

source

theorem NavierStokesAndEuler.SobolevThreeDimensional.sobolevConstant_nonneg :

0 ≤ ↑sobolevConstant

source

theorem NavierStokesAndEuler.SobolevThreeDimensional.eLpNorm_six_le_of_hasCompactSupport {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : EuclideanSpace ℝ (Fin 3) → E} (hf : ContDiff ℝ 1 f) (hs : HasCompactSupport f) :

MeasureTheory.eLpNorm f 6 MeasureTheory.volume ≤ ↑sobolevConstant * MeasureTheory.eLpNorm (fderiv ℝ f) 2 MeasureTheory.volume

Mathlib's homogeneous Sobolev inequality specialised to Euclidean ℝ³, exponents p = 2, p' = 6.

source

theorem NavierStokesAndEuler.SobolevThreeDimensional.norm_fderiv_cutoff_smul_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : EuclideanSpace ℝ (Fin 3) → E} (hf : ContDiff ℝ 1 f) {R : ℝ} (hR : 0 < R) (x : EuclideanSpace ℝ (Fin 3)) :

‖fderiv ℝ (fun (y : EuclideanSpace ℝ (Fin 3)) => SmoothCutoff.cutoff (EuclideanSpace ℝ (Fin 3)) R y • f y) x‖ ≤ ‖fderiv ℝ f x‖ + SmoothCutoff.derivativeConstant (EuclideanSpace ℝ (Fin 3)) 1 / R * ‖f x‖

The product rule with a uniformly bounded spatial cutoff.

source

theorem NavierStokesAndEuler.SobolevThreeDimensional.eLpNorm_fderiv_cutoff_smul_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : EuclideanSpace ℝ (Fin 3) → E} (hf : ContDiff ℝ 1 f) {R : ℝ} (hR : 0 < R) :

MeasureTheory.eLpNorm (fderiv ℝ fun (y : EuclideanSpace ℝ (Fin 3)) => SmoothCutoff.cutoff (EuclideanSpace ℝ (Fin 3)) R y • f y) 2 MeasureTheory.volume ≤ MeasureTheory.eLpNorm (fderiv ℝ f) 2 MeasureTheory.volume + ENNReal.ofReal (SmoothCutoff.derivativeConstant (EuclideanSpace ℝ (Fin 3)) 1 / R) * MeasureTheory.eLpNorm f 2 MeasureTheory.volume

The cutoff derivative has an L² error of size R⁻¹ ‖f‖₂.

source

theorem NavierStokesAndEuler.SobolevThreeDimensional.eLpNorm_six_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : EuclideanSpace ℝ (Fin 3) → E} (hf : ContDiff ℝ 1 f) (h2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) :

MeasureTheory.eLpNorm f 6 MeasureTheory.volume ≤ ↑sobolevConstant * MeasureTheory.eLpNorm (fderiv ℝ f) 2 MeasureTheory.volume

The homogeneous H¹ → L⁶ inequality without a support assumption. Only the function itself must have finite L² norm for this extended-norm inequality; the right side may be infinite.

source