Even Bessel norms of Schwartz tensors through physical derivatives

For a complex tensor-valued Schwartz field, the Bessel potential of even order 2k is the k-fold iterate of the second-order operator 1 - (2π)⁻² Δ. Consequently the complete H²ᵏ norm of the canonical Sobolev lift is the L² norm of that iterate, and every derivative of the iterate is controlled pointwise by the derivatives of the field up to 2k further orders.

theorem CKN.Leray.regularisedSchwartz_iteratedFDeriv_lineDerivOp_norm_le {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (ψ : SchwartzMap Foundation.Parabolic.L2Vec3 F) (v : Foundation.Parabolic.L2Vec3) (n : ℕ) (x : Foundation.Parabolic.L2Vec3) : ‖iteratedFDeriv ℝ n (⇑(LineDeriv.lineDerivOp v ψ)) x‖ ≤ ‖v‖ * ‖iteratedFDeriv ℝ (n + 1) (⇑ψ) x‖

Each Fréchet derivative of a directional derivative of a Schwartz field is bounded by the next derivative of the field times the length of the direction.

theorem CKN.Leray.regularisedSchwartz_iteratedFDeriv_laplacian_norm_le {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (ψ : SchwartzMap Foundation.Parabolic.L2Vec3 F) (n : ℕ) (x : Foundation.Parabolic.L2Vec3) : ‖iteratedFDeriv ℝ n (⇑(Laplacian.laplacian ψ)) x‖ ≤ ↑(Module.finrank ℝ Foundation.Parabolic.L2Vec3) * ‖iteratedFDeriv ℝ (n + 2) (⇑ψ) x‖

Each Fréchet derivative of the Laplacian of a Schwartz field is bounded by three times the derivative two orders higher.

noncomputable def CKN.Leray.regularisedSchwartzBesselStep {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (c : ℝ) (ψ : SchwartzMap Foundation.Parabolic.L2Vec3 F) : SchwartzMap Foundation.Parabolic.L2Vec3 F

The second-order Bessel step ψ ↦ ψ - c Δψ on Schwartz fields.

Equations

• CKN.Leray.regularisedSchwartzBesselStep c ψ = ψ - c • Laplacian.laplacian ψ

theorem CKN.Leray.regularisedSchwartzBesselStep_iteratedFDeriv_norm_le {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (c : ℝ) (ψ : SchwartzMap Foundation.Parabolic.L2Vec3 F) (n : ℕ) (x : Foundation.Parabolic.L2Vec3) : ‖iteratedFDeriv ℝ n (⇑(regularisedSchwartzBesselStep c ψ)) x‖ ≤ ‖iteratedFDeriv ℝ n (⇑ψ) x‖ + |c| * ↑(Module.finrank ℝ Foundation.Parabolic.L2Vec3) * ‖iteratedFDeriv ℝ (n + 2) (⇑ψ) x‖

One Bessel step costs two derivatives in every pointwise derivative bound.

theorem CKN.Leray.regularisedSchwartzBesselStep_iterate_iteratedFDeriv_norm_le {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (c : ℝ) (k : ℕ) : ∃ (A : ℝ), 0 ≤ A ∧ ∀ (ψ : SchwartzMap Foundation.Parabolic.L2Vec3 F) (n : ℕ) (x : Foundation.Parabolic.L2Vec3), ‖iteratedFDeriv ℝ n (⇑((regularisedSchwartzBesselStep c)^[k] ψ)) x‖ ≤ A * ∑ m ∈ Finset.range (2 * k + 1), ‖iteratedFDeriv ℝ (n + m) (⇑ψ) x‖

The k-fold Bessel step is controlled pointwise, at every derivative order, by the next 2k derivatives of the field.

theorem CKN.Leray.regularisedTensor_besselPotential_two_eq (D : TemperedDistribution Foundation.Parabolic.L2Vec3 ComplexTensor3) : (TemperedDistribution.besselPotential Foundation.Parabolic.L2Vec3 ComplexTensor3 2) D = D - ((2 * Real.pi) ^ 2)⁻¹ • Laplacian.laplacian D

The order-two Bessel potential on complex tensor distributions is the identity minus (2π)⁻² times the Laplacian.

theorem CKN.Leray.regularisedTensor_besselPotential_even_schwartz (k : ℕ) (T : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexTensor3) : (TemperedDistribution.besselPotential Foundation.Parabolic.L2Vec3 ComplexTensor3 ↑(2 * k)) ((SchwartzMap.toTemperedDistributionCLM Foundation.Parabolic.L2Vec3 ComplexTensor3 MeasureTheory.volume) T) = (SchwartzMap.toTemperedDistributionCLM Foundation.Parabolic.L2Vec3 ComplexTensor3 MeasureTheory.volume) ((regularisedSchwartzBesselStep ((2 * Real.pi) ^ 2)⁻¹)^[k] T)

On a Schwartz tensor, the even Bessel potential of order 2k is the k-fold second-order Bessel step with constant (2π)⁻².

theorem CKN.Leray.regularisedTensor_schwartz_bessel_even_norm_eq (k : ℕ) (T : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexTensor3) : ‖⋯.toBesselPotentialSpace‖ = ‖((regularisedSchwartzBesselStep ((2 * Real.pi) ^ 2)⁻¹)^[k] T).toLp 2 MeasureTheory.volume‖

The complete H²ᵏ norm of the canonical Sobolev lift of a Schwartz tensor is the L² norm of its k-fold second-order Bessel step.