Good Times #
A positive-time slice in H¹ ∩ J with the specified weak gradient,
as in lem:lps-good-times.
def
ESS.IsLpsGoodTime
(u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3)
(Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3)
(t : ℝ)
:
A positive-time slice in H¹ ∩ J with the specified weak gradient,
as in lem:lps-good-times.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
ESS.lps_good_times_ae
{T : ℝ}
{a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
(hLH : CKN.IsLerayHopfSolution T a u Du)
:
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), IsLpsGoodTime u Du t
Almost every positive-time slice of a Leray--Hopf field belongs to
H¹ ∩ J, with weak gradient Du (lem:lps-good-times).
theorem
ESS.lps_good_time_in_interval
{T : ℝ}
{a₀ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
(hLH : CKN.IsLerayHopfSolution T a₀ u Du)
{a b : ℝ}
(ha : 0 ≤ a)
(hab : a < b)
(hb : b ≤ T)
:
∃ t ∈ Set.Ioo a b, IsLpsGoodTime u Du t
Every nonempty interval inside [0,T] contains a time whose slice is in
H¹ ∩ J with weak gradient Du (lem:lps-good-times).
theorem
ESS.lps_weak_l2_continuity_and_initial_trace
{T : ℝ}
{a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
(hLH : CKN.IsLerayHopfSolution T a u Du)
:
(∀ (w : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3),
MeasureTheory.MemLp w 2 MeasureTheory.volume →
ContinuousOn (fun (t : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, u (x, t) i * w x i)
(Set.Icc 0 T)) ∧ Filter.Tendsto
(fun (t : ℝ) =>
MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t) - a x) 2 MeasureTheory.volume)
(nhdsWithin 0 (Set.Ioi 0) ⊓ MeasureTheory.ae (MeasureTheory.volume.restrict (Set.Ioo 0 T))) (nhds 0)
Weak L² continuity of the prescribed slices and strong convergence to the
initial datum in L² along almost every positive-time slice. The strong trace
is the one in (LH5) of def:leray-hopf; this theorem gives its a.e.-slice
consequence, while lem:lps-good-times supplies the good slices.