The forced regularized solution

The solution of eq:reg-mild-forced with the mollified datum and the strongly measurable modification of the force, its jointly measurable space-time representative, and the slice properties of lem:regularised-forced: continuity in L², the initial datum, weak divergence freedom, the weak gradient, the dissipation bound and the energy inequality.

theorem CKN.Leray.forcedRegInitial_memLp (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) : MeasureTheory.MemLp (regUniformMollifiedInitial ρ ε hε a) 2 MeasureTheory.volume

noncomputable def CKN.Leray.forcedRegDatum (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) : ↥RealVectorL2

The mollified datum of the forced regularized problem as a real L² field.

Equations

• CKN.Leray.forcedRegDatum ρ ε hε ha = CKN.Leray.realVectorL2OfCoordinateFunction (CKN.Leray.regUniformMollifiedInitial ρ ε hε a) ⋯

theorem CKN.Leray.forcedRegDatum_rep (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) : realVectorL2Representative (forcedRegDatum ρ ε hε ha) =ᵐ[MeasureTheory.volume] regUniformMollifiedInitial ρ ε hε a

theorem CKN.Leray.forcedRegDatum_mildJData (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) : RegularizedMildJData (forcedRegDatum ρ ε hε ha)

noncomputable def CKN.Leray.forcedRegCurve (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) : ℝ → ↥RealVectorL2

The solution curve of eq:reg-mild-forced with the mollified datum and the force curve of the strongly measurable modification of the force.

Equations

• CKN.Leray.forcedRegCurve ρ ε hε ha hf = CKN.Leray.forcedSolutionCurve ρ ε hε (CKN.Leray.forcedRegDatum ρ ε hε ha) ⋯ ⋯ ⋯

theorem CKN.Leray.continuous_forcedRegCurve (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) : Continuous (forcedRegCurve ρ ε hε ha hf)

noncomputable def CKN.Leray.forcedRegRep (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3

The jointly measurable space-time representative of the forced regularized solution.

Equations

• CKN.Leray.forcedRegRep ρ ε hε ha hf = CKN.Leray.forcedCurveRep (CKN.Leray.forcedRegCurve ρ ε hε ha hf) ⋯

theorem CKN.Leray.forcedRegRep_stronglyMeasurable (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) : MeasureTheory.StronglyMeasurable (forcedRegRep ρ ε hε ha hf)

theorem CKN.Leray.forcedRegRep_slice (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) (t : ℝ) : (fun (x : Foundation.Parabolic.Vec3) => forcedRegRep ρ ε hε ha hf (x, t)) =ᵐ[MeasureTheory.volume] realVectorL2Representative (forcedRegCurve ρ ε hε ha hf t)

theorem CKN.Leray.forcedRegRep_memLp (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) (t : ℝ) : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => forcedRegRep ρ ε hε ha hf (x, t)) 2 MeasureTheory.volume

theorem CKN.Leray.forcedRegRep_locallyIntegrable (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) (t : ℝ) (i : Fin 3) : MeasureTheory.LocallyIntegrable (fun (y : Foundation.Parabolic.Vec3) => forcedRegRep ρ ε hε ha hf (y, t) i) MeasureTheory.volume

theorem CKN.Leray.forcedRegRep_class (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) (t : ℝ) : realVectorL2OfCoordinateFunction (fun (x : Foundation.Parabolic.Vec3) => forcedRegRep ρ ε hε ha hf (x, t)) ⋯ = forcedRegCurve ρ ε hε ha hf t

theorem CKN.Leray.forcedRegRep_initial (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) : (fun (x : Foundation.Parabolic.Vec3) => forcedRegRep ρ ε hε ha hf (x, 0)) =ᵐ[MeasureTheory.volume] regUniformMollifiedInitial ρ ε hε a

theorem CKN.Leray.forcedRegRep_weakDivFree (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) {t : ℝ} (ht : 0 ≤ t) : IsWeakDivFreeL2 fun (x : Foundation.Parabolic.Vec3) => forcedRegRep ρ ε hε ha hf (x, t)

theorem CKN.Leray.forcedRegRep_weakGradient (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioi 0), ∀ (i : Fin 3), HasWeakGradientOn Set.univ (fun (x : Vec 3) => forcedRegRep ρ ε hε ha hf (x, t) i) fun (x : Vec 3) => forcedMollifiedGrad (forcedRegRep ρ ε hε ha hf) (x, t) i

The weak gradient of the forced regularized solution on almost every positive time slice.

theorem CKN.Leray.forcedRegRep_energy (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) {t : ℝ} (ht : 0 ≤ t) : ∃ (D : ℝ), ∫⁻ (z : Foundation.Parabolic.Vec3 × ℝ), ENNReal.ofReal (spatialGradientSq (forcedRegRep ρ ε hε ha hf) (forcedMollifiedGrad (forcedRegRep ρ ε hε ha hf)) z) ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo 0 t)) ≤ ENNReal.ofReal D ∧ 0 ≤ D ∧ ‖forcedRegCurve ρ ε hε ha hf t‖ ^ 2 + 2 * D ≤ ‖forcedRegDatum ρ ε hε ha‖ ^ 2 + 2 * ∫ (s : ℝ) in Set.Ioc 0 t, inner ℝ (forcedRegCurve ρ ε hε ha hf s) (forcedForceSlice (forcedForceMod f hf) s)

The dissipation bound and the energy inequality of the forced regularized solution up to time t.