Compactness Gradient Energy

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.memLp_gradient_fiber_of_integrated_energy {K : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (u : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.Vec3 × ℝ → Fin 3 → Foundation.Parabolic.Vec3) (hDuMeas : Measurable Du) (henergy : ∫⁻ (t : ℝ) in J, ∫⁻ (x : Foundation.Parabolic.Vec3) in K, ENNReal.ofReal (spatialGradientSq u Du (x, t)) < ⊤) : MeasureTheory.MemLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => toCompactnessGradientFiber (Du z)) 2 ((MeasureTheory.volume.restrict K).prod (MeasureTheory.volume.restrict J))

Finite integrated spatial gradient energy gives L² membership of the matrix field in its Hilbert carrier.

theorem CKN.Leray.norm_toLp_gradient_fiber_le {μ : MeasureTheory.Measure (Foundation.Parabolic.Vec3 × ℝ)} (u : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.Vec3 × ℝ → Fin 3 → Foundation.Parabolic.Vec3) (hf : MeasureTheory.MemLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => toCompactnessGradientFiber (Du z)) 2 μ) (G : ENNReal) (hG : G < ⊤) (henergy : ∫⁻ (z : Foundation.Parabolic.Vec3 × ℝ), ENNReal.ofReal (spatialGradientSq u Du z) ∂μ ≤ G) : ‖MeasureTheory.MemLp.toLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => toCompactnessGradientFiber (Du z)) hf‖ ≤ (G ^ (1 / 2)).toReal

An integrated spatial energy bound controls the corresponding Hilbert L² norm with the same constant.