Uniform energy bounds for the forced regularized solutions

lem:forced-energy-bounds: the forced energy inequality eq:reg-energy-forced with 2 f·u ≤ |f|² + |u|² and Grönwall's inequality bound the kinetic energy on [0,T] by E_T = e^T (‖a‖₂² + ‖f‖²_{L²((0,T)×ℝ³)}), and substitution back into the same inequality bounds the dissipation on (0,T) by G_T² = (‖a‖₂² + ‖f‖²_{L²((0,T)×ℝ³)} + T E_T) / 2. Both constants are independent of the regularization parameter.

theorem CKN.Leray.forcedLerayLimit_energy_bounds (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hf : IsLocallySquareIntegrableForce f) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (hSlice : ∀ (t : ℝ), 0 ≤ t → MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume) (hcont : Continuous fun (t : ↑(Set.Ici 0)) => realVectorL2OfCoordinateFunction (fun (x : Foundation.Parabolic.Vec3) => u (x, ↑t)) ⋯) (hu : ∀ (T : ℝ), 0 < T → MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hDu : ∀ (T : ℝ), 0 < T → MeasureTheory.MemLp Du 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) (henergy : ∀ (t : ℝ), 0 ≤ t → (MeasureTheory.eLpNorm (regUniformVelocitySlice u t) 2 MeasureTheory.volume ^ 2 + 2 * regUniformDissipation u Du t).toReal ≤ (MeasureTheory.eLpNorm (regMollifyVector ρ ε hε (regUniformSpatialField a)) 2 MeasureTheory.volume ^ 2).toReal + 2 * ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 t), ∑ i : Fin 3, f z i * u z i) (T : ℝ) (hT : 0 < T) : (∀ t ∈ Set.Icc 0 T, ∑ i : Fin 3, ∫ (x : Foundation.Parabolic.Vec3), u (x, t) i ^ 2 ≤ Real.exp T * ((∑ i : Fin 3, ∫ (x : Foundation.Parabolic.Vec3), a x i ^ 2) + ∑ i : Fin 3, ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 T), f z i ^ 2)) ∧ 2 * ∑ i : Fin 3, ∑ j : Fin 3, ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 T), Du z i j ^ 2 ≤ ((∑ i : Fin 3, ∫ (x : Foundation.Parabolic.Vec3), a x i ^ 2) + ∑ i : Fin 3, ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 T), f z i ^ 2) + T * (Real.exp T * ((∑ i : Fin 3, ∫ (x : Foundation.Parabolic.Vec3), a x i ^ 2) + ∑ i : Fin 3, ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 T), f z i ^ 2))

lem:forced-energy-bounds: a velocity with continuous L² slices, a square-integrable weak gradient on finite slabs and the forced energy inequality eq:reg-energy-forced satisfies, on every [0,T], the kinetic bound ‖u(t)‖₂² ≤ E_T and the dissipation bound 2 ∫₀ᵀ ‖Du‖₂² ≤ 2 G_T², with E_T and G_T depending only on T, ‖a‖₂ and the L² norm of f on (0,T).