Global L² trace of the regularized mild solution

The coordinate representative of the global mild curve has the spatial L² continuity, initial trace, and weak divergence properties in (R1).

noncomputable def CKN.Leray.regularizedGlobalMildField (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : ↥RealVectorL2) (hb : RegularizedMildJData b) : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3

The coordinate field of the global zero-force mild curve.

Equations

• CKN.Leray.regularizedGlobalMildField ρ ε hε b hb z = CKN.Leray.realVectorL2Representative (CKN.Leray.regularizedGlobalMildCurve ρ ε hε b hb z.2) z.1

theorem CKN.Leray.regularizedGlobalMildField_R1_and_mild (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : ↥RealVectorL2) (hb : RegularizedMildJData b) : have u := regularizedGlobalMildField ρ ε hε b hb; ∃ (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] realVectorL2Representative b ∧ (∀ (t : ℝ), 0 ≤ t → IsWeakDivFreeL2 fun (x : Foundation.Parabolic.Vec3) => u (x, t)) ∧ ∀ (t : ℝ) (ht : 0 ≤ t), realVectorL2OfCoordinateFunction (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) ⋯ = realHeatOperator t ht b - regularizedMildStokesIntegral (regularizedMildTensorTrajectory ρ ε hε (regularizedGlobalMildCurve ρ ε hε b hb)) t

The global mild field has continuous divergence-free spatial L² slices and satisfies its own Duhamel identity at all nonnegative times.

theorem CKN.Leray.regUniformMollifiedInitial_globalR1 (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) : let b := realVectorL2OfCoordinateFunction (regUniformMollifiedInitial ρ ε hε a) ⋯; have u := regularizedGlobalMildField ρ ε hε b ⋯; ∃ (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)

Mollified Leray data give the global spatial L² trace and initial condition required in (R1).