Space-time tests in frequency variables

A smooth compactly supported space-time vector test has, at every time, a Schwartz slice; its spatial transform is jointly continuous in frequency and time, differentiable in time with the transform of the time derivative as derivative, turns spatial derivatives into multiplication by 2πiξⱼ, and is square integrable in frequency and time. These are the test transforms in the frequency form of eq:reg-momentum-forced.

noncomputable def CKN.Leray.spaceDeriv (j : Fin 3) (φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3

The spatial partial derivative of a space-time field.

Equations

• CKN.Leray.spaceDeriv j φ z = (fderiv ℝ φ z) (CKN.basisVec j, 0)

noncomputable def CKN.Leray.timeDeriv (φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3

The time derivative of a space-time field.

Equations

• CKN.Leray.timeDeriv φ z = (fderiv ℝ φ z) (0, 1)

theorem CKN.Leray.contDiff_fderiv_apply {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : ContDiff ℝ (↑⊤) φ) (v : Foundation.Parabolic.Vec3 × ℝ) : ContDiff ℝ ↑⊤ fun (z : Foundation.Parabolic.Vec3 × ℝ) => (fderiv ℝ φ z) v

theorem CKN.Leray.hasCompactSupport_fderiv_apply {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφc : HasCompactSupport φ) (v : Foundation.Parabolic.Vec3 × ℝ) : HasCompactSupport fun (z : Foundation.Parabolic.Vec3 × ℝ) => (fderiv ℝ φ z) v

theorem CKN.Leray.contDiff_spaceDeriv {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : ContDiff ℝ (↑⊤) φ) (j : Fin 3) : ContDiff ℝ (↑⊤) (spaceDeriv j φ)

theorem CKN.Leray.hasCompactSupport_spaceDeriv {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφc : HasCompactSupport φ) (j : Fin 3) : HasCompactSupport (spaceDeriv j φ)

theorem CKN.Leray.contDiff_timeDeriv {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : ContDiff ℝ (↑⊤) φ) : ContDiff ℝ (↑⊤) (timeDeriv φ)

theorem CKN.Leray.hasCompactSupport_timeDeriv {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφc : HasCompactSupport φ) : HasCompactSupport (timeDeriv φ)

theorem CKN.Leray.contDiff_slice {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : ContDiff ℝ (↑⊤) φ) (t : ℝ) : ContDiff ℝ ↑⊤ fun (x : Foundation.Parabolic.Vec3) => φ (x, t)

theorem CKN.Leray.hasCompactSupport_slice {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφc : HasCompactSupport φ) (t : ℝ) : HasCompactSupport fun (x : Foundation.Parabolic.Vec3) => φ (x, t)

theorem CKN.Leray.hasFDerivAt_slice {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : ContDiff ℝ (↑⊤) φ) (x : Foundation.Parabolic.Vec3) (t : ℝ) : HasFDerivAt (fun (y : Foundation.Parabolic.Vec3) => φ (y, t)) (fderiv ℝ φ (x, t) ∘SL ContinuousLinearMap.inl ℝ Foundation.Parabolic.Vec3 ℝ) x

theorem CKN.Leray.hasDerivAt_time_slice {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : ContDiff ℝ (↑⊤) φ) (x : Foundation.Parabolic.Vec3) (t : ℝ) : HasDerivAt (fun (s : ℝ) => φ (x, s)) (timeDeriv φ (x, t)) t

theorem CKN.Leray.spatialPartial_eq_spaceDeriv {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : ContDiff ℝ (↑⊤) φ) (i j : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) : spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) j z = spaceDeriv j φ z i

The CKN spatial partial derivative of a component is the component of the spatial partial derivative.

theorem CKN.Leray.timePartial_eq_timeDeriv {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : ContDiff ℝ (↑⊤) φ) (i : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) : timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) z = timeDeriv φ z i

The CKN time partial derivative of a component is the component of the time derivative.

noncomputable def CKN.Leray.testHat (φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.L2Vec3 × ℝ) : ComplexVec3

The spatial transform of the time slices of a space-time test.

Equations

• CKN.Leray.testHat φ p = FourierTransform.fourier (CKN.Leray.testField fun (x : CKN.Foundation.Parabolic.Vec3) => φ (x, p.2)) p.1

theorem CKN.Leray.testHat_eq_integral (φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.L2Vec3 × ℝ) : testHat φ p = ∫ (y : Foundation.Parabolic.L2Vec3), Real.fourierChar (-inner ℝ y p.1) • testField (fun (x : Foundation.Parabolic.Vec3) => φ (x, p.2)) y

theorem CKN.Leray.testHat_eq_zero {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} {t : ℝ} (h : ∀ (x : Foundation.Parabolic.Vec3), φ (x, t) = 0) (ξ : Foundation.Parabolic.L2Vec3) : testHat φ (ξ, t) = 0

theorem CKN.Leray.exists_testField_bound {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) : ∃ (b : Foundation.Parabolic.L2Vec3 → ℝ), MeasureTheory.Integrable b MeasureTheory.volume ∧ MeasureTheory.Integrable (fun (y : Foundation.Parabolic.L2Vec3) => b y ^ 2) MeasureTheory.volume ∧ ∀ (t : ℝ) (y : Foundation.Parabolic.L2Vec3), ‖testField (fun (x : Foundation.Parabolic.Vec3) => φ (x, t)) y‖ ≤ b y

The slices of a smooth compactly supported test are dominated by one square-integrable function.

theorem CKN.Leray.continuous_testHat {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) : Continuous (testHat φ)

theorem CKN.Leray.hasDerivAt_testHat {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (ξ : Foundation.Parabolic.L2Vec3) (t : ℝ) : HasDerivAt (fun (s : ℝ) => testHat φ (ξ, s)) (testHat (timeDeriv φ) (ξ, t)) t

The transform of a test is differentiable in time, with the transform of the time derivative as derivative.

theorem CKN.Leray.testHat_spaceDeriv {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (j : Fin 3) (p : Foundation.Parabolic.L2Vec3 × ℝ) : testHat (spaceDeriv j φ) p = (2 * ↑Real.pi * Complex.I * ↑(p.1.ofLp j)) • testHat φ p

The transform turns a spatial derivative into multiplication by 2πiξⱼ.

theorem CKN.Leray.integrable_testHat_sq {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (T : ℝ) : MeasureTheory.Integrable (fun (p : Foundation.Parabolic.L2Vec3 × ℝ) => ‖testHat φ p‖ ^ 2) (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc 0 T)))

The transform of a test is square integrable in frequency and time.