Slice properties of strong solutions #
These consequences of IsLpsStrongSolution are used when verifying the
Leray–Hopf clauses (def:leray-hopf).
theorem
ESS.lps_strong_solution_good_time
{t₀ T : ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
(hU : IsLpsStrongSolution t₀ T u Du p)
{t : ℝ}
(ht : t ∈ Set.Icc t₀ T)
:
IsLpsGoodTime u Du t
Every closed-interval slice of a strong solution is suitable as local
strong data (prop:lps-local-strong).
theorem
ESS.lps_strong_solution_slice_memLp_two
{t₀ T : ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
(hU : IsLpsStrongSolution t₀ T u Du p)
{t : ℝ}
(ht : t ∈ Set.Icc t₀ T)
:
MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume ∧ MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => Du (x, t)) 2 MeasureTheory.volume
The velocity and its specified gradient are square integrable on every
closed-interval slice (prop:lps-local-strong).
theorem
ESS.lps_strong_solution_slice_weak_gradient
{t₀ T : ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
(hU : IsLpsStrongSolution t₀ T u Du p)
{t : ℝ}
(ht : t ∈ Set.Icc t₀ T)
(i : Fin 3)
:
CKN.HasWeakGradientOn Set.univ (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t) i)
fun (x : CKN.Foundation.Parabolic.Vec3) => Du (x, t) i
The specified gradient on a strong slice is its weak gradient
(prop:lps-local-strong).
theorem
ESS.lps_strong_solution_slice_weak_div_free
{t₀ T : ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
(hU : IsLpsStrongSolution t₀ T u Du p)
{t : ℝ}
(ht : t ∈ Set.Icc t₀ T)
:
CKN.IsWeakDivFreeL2 fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t)
Every strong slice is weakly divergence free (prop:lps-local-strong).
theorem
ESS.lps_strong_solution_initial_trace
{t₀ T : ℝ}
{b : 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}
{p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
(hU : IsLpsStrongSolution t₀ T u Du p)
(hTrace : (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t₀)) =ᵐ[MeasureTheory.volume] b)
:
Filter.Tendsto
(fun (t : ℝ) =>
MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t₀ + t) - b x) 2 MeasureTheory.volume)
(nhdsWithin 0 (Set.Ioi 0)) (nhds 0)
The a.e. initial representative agrees with the strong right L² trace
(prop:lps-local-strong).