The projected Navier–Stokes nonlinearity on the Sobolev tower

prop:lps-smoothing: on the spaces of slot vectors, the product H^M × H^M → H^M (M ≥ 2) is a bounded bilinear map and the Leray projection acts slotwise. Consequently the right-hand side N(v)_i = Σ_k ∂_k ∂_k v_i - P(Σ_j v_j ∂_j v)_i of the projected Navier–Stokes equation is a smooth map H^(n+3) → H^(n+1) of divergence-free fields.

theorem ESS.lps_leibniz_ae_linear_left (α : List (Fin 3)) (c : ℝ) {D D₁ D₂ E : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ} (h : ∀ (β : List (Fin 3)), β.length ≤ α.length → D β =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => c * D₁ β x + D₂ β x) : CKN.sobolevLeibnizFamily α D E =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => c * CKN.sobolevLeibnizFamily α D₁ E x + CKN.sobolevLeibnizFamily α D₂ E x

The Leibniz family is almost everywhere linear in its first family (prop:lps-smoothing).

theorem ESS.lps_leibniz_ae_linear_right (α : List (Fin 3)) (c : ℝ) {D E E₁ E₂ : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ} (h : ∀ (β : List (Fin 3)), β.length ≤ α.length → E β =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => c * E₁ β x + E₂ β x) : CKN.sobolevLeibnizFamily α D E =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => c * CKN.sobolevLeibnizFamily α D E₁ x + CKN.sobolevLeibnizFamily α D E₂ x

The Leibniz family is almost everywhere linear in its second family (prop:lps-smoothing).

theorem ESS.lps_toLp_linear {f g h : CKN.Foundation.Parabolic.Vec3 → ℝ} (c : ℝ) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) (hh : MeasureTheory.MemLp h 2 MeasureTheory.volume) (hfgh : f =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => c * g x + h x) : MeasureTheory.MemLp.toLp f hf = c • MeasureTheory.MemLp.toLp g hg + MeasureTheory.MemLp.toLp h hh

Linear relations between square-integrable functions hold for their L² classes (prop:lps-smoothing).

theorem ESS.lpsSlotCLM_ae_linear {M : ℕ} (c : ℝ) (v w : ↥(lpsSobolevSpace M)) (α : List (Fin 3)) : ↑↑((lpsSlotCLM M α) (c • v + w)) =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => c * ↑↑((lpsSlotCLM M α) v) x + ↑↑((lpsSlotCLM M α) w) x

The slots of a linear combination are almost everywhere the linear combination of the slots (prop:lps-smoothing).

theorem ESS.lps_mul_family {M : ℕ} (hM : 2 ≤ M) (v w : ↥(lpsSobolevSpace M)) : CKN.IsSobolevFamilyOn M Set.univ (CKN.sobolevLeibnizFamily [] (fun (β : List (Fin 3)) => ↑↑((lpsSlotCLM M β) v)) fun (β : List (Fin 3)) => ↑↑((lpsSlotCLM M β) w)) fun (α : List (Fin 3)) => CKN.sobolevLeibnizFamily α (fun (β : List (Fin 3)) => ↑↑((lpsSlotCLM M β) v)) fun (β : List (Fin 3)) => ↑↑((lpsSlotCLM M β) w)

The Leibniz family of the slots of two elements of H^M(ℝ³), M ≥ 2, is a Sobolev family of their product (prop:lps-smoothing).

noncomputable def ESS.lpsMulFun (M : ℕ) (hM : 2 ≤ M) (v w : ↥(lpsSobolevSpace M)) : ↥(lpsSobolevSpace M)

The product of two elements of H^M(ℝ³), M ≥ 2: its slots are the Leibniz family of the slots (prop:lps-smoothing).

Equations

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

theorem ESS.lps_mul_family_memLp {M : ℕ} (hM : 2 ≤ M) (v w : ↥(lpsSobolevSpace M)) {α : List (Fin 3)} (hα : α.length ≤ M) : MeasureTheory.MemLp (CKN.sobolevLeibnizFamily α (fun (β : List (Fin 3)) => ↑↑((lpsSlotCLM M β) v)) fun (β : List (Fin 3)) => ↑↑((lpsSlotCLM M β) w)) 2 MeasureTheory.volume

The Leibniz family of the slots of two elements of H^M(ℝ³), M ≥ 2, is a Sobolev family of their product (prop:lps-smoothing).

theorem ESS.lpsSlotCLM_mulFun {M : ℕ} (hM : 2 ≤ M) (v w : ↥(lpsSobolevSpace M)) {α : List (Fin 3)} (hα : α.length ≤ M) : (lpsSlotCLM M α) (lpsMulFun M hM v w) = MeasureTheory.MemLp.toLp (CKN.sobolevLeibnizFamily α (fun (β : List (Fin 3)) => ↑↑((lpsSlotCLM M β) v)) fun (β : List (Fin 3)) => ↑↑((lpsSlotCLM M β) w)) ⋯

The slots of a product are the L² classes of the Leibniz family (prop:lps-smoothing).

theorem ESS.lpsMulFun_linear_left {M : ℕ} (hM : 2 ≤ M) (c : ℝ) (v v' w : ↥(lpsSobolevSpace M)) : lpsMulFun M hM (c • v + v') w = c • lpsMulFun M hM v w + lpsMulFun M hM v' w

The product is linear in its first factor (prop:lps-smoothing).

theorem ESS.lpsMulFun_linear_right {M : ℕ} (hM : 2 ≤ M) (c : ℝ) (v w w' : ↥(lpsSobolevSpace M)) : lpsMulFun M hM v (c • w + w') = c • lpsMulFun M hM v w + lpsMulFun M hM v w'

The product is linear in its second factor (prop:lps-smoothing).

theorem ESS.lpsMulFun_zero_left {M : ℕ} (hM : 2 ≤ M) (w : ↥(lpsSobolevSpace M)) : lpsMulFun M hM 0 w = 0

The product with a zero first factor vanishes (prop:lps-smoothing).

theorem ESS.lpsMulFun_zero_right {M : ℕ} (hM : 2 ≤ M) (v : ↥(lpsSobolevSpace M)) : lpsMulFun M hM v 0 = 0

The product with a zero second factor vanishes (prop:lps-smoothing).

noncomputable def ESS.lpsMulLin (M : ℕ) (hM : 2 ≤ M) : ↥(lpsSobolevSpace M) →ₗ[ℝ] ↥(lpsSobolevSpace M) →ₗ[ℝ] ↥(lpsSobolevSpace M)

The product as a bilinear map (prop:lps-smoothing).

Equations

• ESS.lpsMulLin M hM = LinearMap.mk₂ ℝ (ESS.lpsMulFun M hM) ⋯ ⋯ ⋯ ⋯

theorem ESS.lps_sobolevNormSq_slot_le {M : ℕ} (v : ↥(lpsSobolevSpace M)) : (CKN.sobolevNormSqOn M Set.univ fun (α : List (Fin 3)) => ↑↑((lpsSlotCLM M α) v)) ≤ ↑(CKN.sobolevWords M).card * ‖v‖ ^ 2

The squared Sobolev norm of the slots is bounded by the number of words times the squared norm of the slot vector (prop:lps-smoothing).

theorem ESS.lps_mulFun_bound {M : ℕ} (hM : 2 ≤ M) : ∃ (K : ℝ), ∀ (v w : ↥(lpsSobolevSpace M)), ‖lpsMulFun M hM v w‖ ≤ K * ‖v‖ * ‖w‖

The product H^M(ℝ³) × H^M(ℝ³) → H^M(ℝ³), M ≥ 2, is bounded (prop:lps-smoothing).

noncomputable def ESS.lpsMulCLM (M : ℕ) (hM : 2 ≤ M) : ↥(lpsSobolevSpace M) →L[ℝ] ↥(lpsSobolevSpace M) →L[ℝ] ↥(lpsSobolevSpace M)

The product H^M(ℝ³) × H^M(ℝ³) → H^M(ℝ³), M ≥ 2, as a bounded bilinear map (prop:lps-smoothing).

Equations

• ESS.lpsMulCLM M hM = (ESS.lpsMulLin M hM).mkContinuous₂ ⋯.choose ⋯

theorem ESS.lpsMulCLM_apply {M : ℕ} (hM : 2 ≤ M) (v w : ↥(lpsSobolevSpace M)) : ((lpsMulCLM M hM) v) w = lpsMulFun M hM v w

The bounded bilinear product evaluates to the product of slot vectors (prop:lps-smoothing).

theorem ESS.lps_memLp_mul_nil {M : ℕ} (hM : 2 ≤ M) (v w : ↥(lpsSobolevSpace M)) : MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => ↑↑((lpsSlotCLM M []) v) x * ↑↑((lpsSlotCLM M []) w) x) 2 MeasureTheory.volume

The product of the order-zero slots of two elements of H^M(ℝ³), M ≥ 2, is square integrable (prop:lps-smoothing).

theorem ESS.lpsSlotCLM_mul_nil {M : ℕ} (hM : 2 ≤ M) (v w : ↥(lpsSobolevSpace M)) : (lpsSlotCLM M []) (((lpsMulCLM M hM) v) w) = MeasureTheory.MemLp.toLp (fun (x : CKN.Foundation.Parabolic.Vec3) => ↑↑((lpsSlotCLM M []) v) x * ↑↑((lpsSlotCLM M []) w) x) ⋯

The order-zero slot of a product is the product of the order-zero slots (prop:lps-smoothing).

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

The slot α of the Leray projection of a field of slot vectors (prop:lps-smoothing).

Equations

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

theorem ESS.lpsLeraySlotCLM_apply (M : ℕ) (α : List (Fin 3)) (i : Fin 3) (F : Fin 3 → ↥(lpsSobolevSpace M)) : (lpsLeraySlotCLM M α i) F = (lpsLerayP (WithLp.toLp 2 fun (i' : Fin 3) => (lpsSlotCLM M α) (F i'))).ofLp i

The slot of the Leray projection is the projection of the slots (prop:lps-smoothing).

noncomputable def ESS.lpsLerayCLM (M : ℕ) : (Fin 3 → ↥(lpsSobolevSpace M)) →L[ℝ] Fin 3 → ↥(lpsSobolevSpace M)

The Leray projection acting slotwise on fields of H^M(ℝ³) slot vectors (prop:lps-smoothing).

Equations

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

theorem ESS.lpsSlotCLM_leray {M : ℕ} (F : Fin 3 → ↥(lpsSobolevSpace M)) (i : Fin 3) {α : List (Fin 3)} (hα : α.length ≤ M) : (lpsSlotCLM M α) ((lpsLerayCLM M) F i) = (lpsLerayP (WithLp.toLp 2 fun (i' : Fin 3) => (lpsSlotCLM M α) (F i'))).ofLp i

The slots of the slotwise Leray projection (prop:lps-smoothing).

noncomputable def ESS.lpsNSMap (n : ℕ) (v : Fin 3 → ↥(lpsSobolevSpace (n + 2 + 1))) : Fin 3 → ↥(lpsSobolevSpace (n + 1))

The right-hand side of the projected Navier–Stokes equation, from H^(n+3) fields to H^(n+1) fields: N(v)_i = Σ_k ∂_k ∂_k v_i - P(Σ_j v_j ∂_j v)_i (prop:lps-smoothing).

Equations

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

theorem ESS.lpsNSMap_contDiff (n : ℕ) : ContDiff ℝ (↑⊤) (lpsNSMap n)

The projected Navier–Stokes right-hand side is a smooth map H^(n+3) → H^(n+1) (prop:lps-smoothing).

theorem ESS.lps_memLp_slot_mul (n : ℕ) (v : Fin 3 → ↥(lpsSobolevSpace (n + 2 + 1))) (j i' : Fin 3) : MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => ↑↑((lpsSlotCLM (n + 2 + 1) []) (v j)) x * ↑↑((lpsSlotCLM (n + 2 + 1) [j]) (v i')) x) 2 MeasureTheory.volume

The product of the order-zero slot of one component with the first-order slot of another is square integrable (prop:lps-smoothing).

theorem ESS.lpsSlotCLM_NSMap_nil (n : ℕ) (v : Fin 3 → ↥(lpsSobolevSpace (n + 2 + 1))) (i : Fin 3) : (lpsSlotCLM (n + 1) []) (lpsNSMap n v i) = ∑ k : Fin 3, (lpsSlotCLM (n + 2 + 1) [k, k]) (v i) - (lpsLerayP (WithLp.toLp 2 fun (i' : Fin 3) => ∑ j : Fin 3, MeasureTheory.MemLp.toLp (fun (x : CKN.Foundation.Parabolic.Vec3) => ↑↑((lpsSlotCLM (n + 2 + 1) []) (v j)) x * ↑↑((lpsSlotCLM (n + 2 + 1) [j]) (v i')) x) ⋯)).ofLp i

The order-zero slot of the projected Navier–Stokes right-hand side (prop:lps-smoothing).