Physical derivatives of Schwartz fields through the even Bessel order

Every Fréchet derivative of order at most 2k of a complex Schwartz velocity has L² norm bounded by a fixed multiple of the complete H²ᵏ norm of its canonical Sobolev lift.

theorem CKN.Leray.regularisedDistribution_foldl_ofFn_rev_eq_iteratedLineDerivOp {n : ℕ} (m : Fin n → Foundation.Parabolic.L2Vec3) (D : TemperedDistribution Foundation.Parabolic.L2Vec3 ComplexVec3) : List.foldl (fun (F : TemperedDistribution Foundation.Parabolic.L2Vec3 ComplexVec3) (v : Foundation.Parabolic.L2Vec3) => LineDeriv.lineDerivOp v F) D (List.ofFn fun (a : Fin n) => m a.rev) = LineDeriv.iteratedLineDerivOp m D

The ordered distributional derivative along the reversed list of a tuple of directions is the iterated directional derivative along the tuple.

theorem CKN.Leray.regularisedSchwartz_iteratedLineDerivOp_toTemperedDistribution {n : ℕ} (m : Fin n → Foundation.Parabolic.L2Vec3) (f : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3) : LineDeriv.iteratedLineDerivOp m ((SchwartzMap.toTemperedDistributionCLM Foundation.Parabolic.L2Vec3 ComplexVec3 MeasureTheory.volume) f) = (SchwartzMap.toTemperedDistributionCLM Foundation.Parabolic.L2Vec3 ComplexVec3 MeasureTheory.volume) (LineDeriv.iteratedLineDerivOp m f)

Iterated directional derivatives commute with the embedding of Schwartz fields into tempered distributions.

theorem CKN.Leray.regularisedSchwartz_iteratedLineDerivOp_toLp_norm_le_bessel (k : ℕ) {p : ℕ} (hp : p ≤ 2 * k) (m : Fin p → Foundation.Parabolic.L2Vec3) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (f : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3), ‖(LineDeriv.iteratedLineDerivOp m f).toLp 2 MeasureTheory.volume‖ ≤ C * ‖regularisedBesselOfSchwartz (↑(2 * k)) f‖

Each iterated directional derivative of order at most 2k of a complex Schwartz velocity is bounded in L² by the complete H²ᵏ norm of its canonical Sobolev lift.

theorem CKN.Leray.regularisedSchwartz_iteratedFDeriv_eLpNorm_le_bessel (k : ℕ) {p : ℕ} (hp : p ≤ 2 * k) : ∃ (B : ℝ), 0 ≤ B ∧ ∀ (f : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3), MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.L2Vec3) => ‖iteratedFDeriv ℝ p (⇑f) x‖) 2 MeasureTheory.volume ≤ ENNReal.ofReal (B * ‖regularisedBesselOfSchwartz (↑(2 * k)) f‖)

The L² norm of the p-th Fréchet derivative of a complex Schwartz velocity is bounded by the complete H²ᵏ norm when p ≤ 2k.

theorem CKN.Leray.regularisedSchwartz_iteratedFDeriv_sum_eLpNorm_le_bessel (k : ℕ) : ∃ (B : ℝ), 0 ≤ B ∧ ∀ (f : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3), MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.L2Vec3) => ∑ p ∈ Finset.range (2 * k + 1), ‖iteratedFDeriv ℝ p (⇑f) x‖) 2 MeasureTheory.volume ≤ ENNReal.ofReal (B * ‖regularisedBesselOfSchwartz (↑(2 * k)) f‖)

The sum of the pointwise norms of all Fréchet derivatives through order 2k of a complex Schwartz velocity is bounded in L² by the complete H²ᵏ norm of its canonical Sobolev lift.