Sobolev Global L6

Supporting estimates for the Navier–Stokes development.

theorem CKN.sobolev_L6_global : ∃ (C : ENNReal), C ≠ ⊤ ∧ ∀ (g : H1Function Set.univ), lpNormOn 6 Set.univ g.toFun ≤ C * weakGradientLpNormOn 2 Set.univ g.grad

The global homogeneous Sobolev inequality, with one absolute constant chosen before the function.

theorem CKN.sobolev_L6_global_inhomogeneous : ∃ (C : ENNReal), C ≠ ⊤ ∧ ∀ (g : H1Function Set.univ), lpNormOn 6 Set.univ g.toFun ≤ C * (weakGradientLpNormOn 2 Set.univ g.grad + lpNormOn 2 Set.univ g.toFun)

The inhomogeneous whole-space consequence, with the same absolute constant as the homogeneous inequality.

theorem CKN.sobolev_L6_ball_slices {x₀ : Foundation.Parabolic.Vec3} {r : ℝ} (hr : 0 < r) {J : Set ℝ} (u : ℝ → H1Function (euclideanBall x₀ r)) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, lpNormOn 6 (euclideanBall x₀ r) (u t).toFun ≤ ENNReal.ofReal sobolevPoincareFaithfulC5 * (weakGradientLpNormOn 2 (euclideanBall x₀ r) (u t).grad + (ENNReal.ofReal r)⁻¹ * lpNormOn 2 (euclideanBall x₀ r) (u t).toFun)

The scale-explicit spatial Sobolev estimate holds for almost every member of a time-indexed family of H¹ functions on a ball.