Bookkeeping for the limit strong solution #
Square integrability of the components of a good-time slice, scalar weak continuity from the vector
weak continuity of a Leray--Hopf solution, and the replacement of the specified gradient by an
almost everywhere equal field in the space-time weak derivatives and in the equation
(prop:lps-local-strong).
theorem
ESS.LPS.lps_goodTime_memLp
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{t : ℝ}
(h : IsLpsGoodTime u Du t)
(i : Fin 3)
:
MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t) i) 2 MeasureTheory.volume
The components of a good-time slice are square integrable.
theorem
ESS.LPS.lps_weak_continuity_scalar
{T : ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(h :
∀ (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))
(i : Fin 3)
(w : CKN.Foundation.Parabolic.Vec3 → ℝ)
(hw : MeasureTheory.MemLp w 2 MeasureTheory.volume)
:
ContinuousOn (fun (t : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), u (x, t) i * w x) (Set.Icc 0 T)
Scalar weak continuity of a vector field from its vector weak continuity.
theorem
ESS.LPS.lps_hasSpaceTimeWeakDerivs_congr_grad
{I : Set ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Du Du' : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{D2u : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{Dtu : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(h : CKN.HasSpaceTimeWeakDerivs Set.univ I u Du D2u Dtu)
(hae : Du =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ I)] Du')
(hmem : MeasureTheory.MemLp Du' 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ I)))
:
CKN.HasSpaceTimeWeakDerivs Set.univ I u Du' D2u Dtu
The space-time weak derivatives are unchanged when the specified gradient is replaced by an almost everywhere equal square integrable field.
theorem
ESS.LPS.lps_vec3_norm_tendsto
{S : Set ℝ}
{t : ℝ}
{v : ℝ → CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3}
(hmem : ∀ s ∈ S, MeasureTheory.MemLp (v s) 2 MeasureTheory.volume)
(h :
∀ (i : Fin 3),
Filter.Tendsto
(fun (s : ℝ) => MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => v s x i) 2 MeasureTheory.volume)
(nhdsWithin t S) (nhds 0))
:
Filter.Tendsto (fun (s : ℝ) => MeasureTheory.eLpNorm (v s) 2 MeasureTheory.volume) (nhdsWithin t S) (nhds 0)
The L² norm of a vector-valued family tends to zero when its coordinates do.
theorem
ESS.LPS.lps_matrix_norm_tendsto
{S : Set ℝ}
{t : ℝ}
{v : ℝ → CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3}
(hmem : ∀ s ∈ S, MeasureTheory.MemLp (v s) 2 MeasureTheory.volume)
(h :
∀ (i j : Fin 3),
Filter.Tendsto
(fun (s : ℝ) =>
MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => v s x i j) 2 MeasureTheory.volume)
(nhdsWithin t S) (nhds 0))
:
Filter.Tendsto (fun (s : ℝ) => MeasureTheory.eLpNorm (v s) 2 MeasureTheory.volume) (nhdsWithin t S) (nhds 0)
The L² norm of a matrix-valued family tends to zero when its coordinates do.