The pointwise regularized velocity

The velocity of thm:regularised at a point (x,t) is the inverse Fourier integral, at x, of the Fourier transform of the global regularized mild curve at time t. On a time interval [0,T] on which the curve lifts continuously to the Bessel potential space of order four, this is the space-time field of the Fourier transform of the lift, weighted by the inverse Bessel weight of order four.

theorem CKN.Leray.regR12_initial_memLp (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) : MeasureTheory.MemLp (regUniformMollifiedInitial ρ ε hε a) 2 MeasureTheory.volume

theorem CKN.Leray.regR12_initial_mildJData (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) : RegularizedMildJData (realVectorL2OfCoordinateFunction (regUniformMollifiedInitial ρ ε hε a) ⋯)

noncomputable def CKN.Leray.regR12Curve (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (t : ℝ) : ↥RealVectorL2

The global regularized mild curve issued from the mollified datum.

Equations

• CKN.Leray.regR12Curve ρ ε hε a ha t = CKN.Leray.regularizedGlobalMildCurve ρ ε hε (CKN.Leray.realVectorL2OfCoordinateFunction (CKN.Leray.regUniformMollifiedInitial ρ ε hε a) ⋯) ⋯ t

noncomputable def CKN.Leray.regR12FreqCurve (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (t : ℝ) : ↥ComplexVectorL2

The Fourier transform of the complexified global curve.

Equations

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

noncomputable def CKN.Leray.regR12CoordCLM (i : Fin 3) : ComplexVec3 →L[ℝ] ℝ

The real part of the i-th coordinate of a complex vector.

Equations

• CKN.Leray.regR12CoordCLM i = Complex.reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ (PiLp.proj 2 (fun (x : Fin 3) => ℂ) i)

noncomputable def CKN.Leray.regR12Velocity (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3

The pointwise regularized velocity: the inverse Fourier integral of the Fourier transform of the global curve.

Equations

• CKN.Leray.regR12Velocity ρ ε hε a ha z i = (CKN.Leray.regR12CoordCLM i) (FourierTransformInv.fourierInv (↑↑(CKN.Leray.regR12FreqCurve ρ ε hε a ha z.2)) (WithLp.toLp 2 z.1))

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

The Fourier transform of the Bessel lift, extended to all times by clamping to [0,T].

Equations

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

theorem CKN.Leray.regR12LiftFreq_continuous (T : ℝ) (hT : 0 ≤ T) (v : C(↑(RegularizedMildTimeInterval T), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * 2)) 2)) : Continuous (regR12LiftFreq T hT v)

theorem CKN.Leray.regR12LiftFreq_norm_le (T : ℝ) (hT : 0 ≤ T) (v : C(↑(RegularizedMildTimeInterval T), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * 2)) 2)) (t : ℝ) : ‖regR12LiftFreq T hT v t‖ ≤ ‖v‖

theorem CKN.Leray.regR12_besselOrder_nonneg : 0 ≤ ↑(2 * 2)

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

On [0,T], the Fourier transform of the curve is the inverse Bessel weight of order four times the Fourier transform of the lift.

theorem CKN.Leray.regR12Velocity_eq_model (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (T : ℝ) (hT : 0 ≤ T) (v : C(↑(RegularizedMildTimeInterval T), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * 2)) 2)) (hv : ∀ (t : ↑(RegularizedMildTimeInterval T)), (regularisedBesselSobolevToL2CLM (↑(2 * 2)) regR12_besselOrder_nonneg) (v t) = complexifyVectorL2 (regR12Curve ρ ε hε a ha ↑t)) (z : Foundation.Parabolic.ParabolicPoint) (hz : z.2 ∈ Set.Icc 0 T) (i : Fin 3) : regR12Velocity ρ ε hε a ha z i = regR12SpaceTimeField (regR12CoordCLM i) (fun (x : Foundation.Parabolic.L2Vec3) => 1) (regR12LiftFreq T hT v) z

On [0,T], the velocity is the space-time field of the lift.

theorem CKN.Leray.regR12Velocity_slice_ae_eq (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (T : ℝ) (hT : 0 ≤ T) (v : C(↑(RegularizedMildTimeInterval T), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * 2)) 2)) (hv : ∀ (t : ↑(RegularizedMildTimeInterval T)), (regularisedBesselSobolevToL2CLM (↑(2 * 2)) regR12_besselOrder_nonneg) (v t) = complexifyVectorL2 (regR12Curve ρ ε hε a ha ↑t)) (t : ℝ) (ht : t ∈ Set.Icc 0 T) : (fun (x : Foundation.Parabolic.Vec3) => regR12Velocity ρ ε hε a ha (x, t)) =ᵐ[MeasureTheory.volume] realVectorL2Representative (regR12Curve ρ ε hε a ha t)

On [0,T], the velocity slice represents the global curve.