Solenoidal cutoff time limits

Time differentiation and convergence for the Helmholtz cutoff curl.

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

The componentwise time derivative of the Helmholtz vector potential.

Equations

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

theorem CKN.Leray.associatedPressureHelmholtzCutoffCurl_timePartial_eq {T : ℝ} {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : φ ∈ spaceTimeTestFunction Set.univ (Set.Ioo 0 T)) (n : ℕ) (i : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) : associatedPressureTestTimePartial (fun (w : Foundation.Parabolic.Vec3 × ℝ) => associatedPressureTestCurl (associatedPressureHelmholtzCutoffVectorPotential φ n) w i) z = associatedPressureTestCurl (fun (q : Foundation.Parabolic.Vec3 × ℝ) => rieszPressurePotentialCutoff n q.1 • associatedPressureHelmholtzVectorPotentialTimePartial φ q) z i

The time derivative of the cutoff curl is the curl of the cutoff time derivative of the vector potential.

theorem CKN.Leray.associatedPressureHelmholtzCutoffCurl_timePartial_eventually_eq {T : ℝ} {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : φ ∈ spaceTimeTestFunction Set.univ (Set.Ioo 0 T)) (i : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) : ∀ᶠ (n : ℕ) in Filter.atTop, associatedPressureTestTimePartial (fun (w : Foundation.Parabolic.Vec3 × ℝ) => associatedPressureTestCurl (associatedPressureHelmholtzCutoffVectorPotential φ n) w i) z = associatedPressureTestTimePartial (fun (w : Foundation.Parabolic.Vec3 × ℝ) => associatedPressureTestCurl (associatedPressureHelmholtzVectorPotential φ) w i) z

At each fixed point, the cutoff curl time derivative eventually agrees with the full Helmholtz curl time derivative.