A fundamental lemma for scalar weak tests #
A continuous function on the closed unit time interval is determined by its pairings with smooth tests supported in the open interval. This is the separation step used after subtracting the integral primitive of a Fourier coefficient's forcing.
theorem
AVenhance.Infra.Parabolic.WeakUniqueness.continuous_eq_zero_of_smooth_interior_tests
{f : ℝ → ℝ}
(hf : Continuous f)
(hzero :
∀ (g : ℝ → ℝ), ContDiff ℝ (↑⊤) g → HasCompactSupport g → tsupport g ⊆ Set.Ioo 0 1 → ∫ (t : ℝ) in 0..1, f t * g t = 0)
(t : ℝ)
:
A continuous time function that pairs to zero with every smooth compactly supported interior test vanishes at every time, including the endpoints.