Classical spatial derivatives of high-order inverse Fourier fields

The extra Bessel weight places every finite coordinate word within the quadratic-growth inverse Fourier field theorem. Differentiation then appends the corresponding coordinate symbol.

theorem ESS.lps_fourierWordSymbol_continuous (α : List (Fin 3)) : Continuous (lpsFourierWordSymbol α)

The ordered coordinate multiplier is continuous in frequency.

theorem ESS.lps_dampedFourierWordSymbol_continuous (n : ℕ) (α : List (Fin 3)) : Continuous (lpsDampedFourierWordSymbol n α)

The damped ordered multiplier is continuous in frequency.

theorem ESS.lps_dampedSpaceTimeField_spatialPartial {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (n : ℕ) (α : List (Fin 3)) (hα : α.length + 1 ≤ 2 * (n + 1)) (c : E →L[ℝ] ℝ) (G : ℝ → ↥(MeasureTheory.Lp E 2 MeasureTheory.volume)) (z : CKN.Foundation.Parabolic.ParabolicPoint) : DifferentiableAt ℝ (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Leray.regR12SpaceTimeField c (lpsDampedFourierWordSymbol n α) G (x, z.2)) z.1 ∧ ∀ (j : Fin 3), CKN.spatialPartial (CKN.Leray.regR12SpaceTimeField c (lpsDampedFourierWordSymbol n α) G) j z = CKN.Leray.regR12SpaceTimeField c (lpsDampedFourierWordSymbol n (α ++ [j])) G z

A high-order inverse Fourier field has the next classical spatial partial, represented by the appended coordinate word (prop:lps-smoothing).

theorem ESS.lps_dampedSpaceTimeField_wordDeriv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (n : ℕ) (α : List (Fin 3)) (hα : α.length ≤ 2 * (n + 1)) (c : E →L[ℝ] ℝ) (G : ℝ → ↥(MeasureTheory.Lp E 2 MeasureTheory.volume)) (t : ℝ) : (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Leray.regR12SpaceTimeField c (lpsDampedFourierWordSymbol n []) G (x, t)) = fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Leray.regR12SpaceTimeField c (lpsDampedFourierWordSymbol n α) G (x, t)

Every ordered classical spatial derivative of the base inverse Fourier field is represented by its damped coordinate multiplier, through the chosen Bessel order (prop:lps-smoothing).

theorem ESS.lps_dampedSpaceTimeField_continuous {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (n : ℕ) (α : List (Fin 3)) (hα : α.length ≤ 2 * (n + 1)) (c : E →L[ℝ] ℝ) (G : ℝ → ↥(MeasureTheory.Lp E 2 MeasureTheory.volume)) (hG : Continuous G) : Continuous fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.Leray.regR12SpaceTimeField c (lpsDampedFourierWordSymbol n α) G (z.1, z.2)

Continuous higher Bessel frequency curves give jointly continuous ordered spatial derivative fields on the product space (prop:lps-smoothing).

theorem ESS.lps_dampedSpaceTimeField_frequency_memLp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (n : ℕ) (α : List (Fin 3)) (hα : α.length ≤ 2 * (n + 1)) (G : ↥(MeasureTheory.Lp E 2 MeasureTheory.volume)) : MeasureTheory.MemLp (fun (ξ : CKN.Foundation.Parabolic.L2Vec3) => lpsDampedFourierWordSymbol n α ξ • ↑((1 + ‖ξ‖ ^ 2) ^ (-2)) • ↑↑G ξ) 2 MeasureTheory.volume

The weighted frequency representative of each ordered spatial word remains in L² (prop:lps-smoothing).

theorem ESS.lps_dampedSpaceTimeField_slice_memLp {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (n : ℕ) (α : List (Fin 3)) (hα : α.length ≤ 2 * (n + 1)) (c : E →L[ℝ] ℝ) (G : ↥(MeasureTheory.Lp E 2 MeasureTheory.volume)) : MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => c (CKN.Leray.regR12WeightedField (lpsDampedFourierWordSymbol n α) G (WithLp.toLp 2 x))) 2 MeasureTheory.volume

Every spatial slice of a damped high-order inverse Fourier field is square-integrable (prop:lps-smoothing).