Continuous spatial L² curves from damped Fourier multipliers

A bounded frequency multiplier acts continuously on the weighted Bessel frequency trajectory. Inverse Fourier transformation gives the continuous spatial L² derivative curve.

noncomputable def ESS.lpsDampedWeightSymbol (n : ℕ) (α : List (Fin 3)) (ξ : CKN.Foundation.Parabolic.L2Vec3) : ℂ

The bounded frequency symbol for an ordered derivative of a high-Bessel field.

Equations

• ESS.lpsDampedWeightSymbol n α ξ = ESS.lpsDampedFourierWordSymbol n α ξ * ↑((1 + ‖ξ‖ ^ 2) ^ (-2))

theorem ESS.lps_dampedWeightSymbol_continuous (n : ℕ) (α : List (Fin 3)) : Continuous (lpsDampedWeightSymbol n α)

The ordered derivative symbol is continuous in frequency.

noncomputable def ESS.lpsDampedWeightLp (n : ℕ) (α : List (Fin 3)) (hα : α.length ≤ 2 * (n + 1)) : ↥(MeasureTheory.Lp ℂ ⊤ MeasureTheory.volume)

The ordered derivative symbol is an essentially bounded scalar multiplier (prop:lps-smoothing).

Equations

• ESS.lpsDampedWeightLp n α hα = MeasureTheory.MemLp.toLp (ESS.lpsDampedWeightSymbol n α) ⋯

theorem ESS.lps_dampedFourierCurve_continuous {I : Type u_1} [TopologicalSpace I] (n : ℕ) (α : List (Fin 3)) (hα : α.length ≤ 2 * (n + 1)) (G : I → ↥CKN.Leray.ComplexVectorL2) (hG : Continuous G) : Continuous fun (t : I) => (MeasureTheory.Lp.fourierTransformₗᵢ CKN.Foundation.Parabolic.L2Vec3 CKN.Leray.ComplexVec3).symm (lpsDampedWeightLp n α hα • G t)

Applying the ordered bounded multiplier and inverse Fourier transform to a continuous high-Bessel frequency path gives a continuous complex spatial L² curve (prop:lps-smoothing).

theorem ESS.lps_dampedWeightLp_ae_eq (n : ℕ) (α : List (Fin 3)) (hα : α.length ≤ 2 * (n + 1)) : ↑↑(lpsDampedWeightLp n α hα) =ᵐ[MeasureTheory.volume] lpsDampedWeightSymbol n α

The bounded scalar multiplier agrees almost everywhere with its frequency formula.

theorem ESS.lps_dampedSpaceTimeField_ae_eq_curve (n : ℕ) (α : List (Fin 3)) (hα : α.length ≤ 2 * (n + 1)) (G : ↥CKN.Leray.ComplexVectorL2) : CKN.Leray.regR12WeightedField (lpsDampedFourierWordSymbol n α) G =ᵐ[MeasureTheory.volume] ↑↑((MeasureTheory.Lp.fourierTransformₗᵢ CKN.Foundation.Parabolic.L2Vec3 CKN.Leray.ComplexVec3).symm (lpsDampedWeightLp n α hα • G))

The classical inverse Fourier field agrees almost everywhere with the continuous spatial L² curve obtained from its bounded multiplier (prop:lps-smoothing).

noncomputable def ESS.lpsDampedScalarCurve (n : ℕ) (α : List (Fin 3)) (hα : α.length ≤ 2 * (n + 1)) (i : Fin 3) (G : ℝ → ↥CKN.Leray.ComplexVectorL2) (t : ℝ) : ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)

The real coordinate of an ordered Fourier derivative is a continuous spatial L² trajectory after transport from L2Vec3 to Vec3.

Equations

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

theorem ESS.lps_dampedScalarCurve_continuous (n : ℕ) (α : List (Fin 3)) (hα : α.length ≤ 2 * (n + 1)) (i : Fin 3) (G : ℝ → ↥CKN.Leray.ComplexVectorL2) (hG : Continuous G) : Continuous (lpsDampedScalarCurve n α hα i G)

The physical real coordinate inherits the continuous L² curve of the weighted Fourier trajectory (prop:lps-smoothing).

theorem ESS.lps_dampedScalarCurve_ae_eq (n : ℕ) (α : List (Fin 3)) (hα : α.length ≤ 2 * (n + 1)) (i : Fin 3) (G : ℝ → ↥CKN.Leray.ComplexVectorL2) (t : ℝ) : ↑↑(lpsDampedScalarCurve n α hα i G t) =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Leray.regR12SpaceTimeField (CKN.Leray.regR12CoordCLM i) (lpsDampedFourierWordSymbol n α) G (x, t)

On each slice the Fourier scalar curve represents the classical ordered inverse Fourier field almost everywhere.