The forced regularized solutions

lem:regularised-forced: for every divergence-free datum in J, every locally square-integrable force and every ε > 0, the forced regularized problem has a velocity, a weak gradient and a pressure with the slice continuity, initial datum and divergence freedom of the velocity, the weak gradient on almost every positive time slice, square integrability of the gradient and of the quadratic pressure on bounded slabs, the Riesz representation and Laplacian identity of the quadratic pressure on every positive time slice, and the energy inequality eq:reg-energy-forced. The pressure is the quadratic Riesz pressure plus the force pressure of lem:force-pressure.

noncomputable def CKN.Leray.forcedRegVelocity (ρ : RegMollifierProfile) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hf : IsLocallySquareIntegrableForce f) (ε : ℝ) : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3

The velocity of the forced regularized problem, set to zero when ε ≤ 0.

Equations

• CKN.Leray.forcedRegVelocity ρ a ha f hf ε = if hε : 0 < ε then CKN.Leray.forcedRegRep ρ ε hε ha hf else 0

noncomputable def CKN.Leray.forcedRegGradient (ρ : RegMollifierProfile) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hf : IsLocallySquareIntegrableForce f) (ε : ℝ) : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3

The weak gradient field of the forced regularized velocity.

Equations

• CKN.Leray.forcedRegGradient ρ a ha f hf ε = CKN.Leray.forcedMollifiedGrad (CKN.Leray.forcedRegVelocity ρ a ha f hf ε)

noncomputable def CKN.Leray.forcedRegPressure (ρ : RegMollifierProfile) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hf : IsLocallySquareIntegrableForce f) (ε : ℝ) : Foundation.Parabolic.ParabolicPoint → ℝ

The pressure of the forced regularized problem: the quadratic Riesz pressure plus the force pressure, set to zero when ε ≤ 0.

Equations

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

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

theorem CKN.Leray.forcedRegPressure_sub (ρ : RegMollifierProfile) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) {ε : ℝ} (hε : 0 < ε) (z : Foundation.Parabolic.ParabolicPoint) : forcedRegPressure ρ a ha f hf ε z - forcePressure f hf z = forcedQuadPressure ρ ε hε (forcedRegCurve ρ ε hε ha hf) z

theorem CKN.Leray.forcedRegPressure_sub_apply (ρ : RegMollifierProfile) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) {ε : ℝ} (hε : 0 < ε) (x : Foundation.Parabolic.Vec3) (t : ℝ) : forcedRegPressure ρ a ha f hf ε (x, t) - forcePressure f hf (x, t) = forcedQuadPressure ρ ε hε (forcedRegCurve ρ ε hε ha hf) (x, t)

theorem CKN.Leray.forcedRegRep_pressureSlice (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) (t : ℝ) : ∃ (hF : ∀ (i j : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => regUniformMollifiedVelocity ρ ε hε (forcedRegRep ρ ε hε ha hf) (x, t) i * forcedRegRep ρ ε hε ha hf (x, t) j) (ENNReal.ofReal 2) MeasureTheory.volume), ((fun (x : Foundation.Parabolic.Vec3) => forcedQuadPressure ρ ε hε (forcedRegCurve ρ ε hε ha hf) (x, t)) =ᵐ[MeasureTheory.volume] rieszPressureSliceRepresentative 2 forcedRegRep_pressureSlice._proof_1 fun (i j : Fin 3) => MeasureTheory.MemLp.toLp (fun (x : Foundation.Parabolic.Vec3) => regUniformMollifiedVelocity ρ ε hε (forcedRegRep ρ ε hε ha hf) (x, t) i * forcedRegRep ρ ε hε ha hf (x, t) j) ⋯) ∧ ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∫ (x : Foundation.Parabolic.Vec3), forcedQuadPressure ρ ε hε (forcedRegCurve ρ ε hε ha hf) (x, t) * spatialLaplacian ψ x = -∑ i : Fin 3, ∑ j : Fin 3, ∫ (x : Foundation.Parabolic.Vec3), regUniformMollifiedVelocity ρ ε hε (forcedRegRep ρ ε hε ha hf) (x, t) i * forcedRegRep ρ ε hε ha hf (x, t) j * mixedSecond ψ i j x

On every time slice the quadratic pressure is the Riesz pressure of the regularized tensor and satisfies its Laplacian identity.

theorem CKN.Leray.forcedRegRep_work (ρ : 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) : ∫ (s : ℝ) in Set.Ioc 0 t, inner ℝ (forcedRegCurve ρ ε hε ha hf s) (forcedForceSlice (forcedForceMod f hf) s) = ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 t), ∑ i : Fin 3, f z i * forcedRegRep ρ ε hε ha hf z i

The work of the force on (0, t) for t ≥ 0.

theorem CKN.Leray.forcedRegRep_energyClause (ρ : 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) : MeasureTheory.eLpNorm (regUniformVelocitySlice (forcedRegRep ρ ε hε ha hf) t) 2 MeasureTheory.volume ^ 2 + 2 * regUniformDissipation (forcedRegRep ρ ε hε ha hf) (forcedMollifiedGrad (forcedRegRep ρ ε hε ha hf)) t < ⊤ ∧ (MeasureTheory.eLpNorm (regUniformVelocitySlice (forcedRegRep ρ ε hε ha hf) t) 2 MeasureTheory.volume ^ 2 + 2 * regUniformDissipation (forcedRegRep ρ ε hε ha hf) (forcedMollifiedGrad (forcedRegRep ρ ε hε ha hf)) 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 * forcedRegRep ρ ε hε ha hf z i

eq:reg-energy-forced in the form of lem:regularised-forced.

theorem CKN.Leray.forcedRegularised (ρ : RegMollifierProfile) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hf : IsLocallySquareIntegrableForce f) (ε : ℝ) (hε : 0 < ε) : have u := forcedRegVelocity ρ a ha f hf ε; have Du := forcedRegGradient ρ a ha f hf ε; have p := forcedRegPressure ρ a ha f hf ε; (∃ (hSlice : ∀ (t : ℝ), 0 ≤ t → MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume), (Continuous fun (t : ↑(Set.Ici 0)) => realVectorL2OfCoordinateFunction (fun (x : Foundation.Parabolic.Vec3) => u (x, ↑t)) ⋯) ∧ (fun (x : Foundation.Parabolic.Vec3) => u (x, 0)) =ᵐ[MeasureTheory.volume] regUniformMollifiedInitial ρ ε hε a ∧ ∀ (t : ℝ), 0 ≤ t → IsWeakDivFreeL2 fun (x : Foundation.Parabolic.Vec3) => u (x, t)) ∧ (∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioi 0), ∀ (i : Fin 3), HasWeakGradientOn Set.univ (fun (x : Vec 3) => u (x, t) i) fun (x : Vec 3) => Du (x, t) i) ∧ (∀ (T : ℝ), 0 < T → MeasureTheory.MemLp Du 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T))) ∧ MeasureTheory.MemLp (fun (z : Foundation.Parabolic.ParabolicPoint) => p z - forcePressure f hf z) 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) ∧ (∀ (t : ℝ), 0 < t → ∃ (hF : ∀ (i j : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => regUniformMollifiedVelocity ρ ε hε u (x, t) i * u (x, t) j) (ENNReal.ofReal 2) MeasureTheory.volume), ((fun (x : Foundation.Parabolic.Vec3) => p (x, t) - forcePressure f hf (x, t)) =ᵐ[MeasureTheory.volume] rieszPressureSliceRepresentative 2 forcedRegRep_pressureSlice._proof_1 fun (i j : Fin 3) => MeasureTheory.MemLp.toLp (fun (x : Foundation.Parabolic.Vec3) => regUniformMollifiedVelocity ρ ε hε u (x, t) i * u (x, t) j) ⋯) ∧ ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∫ (x : Foundation.Parabolic.Vec3), (p (x, t) - forcePressure f hf (x, t)) * spatialLaplacian ψ x = -∑ i : Fin 3, ∑ j : Fin 3, ∫ (x : Foundation.Parabolic.Vec3), regUniformMollifiedVelocity ρ ε hε u (x, t) i * u (x, t) j * mixedSecond ψ i j x) ∧ ∀ (t : ℝ), 0 ≤ t → MeasureTheory.eLpNorm (regUniformVelocitySlice u t) 2 MeasureTheory.volume ^ 2 + 2 * regUniformDissipation u Du 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

lem:regularised-forced: the forced regularized solutions, with the force pressure of lem:force-pressure, have the slice, gradient, pressure and energy properties used by the limiting argument of thm:leray-forced.