Space-time fields from continuous paths of frequency fields

A continuous path t ↦ G t of square-integrable frequency fields, weighted by the inverse Bessel weight of order four and a multiplier of at most quadratic growth, defines a continuous space-time field through the inverse Fourier integral. Its spatial partial derivatives multiply the frequency field by 2πi ξ_j, and it is bounded on every time set where the path is bounded. These fields realize the velocity and pressure of thm:regularised (R2).

noncomputable def CKN.Leray.regR12SpaceTimeField {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (c : E →L[ℝ] ℝ) (M : Foundation.Parabolic.L2Vec3 → ℂ) (G : ℝ → ↥(MeasureTheory.Lp E 2 MeasureTheory.volume)) : Foundation.Parabolic.ParabolicPoint → ℝ

The real space-time field c (W_M (G t) x).

Equations

• CKN.Leray.regR12SpaceTimeField c M G z = c (CKN.Leray.regR12WeightedField M (G z.2) (WithLp.toLp 2 z.1))

noncomputable def CKN.Leray.regR12CoordSymbol (j : Fin 3) : Foundation.Parabolic.L2Vec3 → ℂ

The frequency multiplier of the coordinate partial derivative ∂_j.

Equations

• CKN.Leray.regR12CoordSymbol j = CKN.Leray.regR12DirSymbol (WithLp.toLp 2 (CKN.basisVec j))

theorem CKN.Leray.regR12CoordSymbol_continuous (j : Fin 3) : Continuous (regR12CoordSymbol j)

theorem CKN.Leray.regR12CoordSymbol_norm_le (j : Fin 3) (ξ : Foundation.Parabolic.L2Vec3) : ‖regR12CoordSymbol j ξ‖ ≤ 2 * Real.pi * ‖ξ‖

theorem CKN.Leray.regR12SpaceTimeField_continuous {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (c : E →L[ℝ] ℝ) (M : Foundation.Parabolic.L2Vec3 → ℂ) (hM : MeasureTheory.AEStronglyMeasurable M MeasureTheory.volume) (C : ℝ) (hC : 0 ≤ C) (hMC : ∀ (ξ : Foundation.Parabolic.L2Vec3), ‖M ξ‖ ≤ C * (1 + ‖ξ‖ ^ 2)) (G : ℝ → ↥(MeasureTheory.Lp E 2 MeasureTheory.volume)) (hG : Continuous G) : Continuous fun (z : Foundation.Parabolic.Vec3 × ℝ) => c (regR12WeightedField M (G z.2) (WithLp.toLp 2 z.1))

The space-time field is continuous for the product topology.

theorem CKN.Leray.regR12SpaceTimeField_abs_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (c : E →L[ℝ] ℝ) (M : Foundation.Parabolic.L2Vec3 → ℂ) (hM : MeasureTheory.AEStronglyMeasurable M MeasureTheory.volume) (C : ℝ) (hC : 0 ≤ C) (hMC : ∀ (ξ : Foundation.Parabolic.L2Vec3), ‖M ξ‖ ≤ C * (1 + ‖ξ‖ ^ 2)) (G : ℝ → ↥(MeasureTheory.Lp E 2 MeasureTheory.volume)) (z : Foundation.Parabolic.ParabolicPoint) : |regR12SpaceTimeField c M G z| ≤ ‖c‖ * (C * (MeasureTheory.eLpNorm regR12Kernel 2 MeasureTheory.volume).toReal * ‖G z.2‖)

The space-time field is bounded by the norm of the frequency path.

theorem CKN.Leray.regR12SpaceTimeField_spatialPartial {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (c : E →L[ℝ] ℝ) (M : Foundation.Parabolic.L2Vec3 → ℂ) (hM : MeasureTheory.AEStronglyMeasurable M MeasureTheory.volume) (C : ℝ) (hC : 0 ≤ C) (hMC : ∀ (ξ : Foundation.Parabolic.L2Vec3), ‖M ξ‖ ≤ C * (1 + ‖ξ‖ ^ 2)) (G : ℝ → ↥(MeasureTheory.Lp E 2 MeasureTheory.volume)) (hMC1 : ∀ (ξ : Foundation.Parabolic.L2Vec3), ‖ξ‖ * ‖M ξ‖ ≤ C * (1 + ‖ξ‖ ^ 2)) (z : Foundation.Parabolic.ParabolicPoint) : DifferentiableAt ℝ (fun (x : Foundation.Parabolic.Vec3) => regR12SpaceTimeField c M G (x, z.2)) z.1 ∧ ∀ (j : Fin 3), spatialPartial (regR12SpaceTimeField c M G) j z = regR12SpaceTimeField c (fun (ξ : Foundation.Parabolic.L2Vec3) => regR12CoordSymbol j ξ * M ξ) G z

The spatial slices of the space-time field are differentiable, with the coordinate partial derivatives given by multiplication by 2πi ξ_j.

theorem CKN.Leray.regR12_continuousOn_of_prod {F : Foundation.Parabolic.ParabolicPoint → ℝ} {S : Set (Foundation.Parabolic.Vec3 × ℝ)} (hF : ContinuousOn (fun (z : Foundation.Parabolic.Vec3 × ℝ) => F (z.1, z.2)) S) : ContinuousOn F S

Continuity for the product topology gives continuity for the parabolic topology of ParabolicPoint.