The limit of the regularized solutions is a Leray–Hopf solution #
This is prop:leray-hopf-limit: for the subsequence and limit fields of
prop:leray-limit, and every T > 0, the limit satisfies the clauses
(LH1)–(LH5) of def:leray-hopf on ℝ³ × [0,T]. The inputs are the
regularized solutions of thm:regularised with their energy equality, the
regularized momentum identity of lem:reg-momentum, and the convergence
statements of prop:leray-limit.
theorem
CKN.Leray.lerayHopfLimit
(ρ : RegMollifierProfile)
(uε :
(a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) →
IsInJ a → ℝ → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(pε :
(a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) → IsInJ a → ℝ → Foundation.Parabolic.ParabolicPoint → ℝ)
(hregularised :
∀ (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (ε : ℝ) (hε : 0 < ε),
lerayAssemblyRegularisedConditions ρ uε pε a ha ε hε)
(hregMomentum :
∀ (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (ε : ℝ) (hε : 0 < ε),
∀ φ ∈ spaceTimeTestFunction Set.univ (Set.Ioi 0),
∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioi 0), -∑ i : Fin 3, uε a ha ε z i * timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) z - ∑ i : Fin 3,
∑ j : Fin 3,
regUniformMollifiedVelocity ρ ε hε (uε a ha ε) z j * uε a ha ε z i * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) j z + ∑ i : Fin 3,
∑ j : Fin 3,
spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => uε a ha ε y i) j z * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) j z - pε a ha ε z * ∑ i : Fin 3, spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) i z = 0)
(hlerayLimit : lerayAssemblyCompactnessLimitContract ρ uε)
(a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3)
(ha : IsInJ a)
(εseq : ℕ → ℝ)
(hseq : ∀ (n : ℕ), 0 < εseq n ∧ εseq n ≤ 1)
(hεseq : Filter.Tendsto εseq Filter.atTop (nhds 0))
:
have hlim := ⋯;
have _σ := Classical.choose hlim;
have hlim₁ := ⋯;
have u := Classical.choose hlim₁;
have hlim₂ := ⋯;
have Du := Classical.choose hlim₂;
∀ (T : ℝ), 0 < T → IsLerayHopfSolution T a u Du
prop:leray-hopf-limit: the limit fields of prop:leray-limit are, on
every finite slab, a Leray–Hopf solution with the given initial datum.