The velocity as a curve in the Sobolev tower

prop:lps-smoothing: slot data of a velocity field that are square-integrable Sobolev families of every order, continuous in time in L², and satisfy the projected Navier–Stokes equation weakly in time, define continuous curves c_n : [a, T] → H^(n+1) that solve c_n(t) - c_n(s) = ∫_s^t N(c_(n+2)(τ)) dτ in every space of the tower.

noncomputable def ESS.lpsTowerCurve (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)) (n : ℕ) (t : ℝ) : Fin 3 → ↥(lpsSobolevSpace (n + 1))

The curve of the level-(n+1) slot vectors of the velocity data (prop:lps-smoothing).

Equations

• ESS.lpsTowerCurve Zm hfam n t i = ESS.lpsSobolevOf (n + 1) (Zm (n + 1) i t) ⋯

theorem ESS.lps_coeFn_sum_three (X : Fin 3 → ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)) : ↑↑(∑ k : Fin 3, X k) =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => ∑ k : Fin 3, ↑↑(X k) x

A sum of three L² classes is represented by the sum of representatives (prop:lps-smoothing).

theorem ESS.lps_towerCurve_memLp {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)) {m : ℕ} (i : Fin 3) (t : ℝ) {α : List (Fin 3)} (hα : α.length ≤ m) : MeasureTheory.MemLp (Zm m i t α) 2 MeasureTheory.volume

The slots of the velocity data are square integrable (prop:lps-smoothing).

theorem ESS.lps_towerCurve_slot {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)) (n : ℕ) (i : Fin 3) (t : ℝ) {α : List (Fin 3)} (hα : α.length ≤ n + 1) : (lpsSlotCLM (n + 1) α) (lpsTowerCurve Zm hfam n t i) = MeasureTheory.MemLp.toLp (Zm (n + 1) i t α) ⋯

The slots of the tower curve are the L² classes of the slot data (prop:lps-smoothing).

theorem ESS.lps_towerCurve_continuousOn {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)) (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)) (n : ℕ) : ContinuousOn (lpsTowerCurve Zm hfam n) (Set.Icc a T)

The tower curves are continuous on the closed interval (prop:lps-smoothing).

theorem ESS.lps_towerCurve_NS_slot_ae {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 : ℕ) {τ : ℝ} (hτ : τ ∈ Set.Icc a T) : ∃ (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), ∀ (i : Fin 3), ↑↑((lpsSlotCLM (n + 1) []) (lpsNSMap n (lpsTowerCurve Zm hfam (n + 2) τ) 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

The order-zero slot of the projected Navier–Stokes right-hand side along the tower curve is almost everywhere the right-hand side computed from the slot data (prop:lps-smoothing); the convection term computed from the slot data is square integrable.

theorem ESS.lps_towerCurve_pair {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 : ℕ) (i : Fin 3) {t : ℝ} (ht : t ∈ Set.Icc a T) {φ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hφ : MeasureTheory.MemLp φ 2 MeasureTheory.volume) : (lpsPairCLM φ hφ) ((lpsSlotCLM (n + 1) []) (lpsTowerCurve Zm hfam n t i)) = ∫ (x : CKN.Foundation.Parabolic.Vec3), Zm 0 i t [] x * φ x

The pairing of the order-zero slot of the tower curve with a test function is the pairing of the velocity data (prop:lps-smoothing).

theorem ESS.lps_towerCurve_integral {a T : ℝ} {Zm : ℕ → Fin 3 → ℝ → List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ} {Dtu : CKN.Foundation.Parabolic.ParabolicPoint → 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 α) (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) (n : ℕ) (s : ℝ) : s ∈ Set.Icc a T → ∀ t ∈ Set.Icc a T, s ≤ t → lpsTowerCurve Zm hfam n t - lpsTowerCurve Zm hfam n s = ∫ (τ : ℝ) in s..t, lpsNSMap n (lpsTowerCurve Zm hfam (n + 2) τ)

The tower curves solve the projected Navier–Stokes equation in integral form in every space of the tower (prop:lps-smoothing).