Spatial regularity of scalar Fourier fields

A bounded continuous path of scalar frequency fields with four Bessel derivatives gives spatially differentiable real slices. The first spatial partials are continuous and share a uniform bound with the field. This is the scalar field estimate used for the pressure in thm:regularised (R2).

theorem CKN.Leray.regR12ScalarPressureField_sliceC1_bound (G : ℝ → ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (hG : Continuous G) (B : ℝ) (hB : ∀ (t : ℝ), ‖G t‖ ≤ B) : (∀ (z : Foundation.Parabolic.ParabolicPoint), DifferentiableAt ℝ (fun (x : Foundation.Parabolic.Vec3) => regR12SpaceTimeField Complex.reCLM (fun (x : Foundation.Parabolic.L2Vec3) => 1) G (x, z.2)) z.1) ∧ (∀ (j : Fin 3), Continuous fun (z : Foundation.Parabolic.Vec3 × ℝ) => spatialPartial (regR12SpaceTimeField Complex.reCLM (fun (x : Foundation.Parabolic.L2Vec3) => 1) G) j z) ∧ ∀ (z : Foundation.Parabolic.ParabolicPoint), |regR12SpaceTimeField Complex.reCLM (fun (x : Foundation.Parabolic.L2Vec3) => 1) G z| ≤ ‖Complex.reCLM‖ * ((1 + 2 * Real.pi) * ((MeasureTheory.eLpNorm regR12Kernel 2 MeasureTheory.volume).toReal * B)) ∧ ∀ (j : Fin 3), |spatialPartial (regR12SpaceTimeField Complex.reCLM (fun (x : Foundation.Parabolic.L2Vec3) => 1) G) j z| ≤ ‖Complex.reCLM‖ * ((1 + 2 * Real.pi) * ((MeasureTheory.eLpNorm regR12Kernel 2 MeasureTheory.volume).toReal * B))

Slice differentiability, continuity of first spatial partials, and a common pointwise bound for a scalar H⁴ Fourier field.