Homogeneous Sobolev bounds for smooth square-integrable functions

Spatial cutoffs extend the compactly supported Sobolev inequality to a smooth function whose value and derivative belong to L². The derivative of the cutoff contributes an error tending to zero; Fatou's lemma passes to the limit.

theorem NavierStokesR3.RieszTestOperators.norm_fderiv_cutoff_smul_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : ProblemStatement.Space → E} (hf : ContDiff ℝ 1 f) {R : ℝ} (hR : 0 < R) (x : ProblemStatement.Space) : ‖fderiv ℝ (fun (y : ProblemStatement.Space) => ComparisonCutoffs.cutoff R y • f y) x‖ ≤ ‖fderiv ℝ f x‖ + ComparisonCutoffs.derivativeConstant 1 / R * ‖f x‖

The product rule with a uniformly bounded spatial cutoff.

theorem NavierStokesR3.RieszTestOperators.eLpNorm_fderiv_cutoff_smul_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : ProblemStatement.Space → E} (hf : ContDiff ℝ 1 f) {R : ℝ} (hR : 0 < R) : MeasureTheory.eLpNorm (fderiv ℝ fun (y : ProblemStatement.Space) => ComparisonCutoffs.cutoff R y • f y) 2 MeasureTheory.volume ≤ MeasureTheory.eLpNorm (fderiv ℝ f) 2 MeasureTheory.volume + ENNReal.ofReal (ComparisonCutoffs.derivativeConstant 1 / R) * MeasureTheory.eLpNorm f 2 MeasureTheory.volume

The cutoff derivative has a vanishing L² error.

theorem NavierStokesR3.RieszTestOperators.smooth_eLpNorm_six_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : ProblemStatement.Space → E} (hf : ContDiff ℝ 1 f) (h2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) : MeasureTheory.eLpNorm f 6 MeasureTheory.volume ≤ ↑(MeasureTheory.eLpNormLESNormFDerivOfEqInnerConst MeasureTheory.volume 2) * 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.

theorem NavierStokesR3.RieszTestOperators.smooth_memLp_six {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : ProblemStatement.Space → E} (hf : ContDiff ℝ 1 f) (h2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hD2 : MeasureTheory.MemLp (fderiv ℝ f) 2 MeasureTheory.volume) : MeasureTheory.MemLp f 6 MeasureTheory.volume

A smooth function with square-integrable value and derivative belongs to L⁶, with no support hypothesis.

theorem NavierStokesR3.RieszTestOperators.smooth_eLpNorm_six_toReal_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : ProblemStatement.Space → E} (hf : ContDiff ℝ 1 f) (h2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hD2 : MeasureTheory.MemLp (fderiv ℝ f) 2 MeasureTheory.volume) : (MeasureTheory.eLpNorm f 6 MeasureTheory.volume).toReal ≤ ↑(MeasureTheory.eLpNormLESNormFDerivOfEqInnerConst MeasureTheory.volume 2) * (MeasureTheory.eLpNorm (fderiv ℝ f) 2 MeasureTheory.volume).toReal

The real-valued homogeneous Sobolev bound when both L² norms are finite.