Sobolev spaces of slot vectors

prop:lps-smoothing: the space H^M(ℝ³) realized as the closed subspace of the vectors of L²(ℝ³) classes indexed by the ordered derivative words of length at most M whose entries satisfy the weak derivative relations. With the inclusions and the partial derivatives between them, these spaces form the tower of Banach spaces in which the projected Navier–Stokes evolution is smooth in time.

@[reducible, inline]

abbrev ESS.LpsSlots (M : ℕ) : Type

Vectors of L²(ℝ³) classes indexed by the ordered derivative words of length at most M (prop:lps-smoothing).

Equations

• ESS.LpsSlots M = (↥(CKN.sobolevWords M) → ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume))

noncomputable def ESS.lpsPairCLM (ψ : CKN.Foundation.Parabolic.Vec3 → ℝ) (hψ : MeasureTheory.MemLp ψ 2 MeasureTheory.volume) : ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume) →L[ℝ] ℝ

The L² pairing with a fixed square-integrable function (prop:lps-smoothing).

Equations

• ESS.lpsPairCLM ψ hψ = (innerSL ℝ) (MeasureTheory.MemLp.toLp ψ hψ)

theorem ESS.lpsPairCLM_apply {ψ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hψ : MeasureTheory.MemLp ψ 2 MeasureTheory.volume) (f : ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)) : (lpsPairCLM ψ hψ) f = ∫ (x : CKN.Foundation.Parabolic.Vec3), ↑↑f x * ψ x

The L² pairing with a square-integrable function is the integral of the product (prop:lps-smoothing).

theorem ESS.lps_mem_sobolevWords_of_append {M : ℕ} {α : List (Fin 3)} {j : Fin 3} (h : α ++ [j] ∈ CKN.sobolevWords M) : α ∈ CKN.sobolevWords M

Removing the last letter keeps a word within the order bound (prop:lps-smoothing).

theorem ESS.lps_mem_sobolevWords_succ {M : ℕ} {α : List (Fin 3)} (h : α ∈ CKN.sobolevWords M) : α ∈ CKN.sobolevWords (M + 1)

Words of length at most M have length at most M + 1 (prop:lps-smoothing).

theorem ESS.lps_cons_mem_sobolevWords {M : ℕ} {α : List (Fin 3)} (k : Fin 3) (h : α ∈ CKN.sobolevWords M) : k :: α ∈ CKN.sobolevWords (M + 1)

Adding a first letter raises the order bound by one (prop:lps-smoothing).

noncomputable def ESS.lpsRelCLM (M : ℕ) (α : List (Fin 3)) (j : Fin 3) (h : α ++ [j] ∈ CKN.sobolevWords M) (φ : LpsTestFunction) : LpsSlots M →L[ℝ] ℝ

The weak derivative relation between two slots, tested against one function, as a continuous linear functional (prop:lps-smoothing).

Equations

• ESS.lpsRelCLM M α j h φ = ESS.lpsPairCLM (CKN.spatialDeriv (↑φ) j) ⋯ ∘SL ContinuousLinearMap.proj ⟨α, ⋯⟩ + ESS.lpsPairCLM ↑φ ⋯ ∘SL ContinuousLinearMap.proj ⟨α ++ [j], h⟩

theorem ESS.lpsRelCLM_apply (M : ℕ) (α : List (Fin 3)) (j : Fin 3) (h : α ++ [j] ∈ CKN.sobolevWords M) (φ : LpsTestFunction) (v : LpsSlots M) : (lpsRelCLM M α j h φ) v = (∫ (x : CKN.Foundation.Parabolic.Vec3), ↑↑(v ⟨α, ⋯⟩) x * CKN.spatialDeriv (↑φ) j x) + ∫ (x : CKN.Foundation.Parabolic.Vec3), ↑↑(v ⟨α ++ [j], h⟩) x * ↑φ x

The weak derivative relation functional evaluated on a slot vector (prop:lps-smoothing).

noncomputable def ESS.lpsSobolevSpace (M : ℕ) : Submodule ℝ (LpsSlots M)

The Sobolev space H^M(ℝ³) as a space of slot vectors: the slot α ++ [j] is the weak j-th derivative of the slot α (prop:lps-smoothing).

Equations

• ESS.lpsSobolevSpace M = ⨅ (α : List (Fin 3)), ⨅ (j : Fin 3), ⨅ (h : α ++ [j] ∈ CKN.sobolevWords M), ⨅ (φ : ESS.LpsTestFunction), (↑(ESS.lpsRelCLM M α j h φ)).ker

theorem ESS.mem_lpsSobolevSpace {M : ℕ} {v : LpsSlots M} : v ∈ lpsSobolevSpace M ↔ ∀ (α : List (Fin 3)) (j : Fin 3) (h : α ++ [j] ∈ CKN.sobolevWords M), CKN.HasWeakPartialDerivOn Set.univ j ↑↑(v ⟨α, ⋯⟩) ↑↑(v ⟨α ++ [j], h⟩)

Membership in H^M(ℝ³) is the family of weak derivative relations between consecutive slots (prop:lps-smoothing).

theorem ESS.isClosed_lpsSobolevSpace (M : ℕ) : IsClosed ↑(lpsSobolevSpace M)

H^M(ℝ³) is closed in the space of slot vectors (prop:lps-smoothing).

instance ESS.instCompleteSpaceSubtypeLpsSlotsMemSubmoduleRealLpsSobolevSpace (M : ℕ) : CompleteSpace ↥(lpsSobolevSpace M)

H^M(ℝ³) is complete (prop:lps-smoothing).

noncomputable def ESS.lpsSlotCLM (M : ℕ) (α : List (Fin 3)) : ↥(lpsSobolevSpace M) →L[ℝ] ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)

The slot of an element of H^M(ℝ³) at the word α cut to its first M letters; for words of length at most M this is the slot α itself (prop:lps-smoothing).

Equations

• ESS.lpsSlotCLM M α = ContinuousLinearMap.proj ⟨List.take M α, ⋯⟩ ∘SL (ESS.lpsSobolevSpace M).subtypeL

theorem ESS.lpsSlotCLM_of_mem {M : ℕ} {α : List (Fin 3)} (h : α ∈ CKN.sobolevWords M) (v : ↥(lpsSobolevSpace M)) : (lpsSlotCLM M α) v = ↑v ⟨α, h⟩

The slot of a word within the order bound is the corresponding entry (prop:lps-smoothing).

theorem ESS.lpsSlotCLM_norm_le {M : ℕ} (α : List (Fin 3)) (v : ↥(lpsSobolevSpace M)) : ‖(lpsSlotCLM M α) v‖ ≤ ‖v‖

Each slot is bounded by the norm of the slot vector (prop:lps-smoothing).

theorem ESS.lps_isSobolevFamilyOn_slot {M : ℕ} (v : ↥(lpsSobolevSpace M)) : CKN.IsSobolevFamilyOn M Set.univ ↑↑((lpsSlotCLM M []) v) fun (α : List (Fin 3)) => ↑↑((lpsSlotCLM M α) v)

The slots of an element of H^M(ℝ³) form a Sobolev family through order M (prop:lps-smoothing).

theorem ESS.lps_sobolevSpace_ext {M : ℕ} {v w : ↥(lpsSobolevSpace M)} (h : ∀ (α : List (Fin 3)), α.length ≤ M → (lpsSlotCLM M α) v = (lpsSlotCLM M α) w) : v = w

An element of H^M(ℝ³) is determined by its slots (prop:lps-smoothing).

theorem ESS.lps_sobolevSpace_eq_of_slot_nil {M : ℕ} {v w : ↥(lpsSobolevSpace M)} (h : (lpsSlotCLM M []) v = (lpsSlotCLM M []) w) : v = w

An element of H^M(ℝ³) is determined by its order-zero slot, since weak derivatives are unique (prop:lps-smoothing).

theorem ESS.lps_Lp_eq_of_pairing {f g : ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)} (h : ∀ (φ : CKN.Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → ∫ (x : CKN.Foundation.Parabolic.Vec3), ↑↑f x * φ x = ∫ (x : CKN.Foundation.Parabolic.Vec3), ↑↑g x * φ x) : f = g

Two L² classes with the same pairings against all test functions coincide (prop:lps-smoothing).

noncomputable def ESS.lpsInclCLM (M : ℕ) : ↥(lpsSobolevSpace (M + 1)) →L[ℝ] ↥(lpsSobolevSpace M)

The inclusion H^(M+1)(ℝ³) → H^M(ℝ³) (prop:lps-smoothing).

Equations

• One or more equations did not get rendered due to their size.

theorem ESS.lpsSlotCLM_incl {M : ℕ} (v : ↥(lpsSobolevSpace (M + 1))) {α : List (Fin 3)} (hα : α.length ≤ M) : (lpsSlotCLM M α) ((lpsInclCLM M) v) = (lpsSlotCLM (M + 1) α) v

The inclusion keeps the slots of order at most M (prop:lps-smoothing).

noncomputable def ESS.lpsDerivCLM (M : ℕ) (k : Fin 3) : ↥(lpsSobolevSpace (M + 1)) →L[ℝ] ↥(lpsSobolevSpace M)

The weak partial derivative ∂_k : H^(M+1)(ℝ³) → H^M(ℝ³): the slot α of ∂_k v is the slot k :: α of v (prop:lps-smoothing).

Equations

• One or more equations did not get rendered due to their size.

theorem ESS.lpsSlotCLM_deriv {M : ℕ} (k : Fin 3) (v : ↥(lpsSobolevSpace (M + 1))) {α : List (Fin 3)} (hα : α.length ≤ M) : (lpsSlotCLM M α) ((lpsDerivCLM M k) v) = (lpsSlotCLM (M + 1) (k :: α)) v

The slot α of ∂_k v is the slot k :: α of v (prop:lps-smoothing).

theorem ESS.lps_memLp_of_family {M : ℕ} {D : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ} (hD : CKN.IsSobolevFamilyOn M Set.univ (D []) D) {α : List (Fin 3)} (hα : α.length ≤ M) : MeasureTheory.MemLp (D α) 2 MeasureTheory.volume

The members of a Sobolev family of order at most M are square integrable (prop:lps-smoothing).

theorem ESS.lps_slots_mem_of_family {M : ℕ} {D : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ} (hD : CKN.IsSobolevFamilyOn M Set.univ (D []) D) : (fun (α : ↥(CKN.sobolevWords M)) => MeasureTheory.MemLp.toLp (D ↑α) ⋯) ∈ lpsSobolevSpace M

The L² classes of a Sobolev family through order M form an element of H^M(ℝ³) (prop:lps-smoothing).

noncomputable def ESS.lpsSobolevOf (M : ℕ) (D : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ) (hD : CKN.IsSobolevFamilyOn M Set.univ (D []) D) : ↥(lpsSobolevSpace M)

The element of H^M(ℝ³) whose slots are the L² classes of a Sobolev family through order M (prop:lps-smoothing).

Equations

• ESS.lpsSobolevOf M D hD = ⟨fun (α : ↥(CKN.sobolevWords M)) => MeasureTheory.MemLp.toLp (D ↑α) ⋯, ⋯⟩

theorem ESS.lpsSlotCLM_sobolevOf {M : ℕ} {D : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ} (hD : CKN.IsSobolevFamilyOn M Set.univ (D []) D) {α : List (Fin 3)} (hα : α.length ≤ M) : (lpsSlotCLM M α) (lpsSobolevOf M D hD) = MeasureTheory.MemLp.toLp (D α) ⋯

The slots of the element of H^M(ℝ³) built from a Sobolev family are the L² classes of the family (prop:lps-smoothing).