Scalar Grönwall closure for weak energy estimates

The parabolic uniqueness argument reduces the squared norm of the difference to a homogeneous integral Grönwall inequality. This lemma packages that final implication.

theorem AVenhance.Infra.Parabolic.WeakUniqueness.continuous_nonneg_eq_zero_of_integral_gronwall {f : ℝ → ℝ} (hf : Continuous f) {C : ℝ} (hC : 0 ≤ C) (hf_nonneg : ∀ t ∈ Set.Icc 0 1, 0 ≤ f t) (hineq : ∀ t ∈ Set.Icc 0 1, f t ≤ C * ∫ (s : ℝ) in 0..t, f s) (t : ℝ) : t ∈ Set.Icc 0 1 → f t = 0

A nonnegative continuous function satisfying a homogeneous integral Grönwall bound vanishes on the whole interval.