Higher Bessel lifts of the regularized velocity

Every even-order Bessel lift gives a continuous frequency trajectory. Its inverse Bessel weight represents the Fourier transform of the same physical regularized velocity.

noncomputable def ESS.lpsRegR12HighLiftFreq (n : ℕ) (T : ℝ) (hT : 0 ≤ T) (v : C(↑(CKN.Leray.RegularizedMildTimeInterval T), BesselPotentialSpace CKN.Foundation.Parabolic.L2Vec3 CKN.Leray.ComplexVec3 (↑(2 * (n + 2))) 2)) (t : ℝ) : ↥CKN.Leray.ComplexVectorL2

Frequency trajectory of a Bessel lift of order 2(n+2), extended from a finite interval by clamping time.

Equations

• ESS.lpsRegR12HighLiftFreq n T hT v t = (MeasureTheory.Lp.fourierTransformₗᵢ CKN.Foundation.Parabolic.L2Vec3 CKN.Leray.ComplexVec3) (v (CKN.Leray.regularizedMildTimeClamp T hT t)).toLp

theorem ESS.lps_regR12HighLiftFreq_continuous (n : ℕ) (T : ℝ) (hT : 0 ≤ T) (v : C(↑(CKN.Leray.RegularizedMildTimeInterval T), BesselPotentialSpace CKN.Foundation.Parabolic.L2Vec3 CKN.Leray.ComplexVec3 (↑(2 * (n + 2))) 2)) : Continuous (lpsRegR12HighLiftFreq n T hT v)

A higher Bessel lift has a continuous weighted Fourier trajectory (prop:lps-smoothing).

theorem ESS.lps_regR12HighLiftFreq_norm_le (n : ℕ) (T : ℝ) (hT : 0 ≤ T) (v : C(↑(CKN.Leray.RegularizedMildTimeInterval T), BesselPotentialSpace CKN.Foundation.Parabolic.L2Vec3 CKN.Leray.ComplexVec3 (↑(2 * (n + 2))) 2)) (t : ℝ) : ‖lpsRegR12HighLiftFreq n T hT v t‖ ≤ ‖v‖

The weighted frequency trajectory has norm bounded by its Bessel lift on every time slice.

theorem ESS.lps_regR12HighLiftFreq_curve_ae_eq (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (ha : CKN.IsInJ a) (n : ℕ) (T : ℝ) (hT : 0 ≤ T) (v : C(↑(CKN.Leray.RegularizedMildTimeInterval T), BesselPotentialSpace CKN.Foundation.Parabolic.L2Vec3 CKN.Leray.ComplexVec3 (↑(2 * (n + 2))) 2)) (hv : ∀ (t : ↑(CKN.Leray.RegularizedMildTimeInterval T)), (CKN.Leray.regularisedBesselSobolevToL2CLM ↑(2 * (n + 2)) ⋯) (v t) = CKN.Leray.complexifyVectorL2 (CKN.Leray.regR12Curve ρ ε hε a ha ↑t)) (t : ℝ) (ht : t ∈ Set.Icc 0 T) : ↑↑(CKN.Leray.regR12FreqCurve ρ ε hε a ha t) =ᵐ[MeasureTheory.volume] fun (ξ : CKN.Foundation.Parabolic.L2Vec3) => ↑((1 + ‖ξ‖ ^ 2) ^ (-↑(2 * (n + 2)) / 2)) • ↑↑(lpsRegR12HighLiftFreq n T hT v t) ξ

The physical regularized curve has the inverse Bessel-weight Fourier representation of every higher lift on its time interval (prop:lps-smoothing).

theorem ESS.lps_damped_base_weight_eq (n : ℕ) (ξ : CKN.Foundation.Parabolic.L2Vec3) : ↑((1 + ‖ξ‖ ^ 2) ^ (-↑n)) * ↑((1 + ‖ξ‖ ^ 2) ^ (-2)) = ↑((1 + ‖ξ‖ ^ 2) ^ (-↑(2 * (n + 2)) / 2))

The inverse order-four weight and the extra Bessel damping combine to the inverse weight of order 2(n+2) (prop:lps-smoothing).

theorem ESS.lps_regR12Velocity_eq_high_model (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (ha : CKN.IsInJ a) (n : ℕ) (T : ℝ) (hT : 0 ≤ T) (v : C(↑(CKN.Leray.RegularizedMildTimeInterval T), BesselPotentialSpace CKN.Foundation.Parabolic.L2Vec3 CKN.Leray.ComplexVec3 (↑(2 * (n + 2))) 2)) (hv : ∀ (t : ↑(CKN.Leray.RegularizedMildTimeInterval T)), (CKN.Leray.regularisedBesselSobolevToL2CLM ↑(2 * (n + 2)) ⋯) (v t) = CKN.Leray.complexifyVectorL2 (CKN.Leray.regR12Curve ρ ε hε a ha ↑t)) (z : CKN.Foundation.Parabolic.ParabolicPoint) (hz : z.2 ∈ Set.Icc 0 T) (i : Fin 3) : CKN.Leray.regR12Velocity ρ ε hε a ha z i = CKN.Leray.regR12SpaceTimeField (CKN.Leray.regR12CoordCLM i) (lpsDampedFourierWordSymbol n []) (lpsRegR12HighLiftFreq n T hT v) z

On a finite interval, the physical regularized velocity is the high-Bessel inverse Fourier field with the excess weight moved into the multiplier (prop:lps-smoothing).

theorem ESS.lps_regR12Velocity_wordDeriv_eq_high_model (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (ha : CKN.IsInJ a) (n : ℕ) (T : ℝ) (hT : 0 ≤ T) (v : C(↑(CKN.Leray.RegularizedMildTimeInterval T), BesselPotentialSpace CKN.Foundation.Parabolic.L2Vec3 CKN.Leray.ComplexVec3 (↑(2 * (n + 2))) 2)) (hv : ∀ (t : ↑(CKN.Leray.RegularizedMildTimeInterval T)), (CKN.Leray.regularisedBesselSobolevToL2CLM ↑(2 * (n + 2)) ⋯) (v t) = CKN.Leray.complexifyVectorL2 (CKN.Leray.regR12Curve ρ ε hε a ha ↑t)) (t : ℝ) (ht : t ∈ Set.Icc 0 T) (i : Fin 3) (α : List (Fin 3)) (hα : α.length ≤ 2 * (n + 1)) : (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Leray.regR12Velocity ρ ε hε a ha (x, t) i) = fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Leray.regR12SpaceTimeField (CKN.Leray.regR12CoordCLM i) (lpsDampedFourierWordSymbol n α) (lpsRegR12HighLiftFreq n T hT v) (x, t)

Every classical ordered derivative of the physical regularized velocity on a finite interval is the corresponding high-Bessel inverse Fourier field (prop:lps-smoothing).

theorem ESS.lps_regR12Velocity_wordDeriv_memLp_slab (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (ha : CKN.IsInJ a) (n : ℕ) (δ T : ℝ) (hδ : 0 ≤ δ) (hδT : δ < T) (v : C(↑(CKN.Leray.RegularizedMildTimeInterval T), BesselPotentialSpace CKN.Foundation.Parabolic.L2Vec3 CKN.Leray.ComplexVec3 (↑(2 * (n + 2))) 2)) (hv : ∀ (t : ↑(CKN.Leray.RegularizedMildTimeInterval T)), (CKN.Leray.regularisedBesselSobolevToL2CLM ↑(2 * (n + 2)) ⋯) (v t) = CKN.Leray.complexifyVectorL2 (CKN.Leray.regR12Curve ρ ε hε a ha ↑t)) (i : Fin 3) (α : List (Fin 3)) (hα : α.length ≤ 2 * (n + 1)) : MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.wordDeriv α (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Leray.regR12Velocity ρ ε hε a ha (x, z.2) i) z.1) 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo δ T)))

Ordered physical spatial derivatives of the regularized velocity belong to space-time L² on every positive-time slab through the available higher Bessel order (prop:lps-smoothing).

theorem ESS.lps_regR12Velocity_wordDeriv_memLp_slice_of_lift (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (ha : CKN.IsInJ a) (n : ℕ) (T : ℝ) (hT : 0 ≤ T) (v : C(↑(CKN.Leray.RegularizedMildTimeInterval T), BesselPotentialSpace CKN.Foundation.Parabolic.L2Vec3 CKN.Leray.ComplexVec3 (↑(2 * (n + 2))) 2)) (hv : ∀ (t : ↑(CKN.Leray.RegularizedMildTimeInterval T)), (CKN.Leray.regularisedBesselSobolevToL2CLM ↑(2 * (n + 2)) ⋯) (v t) = CKN.Leray.complexifyVectorL2 (CKN.Leray.regR12Curve ρ ε hε a ha ↑t)) (t : ℝ) (ht : t ∈ Set.Icc 0 T) (i : Fin 3) (α : List (Fin 3)) (hα : α.length ≤ 2 * (n + 1)) : MeasureTheory.MemLp (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Leray.regR12Velocity ρ ε hε a ha (x, t) i) 2 MeasureTheory.volume

A higher Bessel lift makes every ordered physical derivative square-integrable on each closed-interval slice (prop:lps-smoothing).

theorem ESS.lps_regR12Velocity_all_word_memLp_slice (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (ha : CKN.IsInJ a) (t : ℝ) (ht : 0 ≤ t) (i : Fin 3) (α : List (Fin 3)) : MeasureTheory.MemLp (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Leray.regR12Velocity ρ ε hε a ha (x, t) i) 2 MeasureTheory.volume

Every nonnegative-time slice of the actual regularized velocity has square-integrable classical derivatives at every ordered spatial word (prop:lps-smoothing).

theorem ESS.lps_regR12Velocity_all_word_continuousOn (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (ha : CKN.IsInJ a) (i : Fin 3) (α : List (Fin 3)) : ContinuousOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.wordDeriv α (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Leray.regR12Velocity ρ ε hε a ha (x, z.2) i) z.1) (CKN.spaceTimeSet Set.univ (Set.Ioi 0))

Every ordered spatial derivative of the physical regularized velocity is jointly continuous at positive times (prop:lps-smoothing).