The ordinary three-dimensional H¹ product estimate. The homogeneous L⁶ inequality is extended from compact fields by genuine cutoff limits; the L⁴ bound and product estimate therefore require no support hypothesis.

theorem EulerOrdinarySobolev.eLpNorm_six_le {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (f : EulerSmoothLimit.Space → V) (hf : ContDiff ℝ (↑⊤) f) (hL : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hD : MeasureTheory.MemLp (fderiv ℝ f) 2 MeasureTheory.volume) : MeasureTheory.eLpNorm f 6 MeasureTheory.volume ≤ ↑EulerMeanCutoffCurl.sobolevConstant * MeasureTheory.eLpNorm (fderiv ℝ f) 2 MeasureTheory.volume

theorem EulerOrdinarySobolev.memLp_six {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (f : EulerSmoothLimit.Space → V) (hf : ContDiff ℝ (↑⊤) f) (hL : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hD : MeasureTheory.MemLp (fderiv ℝ f) 2 MeasureTheory.volume) : MeasureTheory.MemLp f 6 MeasureTheory.volume

theorem EulerOrdinarySobolev.norm_six_le {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (f : EulerSmoothLimit.Space → V) (hf : ContDiff ℝ (↑⊤) f) (hL : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hD : MeasureTheory.MemLp (fderiv ℝ f) 2 MeasureTheory.volume) : (MeasureTheory.eLpNorm f 6 MeasureTheory.volume).toReal ≤ ↑EulerMeanCutoffCurl.sobolevConstant * (MeasureTheory.eLpNorm (fderiv ℝ f) 2 MeasureTheory.volume).toReal

theorem EulerOrdinarySobolev.cube_memLp {E : Type u_2} [NormedAddCommGroup E] {f : EulerSmoothLimit.Space → E} (h6 : MeasureTheory.MemLp f 6 MeasureTheory.volume) : MeasureTheory.MemLp (fun (x : EulerSmoothLimit.Space) => ‖f x‖ ^ 3) 2 MeasureTheory.volume

theorem EulerOrdinarySobolev.cube_norm {E : Type u_2} [NormedAddCommGroup E] {f : EulerSmoothLimit.Space → E} (h6 : MeasureTheory.MemLp f 6 MeasureTheory.volume) : MeasureTheory.lpNorm (fun (x : EulerSmoothLimit.Space) => ‖f x‖ ^ 3) 2 MeasureTheory.volume = MeasureTheory.lpNorm f 6 MeasureTheory.volume ^ 3

theorem EulerOrdinarySobolev.square_memLp {E : Type u_2} [NormedAddCommGroup E] {f : EulerSmoothLimit.Space → E} (h2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) (h6 : MeasureTheory.MemLp f 6 MeasureTheory.volume) : MeasureTheory.MemLp (fun (x : EulerSmoothLimit.Space) => ‖f x‖ ^ 2) 2 MeasureTheory.volume

theorem EulerOrdinarySobolev.square_norm_scaled {E : Type u_2} [NormedAddCommGroup E] {f : EulerSmoothLimit.Space → E} (h2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) (h6 : MeasureTheory.MemLp f 6 MeasureTheory.volume) (a : ℝ) (ha : 0 < a) : MeasureTheory.lpNorm (fun (x : EulerSmoothLimit.Space) => ‖f x‖ ^ 2) 2 MeasureTheory.volume ≤ a * MeasureTheory.lpNorm f 2 MeasureTheory.volume + a⁻¹ * MeasureTheory.lpNorm f 6 MeasureTheory.volume ^ 3

theorem EulerOrdinarySobolev.square_norm_le_two {E : Type u_2} [NormedAddCommGroup E] {f : EulerSmoothLimit.Space → E} (h2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) (h6 : MeasureTheory.MemLp f 6 MeasureTheory.volume) (a : ℝ) (ha : 0 ≤ a) (h2a : MeasureTheory.lpNorm f 2 MeasureTheory.volume ≤ a) (h6a : MeasureTheory.lpNorm f 6 MeasureTheory.volume ≤ a) : MeasureTheory.lpNorm (fun (x : EulerSmoothLimit.Space) => ‖f x‖ ^ 2) 2 MeasureTheory.volume ≤ 2 * a ^ 2

theorem EulerOrdinarySobolev.memLp_four {E : Type u_2} [NormedAddCommGroup E] {f : EulerSmoothLimit.Space → E} (h2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) (h6 : MeasureTheory.MemLp f 6 MeasureTheory.volume) : MeasureTheory.MemLp f 4 MeasureTheory.volume

theorem EulerOrdinarySobolev.norm_four_sq {E : Type u_2} [NormedAddCommGroup E] {f : EulerSmoothLimit.Space → E} (h2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) (h6 : MeasureTheory.MemLp f 6 MeasureTheory.volume) : MeasureTheory.lpNorm f 4 MeasureTheory.volume ^ 2 = MeasureTheory.lpNorm (fun (x : EulerSmoothLimit.Space) => ‖f x‖ ^ 2) 2 MeasureTheory.volume

theorem EulerOrdinarySobolev.norm_four_le_two {E : Type u_2} [NormedAddCommGroup E] {f : EulerSmoothLimit.Space → E} (h2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) (h6 : MeasureTheory.MemLp f 6 MeasureTheory.volume) (a : ℝ) (ha : 0 ≤ a) (h2a : MeasureTheory.lpNorm f 2 MeasureTheory.volume ≤ a) (h6a : MeasureTheory.lpNorm f 6 MeasureTheory.volume ≤ a) : MeasureTheory.lpNorm f 4 MeasureTheory.volume ≤ 2 * a

theorem EulerOrdinarySobolev.smooth_four_bound {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (f : EulerSmoothLimit.Space → V) (hf : ContDiff ℝ (↑⊤) f) (hL : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hD : MeasureTheory.MemLp (fderiv ℝ f) 2 MeasureTheory.volume) : MeasureTheory.MemLp f 4 MeasureTheory.volume ∧ MeasureTheory.lpNorm f 4 MeasureTheory.volume ≤ 2 * (MeasureTheory.lpNorm f 2 MeasureTheory.volume + ↑EulerMeanCutoffCurl.sobolevConstant * MeasureTheory.lpNorm (fderiv ℝ f) 2 MeasureTheory.volume)

theorem EulerOrdinarySobolev.smooth_product_h1 {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (f : EulerSmoothLimit.Space → ℝ) (g : EulerSmoothLimit.Space → V) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (hfL : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hgL : MeasureTheory.MemLp g 2 MeasureTheory.volume) (hfD : MeasureTheory.MemLp (fderiv ℝ f) 2 MeasureTheory.volume) (hgD : MeasureTheory.MemLp (fderiv ℝ g) 2 MeasureTheory.volume) : MeasureTheory.MemLp (fun (x : EulerSmoothLimit.Space) => f x • g x) 2 MeasureTheory.volume ∧ MeasureTheory.lpNorm (fun (x : EulerSmoothLimit.Space) => f x • g x) 2 MeasureTheory.volume ≤ 4 * (MeasureTheory.lpNorm f 2 MeasureTheory.volume + ↑EulerMeanCutoffCurl.sobolevConstant * MeasureTheory.lpNorm (fderiv ℝ f) 2 MeasureTheory.volume) * (MeasureTheory.lpNorm g 2 MeasureTheory.volume + ↑EulerMeanCutoffCurl.sobolevConstant * MeasureTheory.lpNorm (fderiv ℝ g) 2 MeasureTheory.volume)