Documentation

LeanPool.CaffarelliKohnNirenberg.Leray.RegularisedR12FinalAssembly

The slice and regularity properties (R1)–(R2) of thm:regularised #

For the pointwise regularized velocity and the canonical Riesz pressure of the global regularized mild curve, the properties (R1)–(R2) of thm:regularised follow from:

source
theorem CKN.Leray.regR12_R1R2 (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (hPath : ∀ (T : ℝ), 0 ≤ T → ∃ (v : C(↑(RegularizedMildTimeInterval T), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * 2)) 2)), ∀ (t : ↑(RegularizedMildTimeInterval T)), (regularisedBesselSobolevToL2CLM (↑(2 * 2)) regR12_R1R2._proof_109) (v t) = complexifyVectorL2 (regR12Curve ρ ε hε a ha ↑t)) (hPress : have p := forcedQuadPressure ρ ε hε (regR12Curve ρ ε hε a ha); ContinuousOn p (spaceTimeSet Set.univ (Set.Ioi 0)) ∧ (∀ (i : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => p y) i z) (spaceTimeSet Set.univ (Set.Ioi 0))) ∧ (∀ z ∈ spaceTimeSet Set.univ (Set.Ioi 0), DifferentiableAt ℝ (fun (x : Foundation.Parabolic.Vec3) => p (x, z.2)) z.1) ∧ (∀ (δ T : ℝ), 0 < δ → δ < T → ∃ (C : ℝ), 0 ≤ C ∧ ∀ z ∈ spaceTimeSet Set.univ (Set.Icc δ T), |p z| ≤ C ∧ ∀ (i : Fin 3), |spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => p y) i z| ≤ C) ∧ ∀ (δ T : ℝ), 0 < δ → δ < T → MeasureTheory.MemLp p 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo δ T))) ∧ ∀ (i : Fin 3), MeasureTheory.MemLp (fun (z : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => p y) i z) 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo δ T)))) (hTime : ∀ (z : Foundation.Parabolic.ParabolicPoint), 0 < z.2 → ∀ (i : Fin 3), HasDerivAt (fun (s : ℝ) => regR12Velocity ρ ε hε a ha (z.1, s) i) (regR12TimeRHS ρ ε hε (regR12Velocity ρ ε hε a ha) (forcedQuadPressure ρ ε hε (regR12Curve ρ ε hε a ha)) z i) z.2) (hJoint : ∀ (f g : Foundation.Parabolic.ParabolicPoint → ℝ), (∀ z ∈ spaceTimeSet Set.univ (Set.Ioi 0), DifferentiableAt ℝ (fun (x : Foundation.Parabolic.Vec3) => f (x, z.2)) z.1) → (∀ (j : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => spatialPartial f j z) (spaceTimeSet Set.univ (Set.Ioi 0))) → (∀ z ∈ spaceTimeSet Set.univ (Set.Ioi 0), HasDerivAt (fun (s : ℝ) => f (z.1, s)) (g z) z.2) → ContinuousOn g (spaceTimeSet Set.univ (Set.Ioi 0)) → ContDiffOn ℝ 1 f (spaceTimeSet Set.univ (Set.Ioi 0))) :
have u := regR12Velocity ρ ε hε a ha; have p := forcedQuadPressure ρ ε hε (regR12Curve ρ ε hε a ha); have D := fun (z : Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j z; have DD := fun (z : Foundation.Parabolic.ParabolicPoint) (i j k : Fin 3) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (x : Foundation.Parabolic.ParabolicPoint) => u x i) j y) k z; have Dt := fun (z : Foundation.Parabolic.ParabolicPoint) (i : Fin 3) => timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) z; have Dp := fun (z : Foundation.Parabolic.ParabolicPoint) (i : Fin 3) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => p y) i z; (∃ (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)) ∧ (∀ (i : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) (spaceTimeSet Set.univ (Set.Ioi 0))) ∧ (∀ (i j : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => D z i j) (spaceTimeSet Set.univ (Set.Ioi 0))) ∧ (∀ (i j k : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => DD z i j k) (spaceTimeSet Set.univ (Set.Ioi 0))) ∧ (∀ (i : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => Dt z i) (spaceTimeSet Set.univ (Set.Ioi 0))) ∧ ContinuousOn p (spaceTimeSet Set.univ (Set.Ioi 0)) ∧ (∀ (i : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) (spaceTimeSet Set.univ (Set.Ioi 0))) ∧ (∀ (i : Fin 3), ContDiffOn ℝ 1 (fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) (spaceTimeSet Set.univ (Set.Ioi 0))) ∧ (∀ z ∈ spaceTimeSet Set.univ (Set.Ioi 0), ∀ (i j : Fin 3), DifferentiableAt ℝ (fun (x : Foundation.Parabolic.Vec3) => D (x, z.2) i j) z.1) ∧ (∀ z ∈ spaceTimeSet Set.univ (Set.Ioi 0), DifferentiableAt ℝ (fun (x : Foundation.Parabolic.Vec3) => p (x, z.2)) z.1) ∧ (∀ (δ T : ℝ), 0 < δ → δ < T → ∃ (C : ℝ), 0 ≤ C ∧ ∀ z ∈ spaceTimeSet Set.univ (Set.Icc δ T), Foundation.Parabolic.vec3EuclideanNorm (u z) ≤ C ∧ |p z| ≤ C ∧ (∀ (i j : Fin 3), |D z i j| ≤ C) ∧ (∀ (i j k : Fin 3), |DD z i j k| ≤ C) ∧ (∀ (i : Fin 3), |Dt z i| ≤ C) ∧ ∀ (i : Fin 3), |Dp z i| ≤ C) ∧ ∀ (δ T : ℝ), 0 < δ → δ < T → (∀ (i : Fin 3), MeasureTheory.MemLp (fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo δ T)))) ∧ (∀ (i j : Fin 3), MeasureTheory.MemLp (fun (z : Foundation.Parabolic.ParabolicPoint) => D z i j) 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo δ T)))) ∧ (∀ (i j k : Fin 3), MeasureTheory.MemLp (fun (z : Foundation.Parabolic.ParabolicPoint) => DD z i j k) 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo δ T)))) ∧ (∀ (i : Fin 3), MeasureTheory.MemLp (fun (z : Foundation.Parabolic.ParabolicPoint) => Dt z i) 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo δ T)))) ∧ MeasureTheory.MemLp p 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo δ T)))

thm:regularised (R1)–(R2) for the pointwise regularized velocity and the canonical pressure.