The energy equality of the regularized solutions on an interval

The energy equality (R5) of thm:regularised, in its local form on [0, T]: a velocity that solves the regularized mild equation eq:reg-mild on [0, T] with the mollified datum, has divergence-free square-integrable slices that depend continuously on time, and is classically differentiable in space at positive times, satisfies ‖u(t)‖² + 2∫₀ᵗ‖∇u‖² = ‖J_ε a‖² for every t ∈ [0, T].

The proof works on the Fourier side. The frequency-wise damped Duhamel identity integrates to the energy balance of the mild equation; the Fourier solution is real because the heat and Stokes symbols respect the reflected conjugation; the transport term vanishes because the transporting field J_ε u is divergence free; and the frequency dissipation equals the classical dissipation because the classical spatial derivatives of u are its weak derivatives.

@[instance_reducible]

def CKN.Leray.regularisedEnergyIntervalNormedAddCommGroup : NormedAddCommGroup Foundation.Parabolic.ParabolicPoint

The product normed additive group structure on space-time used for energy intervals.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable def CKN.Leray.regularisedEnergyIntervalNormedSpace : NormedSpace ℝ Foundation.Parabolic.ParabolicPoint

The real normed-space structure on space-time used for regularized energy intervals.

Equations

• One or more equations did not get rendered due to their size.

theorem CKN.Leray.regUniformSpatialField_eLpNorm_sq_eq_ofReal (f : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) : MeasureTheory.eLpNorm (regUniformSpatialField f) 2 MeasureTheory.volume ^ 2 = ENNReal.ofReal (‖realVectorL2OfCoordinateFunction f hf‖ ^ 2)

The squared spatial L² seminorm of a CKN vector field is the squared norm of its Fourier-space L² class.

theorem CKN.Leray.regularised_R5_on_interval_of_mild (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (T : ℝ) (hT : 0 < T) (hSlice : ∀ t ∈ Set.Icc 0 T, MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume) (hL2Continuous : Continuous fun (t : ↑(Set.Icc 0 T)) => realVectorL2OfCoordinateFunction (fun (x : Foundation.Parabolic.Vec3) => u (x, ↑t)) ⋯) (hDivFree : ∀ t ∈ Set.Icc 0 T, IsWeakDivFreeL2 fun (x : Foundation.Parabolic.Vec3) => u (x, t)) (hDcontinuous : ∀ (i j : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j z) (spaceTimeSet Set.univ (Set.Ioc 0 T))) (hUjoint : ∀ (i : Fin 3), ContDiffOn ℝ 1 (fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) (spaceTimeSet Set.univ (Set.Ioc 0 T))) (hMild : ∀ (t : ℝ) (ht : t ∈ Set.Icc 0 T), realVectorL2OfCoordinateFunction (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) ⋯ = realHeatOperator t ⋯ (realVectorL2OfCoordinateFunction (regUniformMollifiedInitial ρ ε hε a) ⋯) - regularizedMildStokesIntegral (regularizedMildTensorTrajectory ρ ε hε fun (s : ℝ) => realVectorL2OfCoordinateFunction (fun (x : Foundation.Parabolic.Vec3) => u (x, ↑(regularizedMildTimeClamp T ⋯ s))) ⋯) t) (t : ℝ) : t ∈ Set.Icc 0 T → MeasureTheory.eLpNorm (regUniformVelocitySlice u t) 2 MeasureTheory.volume ^ 2 + 2 * regUniformDissipation u (fun (z : Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j z) t = MeasureTheory.eLpNorm (regMollifyVector ρ ε hε (regUniformSpatialField a)) 2 MeasureTheory.volume ^ 2

The energy equality (R5) of thm:regularised on [0, T] from the hypotheses its proof uses: square-integrable, divergence-free slices depending continuously on time, spatial derivatives continuous at positive times, joint continuous differentiability at positive times, and the mild equation eq:reg-mild with the mollified datum.

theorem CKN.Leray.regularised_R5_on_interval (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (T : ℝ) (hT : 0 < T) (hSlice : ∀ t ∈ Set.Icc 0 T, MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume) (hL2Continuous : Continuous fun (t : ↑(Set.Icc 0 T)) => realVectorL2OfCoordinateFunction (fun (x : Foundation.Parabolic.Vec3) => u (x, ↑t)) ⋯) (hDivFree : ∀ t ∈ Set.Icc 0 T, IsWeakDivFreeL2 fun (x : Foundation.Parabolic.Vec3) => u (x, t)) (hDcontinuous : ∀ (i j : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j z) (spaceTimeSet Set.univ (Set.Ioc 0 T))) (hUjoint : ∀ (i : Fin 3), ContDiffOn ℝ 1 (fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) (spaceTimeSet Set.univ (Set.Ioc 0 T))) (hMild : ∀ (t : ℝ) (ht : t ∈ Set.Icc 0 T), realVectorL2OfCoordinateFunction (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) ⋯ = realHeatOperator t ⋯ (realVectorL2OfCoordinateFunction (regUniformMollifiedInitial ρ ε hε a) ⋯) - regularizedMildStokesIntegral (regularizedMildTensorTrajectory ρ ε hε fun (s : ℝ) => realVectorL2OfCoordinateFunction (fun (x : Foundation.Parabolic.Vec3) => u (x, ↑(regularizedMildTimeClamp T ⋯ s))) ⋯) t) (t : ℝ) : t ∈ Set.Icc 0 T → MeasureTheory.eLpNorm (regUniformVelocitySlice u t) 2 MeasureTheory.volume ^ 2 + 2 * regUniformDissipation u (fun (z : Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j z) t = MeasureTheory.eLpNorm (regMollifyVector ρ ε hε (regUniformSpatialField a)) 2 MeasureTheory.volume ^ 2

The energy equality (R5) of thm:regularised on the interval [0, T], for the regularized mild solution with the mollified datum.