Pointwise recovery from the space-time weak equation

A continuous residual that pairs to zero with every smooth compactly supported scalar test vanishes at every interior positive-time point.

theorem CKN.Leray.regularised_continuousResidual_eq_zero_of_tests (T : ℝ) (R : Foundation.Parabolic.Vec3 × ℝ → ℝ) (hRcont : ContinuousOn R (Set.univ ×ˢ Set.Ioo 0 T)) (hzero : ∀ (ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ Set.univ ×ˢ Set.Ioo 0 T → ∫ (z : Foundation.Parabolic.Vec3 × ℝ) in Set.univ ×ˢ Set.Ioo 0 T, R z * ψ z = 0) (z : Foundation.Parabolic.Vec3 × ℝ) : z ∈ Set.univ ×ˢ Set.Ioo 0 T → R z = 0

A continuous scalar residual with zero pairing against all smooth tests supported inside (0,T) is pointwise zero there.