Pointwise separation for regularized time identities

Smooth compactly supported spatial tests determine a continuous vector field on every interior time slice. The same fact recovers pointwise time increments from their spatial pairings.

theorem CKN.Leray.regularisedR12TimeSeparation_eq_zero_of_tests (T : ℝ) {F : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hFcont : ContinuousOn F (Set.univ ×ˢ Set.Ioo 0 T)) (hzero : ∀ (η : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3), ContDiff ℝ (↑⊤) η → HasCompactSupport η → ∀ t ∈ Set.Ioo 0 T, ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, F (x, t) i * η x i = 0) (z : Foundation.Parabolic.Vec3 × ℝ) : z ∈ Set.univ ×ˢ Set.Ioo 0 T → F z = 0

A continuous vector field on a positive-time slab vanishes if all its spatial pairings with smooth compactly supported vector tests vanish.

theorem CKN.Leray.regularisedR12TimeSeparation_eq_zero_of_interval_tests (T : ℝ) {u G : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hu : ContinuousOn u (Set.univ ×ˢ Set.Ioo 0 T)) (hG : ContinuousOn G (Set.univ ×ˢ Set.Ioo 0 T)) (hzero : ∀ (η : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3), ContDiff ℝ (↑⊤) η → HasCompactSupport η → ∀ (t₁ t₂ : ℝ), t₁ < t₂ → t₁ ∈ Set.Ioo 0 T → t₂ ∈ Set.Ioo 0 T → ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, (u (x, t₂) i - u (x, t₁) i - (∫ (s : ℝ) in t₁..t₂, G (x, s)) i) * η x i = 0) (x : Foundation.Parabolic.Vec3) (t₁ t₂ : ℝ) : t₁ < t₂ → t₁ ∈ Set.Ioo 0 T → t₂ ∈ Set.Ioo 0 T → u (x, t₂) - u (x, t₁) = ∫ (s : ℝ) in t₁..t₂, G (x, s)

A pointwise interval increment follows from its spatial test pairings.