Time smoothness of the projected Navier–Stokes evolution

prop:lps-smoothing: slot data of a velocity field that are Sobolev families of every order, continuous in time in L², consistent across orders, and that solve the Leray-projected Navier–Stokes equation ∂ₜ u = Δu - P(u · ∇u) weakly in time, have time derivatives of every order. For each j and each word α, the slot α of ∂ₜ^j u is an L²-continuous curve on the closed interval whose test pairings are differentiable with the pairings of ∂ₜ^(j+1) u as derivatives. The tower curves are C^∞ by lps_ode_tower_contDiffOn, and the slots of their iterated derivatives are the required data.

noncomputable def ESS.lpsFieldInclCLM (n : ℕ) : (Fin 3 → ↥(lpsSobolevSpace (n + 1 + 1))) →L[ℝ] Fin 3 → ↥(lpsSobolevSpace (n + 1))

The inclusion H^(n+2) → H^(n+1) of vector fields (prop:lps-smoothing).

Equations

• ESS.lpsFieldInclCLM n = ContinuousLinearMap.pi fun (i : Fin 3) => ESS.lpsInclCLM (n + 1) ∘SL ContinuousLinearMap.proj i

noncomputable def ESS.lpsTimeChainSlots (a T : ℝ) (Zm : ℕ → Fin 3 → ℝ → List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ) (hfam : ∀ (m : ℕ) (i : Fin 3) (t : ℝ), CKN.IsSobolevFamilyOn m Set.univ (Zm m i t []) (Zm m i t)) (j : ℕ) (i : Fin 3) (t : ℝ) (α : List (Fin 3)) : CKN.Foundation.Parabolic.Vec3 → ℝ

The slot α of the j-th time derivative of the i-th velocity component at time t, read off the tower curve of level α.length + 1 (prop:lps-smoothing).

Equations

• ESS.lpsTimeChainSlots a T Zm hfam j i t α = ↑↑((ESS.lpsSlotCLM (α.length + 1) α) (iteratedDerivWithin j (ESS.lpsTowerCurve Zm hfam α.length) (Set.Icc a T) t i))

theorem ESS.lps_towerCurve_incl {a T : ℝ} {Zm : ℕ → Fin 3 → ℝ → List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ} (hfam : ∀ (m : ℕ) (i : Fin 3) (t : ℝ), CKN.IsSobolevFamilyOn m Set.univ (Zm m i t []) (Zm m i t)) (hcons : ∀ (m m' : ℕ) (i : Fin 3) (α : List (Fin 3)), α.length ≤ m → α.length ≤ m' → ∀ t ∈ Set.Icc a T, Zm m i t α =ᵐ[MeasureTheory.volume] Zm m' i t α) (n : ℕ) : Set.EqOn (lpsTowerCurve Zm hfam n) (⇑(lpsFieldInclCLM n) ∘ lpsTowerCurve Zm hfam (n + 1)) (Set.Icc a T)

Consecutive tower curves are related by the inclusion (prop:lps-smoothing).

theorem ESS.lps_towerCurve_iteratedDeriv_incl {a T : ℝ} {Zm : ℕ → Fin 3 → ℝ → List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ} (hab : a < T) (hfam : ∀ (m : ℕ) (i : Fin 3) (t : ℝ), CKN.IsSobolevFamilyOn m Set.univ (Zm m i t []) (Zm m i t)) (hcons : ∀ (m m' : ℕ) (i : Fin 3) (α : List (Fin 3)), α.length ≤ m → α.length ≤ m' → ∀ t ∈ Set.Icc a T, Zm m i t α =ᵐ[MeasureTheory.volume] Zm m' i t α) (hsmooth : ∀ (k n : ℕ), ContDiffOn ℝ (↑k) (lpsTowerCurve Zm hfam n) (Set.Icc a T)) (n j : ℕ) {t : ℝ} (ht : t ∈ Set.Icc a T) : iteratedDerivWithin j (lpsTowerCurve Zm hfam n) (Set.Icc a T) t = (lpsFieldInclCLM n) (iteratedDerivWithin j (lpsTowerCurve Zm hfam (n + 1)) (Set.Icc a T) t)

The iterated time derivatives of consecutive tower curves are related by the inclusion (prop:lps-smoothing).

theorem ESS.lps_towerCurve_slot_level {a T : ℝ} {Zm : ℕ → Fin 3 → ℝ → List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ} (hab : a < T) (hfam : ∀ (m : ℕ) (i : Fin 3) (t : ℝ), CKN.IsSobolevFamilyOn m Set.univ (Zm m i t []) (Zm m i t)) (hcons : ∀ (m m' : ℕ) (i : Fin 3) (α : List (Fin 3)), α.length ≤ m → α.length ≤ m' → ∀ t ∈ Set.Icc a T, Zm m i t α =ᵐ[MeasureTheory.volume] Zm m' i t α) (hsmooth : ∀ (k n : ℕ), ContDiffOn ℝ (↑k) (lpsTowerCurve Zm hfam n) (Set.Icc a T)) (j : ℕ) (i : Fin 3) {t : ℝ} (ht : t ∈ Set.Icc a T) (α : List (Fin 3)) (n : ℕ) : α.length ≤ n → (lpsSlotCLM (n + 1) α) (iteratedDerivWithin j (lpsTowerCurve Zm hfam n) (Set.Icc a T) t i) = (lpsSlotCLM (α.length + 1) α) (iteratedDerivWithin j (lpsTowerCurve Zm hfam α.length) (Set.Icc a T) t i)

The slot α of an iterated time derivative does not depend on the level of the tower curve it is read from (prop:lps-smoothing).

theorem ESS.lps_timeChainSlots_family {a T : ℝ} {Zm : ℕ → Fin 3 → ℝ → List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ} (hab : a < T) (hfam : ∀ (m : ℕ) (i : Fin 3) (t : ℝ), CKN.IsSobolevFamilyOn m Set.univ (Zm m i t []) (Zm m i t)) (hcons : ∀ (m m' : ℕ) (i : Fin 3) (α : List (Fin 3)), α.length ≤ m → α.length ≤ m' → ∀ t ∈ Set.Icc a T, Zm m i t α =ᵐ[MeasureTheory.volume] Zm m' i t α) (hsmooth : ∀ (k n : ℕ), ContDiffOn ℝ (↑k) (lpsTowerCurve Zm hfam n) (Set.Icc a T)) (j : ℕ) (i : Fin 3) {t : ℝ} (ht : t ∈ Set.Icc a T) (m : ℕ) : CKN.IsSobolevFamilyOn m Set.univ (lpsTimeChainSlots a T Zm hfam j i t []) (lpsTimeChainSlots a T Zm hfam j i t)

The extracted slots are Sobolev families of every order (prop:lps-smoothing).

theorem ESS.lps_timeChainSlots_tendsto {a T : ℝ} {Zm : ℕ → Fin 3 → ℝ → List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ} (hab : a < T) (hfam : ∀ (m : ℕ) (i : Fin 3) (t : ℝ), CKN.IsSobolevFamilyOn m Set.univ (Zm m i t []) (Zm m i t)) (hsmooth : ∀ (k n : ℕ), ContDiffOn ℝ (↑k) (lpsTowerCurve Zm hfam n) (Set.Icc a T)) (j : ℕ) (i : Fin 3) (α : List (Fin 3)) {t : ℝ} (ht : t ∈ Set.Icc a T) : Filter.Tendsto (fun (s : ℝ) => MeasureTheory.eLpNorm (lpsTimeChainSlots a T Zm hfam j i s α - lpsTimeChainSlots a T Zm hfam j i t α) 2 MeasureTheory.volume) (nhdsWithin t (Set.Icc a T)) (nhds 0)

The extracted slots are continuous in time in L² (prop:lps-smoothing).

theorem ESS.lps_timeChainSlots_hasDerivWithinAt {a T : ℝ} {Zm : ℕ → Fin 3 → ℝ → List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ} (hab : a < T) (hfam : ∀ (m : ℕ) (i : Fin 3) (t : ℝ), CKN.IsSobolevFamilyOn m Set.univ (Zm m i t []) (Zm m i t)) (hsmooth : ∀ (k n : ℕ), ContDiffOn ℝ (↑k) (lpsTowerCurve Zm hfam n) (Set.Icc a T)) (j : ℕ) (i : Fin 3) (α : List (Fin 3)) {ψ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) {t : ℝ} (ht : t ∈ Set.Icc a T) : HasDerivWithinAt (fun (s : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), lpsTimeChainSlots a T Zm hfam j i s α x * ψ x) (∫ (x : CKN.Foundation.Parabolic.Vec3), lpsTimeChainSlots a T Zm hfam (j + 1) i t α x * ψ x) (Set.Icc a T) t

The test pairings of the extracted slots are differentiable in time, with the pairings of the next time derivative as derivatives (prop:lps-smoothing).

theorem ESS.lps_timeChainSlots_zero {a T : ℝ} {Zm : ℕ → Fin 3 → ℝ → List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ} (hfam : ∀ (m : ℕ) (i : Fin 3) (t : ℝ), CKN.IsSobolevFamilyOn m Set.univ (Zm m i t []) (Zm m i t)) (hcons : ∀ (m m' : ℕ) (i : Fin 3) (α : List (Fin 3)), α.length ≤ m → α.length ≤ m' → ∀ t ∈ Set.Icc a T, Zm m i t α =ᵐ[MeasureTheory.volume] Zm m' i t α) {t : ℝ} (ht : t ∈ Set.Icc a T) (i : Fin 3) : lpsTimeChainSlots a T Zm hfam 0 i t [] =ᵐ[MeasureTheory.volume] Zm 0 i t []

The order-zero slot of the order-zero time derivative is the velocity data (prop:lps-smoothing).

theorem ESS.lps_time_chain_of_family {a T : ℝ} (hab : a < T) {u Dtu : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (Zm : ℕ → Fin 3 → ℝ → List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ) (hfam : ∀ (m : ℕ) (i : Fin 3) (t : ℝ), CKN.IsSobolevFamilyOn m Set.univ (Zm m i t []) (Zm m i t)) (hcont : ∀ (m : ℕ) (i : Fin 3) (α : List (Fin 3)), α.length ≤ m → ∀ t ∈ Set.Icc a T, Filter.Tendsto (fun (s : ℝ) => MeasureTheory.eLpNorm (Zm m i s α - Zm m i t α) 2 MeasureTheory.volume) (nhdsWithin t (Set.Icc a T)) (nhds 0)) (hcons : ∀ (m m' : ℕ) (i : Fin 3) (α : List (Fin 3)), α.length ≤ m → α.length ≤ m' → ∀ t ∈ Set.Icc a T, Zm m i t α =ᵐ[MeasureTheory.volume] Zm m' i t α) (hae : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a T), ∀ (i : Fin 3), Zm 0 i t [] =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t) i) (htw : ∀ (i : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∀ (s t : ℝ), a ≤ s → s ≤ t → t ≤ T → (∫ (x : CKN.Foundation.Parabolic.Vec3), Zm 0 i t [] x * ψ x) - ∫ (x : CKN.Foundation.Parabolic.Vec3), Zm 0 i s [] x * ψ x = ∫ (τ : ℝ) in s..t, ∫ (x : CKN.Foundation.Parabolic.Vec3), Dtu (x, τ) i * ψ x) (hequ : ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a T), ∀ (i : Fin 3) (hg : ∀ (i' : Fin 3), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => ∑ j : Fin 3, Zm 1 j τ [] x * Zm 1 i' τ [j] x) 2 MeasureTheory.volume), (fun (x : CKN.Foundation.Parabolic.Vec3) => Dtu (x, τ) i) =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => ∑ k : Fin 3, Zm 2 i τ [k, k] x - lpsLerayApply (fun (i' : Fin 3) (x : CKN.Foundation.Parabolic.Vec3) => ∑ j : Fin 3, Zm 1 j τ [] x * Zm 1 i' τ [j] x) hg i x) : ∃ (Z : ℕ → Fin 3 → ℝ → List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ), (∀ (i : Fin 3) (j : ℕ), ∀ t ∈ Set.Icc a T, ∀ (m : ℕ), CKN.IsSobolevFamilyOn m Set.univ (Z j i t []) (Z j i t)) ∧ (∀ (i : Fin 3) (j : ℕ) (α : List (Fin 3)), ∀ t ∈ Set.Icc a T, Filter.Tendsto (fun (s : ℝ) => MeasureTheory.eLpNorm (Z j i s α - Z j i t α) 2 MeasureTheory.volume) (nhdsWithin t (Set.Icc a T)) (nhds 0)) ∧ (∀ (i : Fin 3) (j : ℕ) (α : List (Fin 3)) (ψ : CKN.Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∀ t ∈ Set.Icc a T, HasDerivWithinAt (fun (s : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), Z j i s α x * ψ x) (∫ (x : CKN.Foundation.Parabolic.Vec3), Z (j + 1) i t α x * ψ x) (Set.Icc a T) t) ∧ ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a T), ∀ (i : Fin 3), Z 0 i t [] =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t) i

Time chain of the projected Navier–Stokes evolution for slot data defined at all times (prop:lps-smoothing): the statement of lps_time_chain with the family hypothesis at every time.

theorem ESS.lps_time_chain {a T : ℝ} (hab : a < T) {u Dtu : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (Zm : ℕ → Fin 3 → ℝ → List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ) (hfam : ∀ (m : ℕ) (i : Fin 3), ∀ t ∈ Set.Icc a T, CKN.IsSobolevFamilyOn m Set.univ (Zm m i t []) (Zm m i t)) (hcont : ∀ (m : ℕ) (i : Fin 3) (α : List (Fin 3)), α.length ≤ m → ∀ t ∈ Set.Icc a T, Filter.Tendsto (fun (s : ℝ) => MeasureTheory.eLpNorm (Zm m i s α - Zm m i t α) 2 MeasureTheory.volume) (nhdsWithin t (Set.Icc a T)) (nhds 0)) (hcons : ∀ (m m' : ℕ) (i : Fin 3) (α : List (Fin 3)), α.length ≤ m → α.length ≤ m' → ∀ t ∈ Set.Icc a T, Zm m i t α =ᵐ[MeasureTheory.volume] Zm m' i t α) (hae : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a T), ∀ (i : Fin 3), Zm 0 i t [] =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t) i) (htw : ∀ (i : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∀ (s t : ℝ), a ≤ s → s ≤ t → t ≤ T → (∫ (x : CKN.Foundation.Parabolic.Vec3), Zm 0 i t [] x * ψ x) - ∫ (x : CKN.Foundation.Parabolic.Vec3), Zm 0 i s [] x * ψ x = ∫ (τ : ℝ) in s..t, ∫ (x : CKN.Foundation.Parabolic.Vec3), Dtu (x, τ) i * ψ x) (hequ : ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a T), ∀ (i : Fin 3) (hg : ∀ (i' : Fin 3), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => ∑ j : Fin 3, Zm 1 j τ [] x * Zm 1 i' τ [j] x) 2 MeasureTheory.volume), (fun (x : CKN.Foundation.Parabolic.Vec3) => Dtu (x, τ) i) =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => ∑ k : Fin 3, Zm 2 i τ [k, k] x - lpsLerayApply (fun (i' : Fin 3) (x : CKN.Foundation.Parabolic.Vec3) => ∑ j : Fin 3, Zm 1 j τ [] x * Zm 1 i' τ [j] x) hg i x) : ∃ (Z : ℕ → Fin 3 → ℝ → List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ), (∀ (i : Fin 3) (j : ℕ), ∀ t ∈ Set.Icc a T, ∀ (m : ℕ), CKN.IsSobolevFamilyOn m Set.univ (Z j i t []) (Z j i t)) ∧ (∀ (i : Fin 3) (j : ℕ) (α : List (Fin 3)), ∀ t ∈ Set.Icc a T, Filter.Tendsto (fun (s : ℝ) => MeasureTheory.eLpNorm (Z j i s α - Z j i t α) 2 MeasureTheory.volume) (nhdsWithin t (Set.Icc a T)) (nhds 0)) ∧ (∀ (i : Fin 3) (j : ℕ) (α : List (Fin 3)) (ψ : CKN.Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∀ t ∈ Set.Icc a T, HasDerivWithinAt (fun (s : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), Z j i s α x * ψ x) (∫ (x : CKN.Foundation.Parabolic.Vec3), Z (j + 1) i t α x * ψ x) (Set.Icc a T) t) ∧ ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a T), ∀ (i : Fin 3), Z 0 i t [] =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t) i

Time chain of the projected Navier–Stokes evolution (prop:lps-smoothing). Slot data Zm m i t of the velocity components that are Sobolev families of every order m, continuous in time in L², consistent across orders, equal to the velocity at almost every time, and that solve ∂ₜ u = Δu - P(u · ∇u) weakly in time, have all time derivatives: there are slots Z j i t α of ∂ₜ^j u_i(t) forming Sobolev families of every order, continuous in time in L² on the closed interval, whose test pairings are differentiable in time with the pairings of Z (j + 1) as derivatives, and with Z 0 i t [] = u(·, t)_i at almost every time.