Supremum absorption for scalar energy estimates.

theorem AVenhance.Infra.ScalarEnergySup.cell_sup_le_of_quadratic_bound {f : ℝ → ℝ} {cell : Set ℝ} {H L D : ℝ} (hnonneg : ∀ t ∈ cell, 0 ≤ f t) (hLD : 0 ≤ L * D) (hFTC : ∀ t ∈ cell, f t ^ 2 ≤ 2 * L * D * H) (hH : ∃ t₀ ∈ cell, H = f t₀ ∧ ∀ t ∈ cell, f t ≤ f t₀) (t : ℝ) : t ∈ cell → f t ≤ 2 * L * D

Absorb an attained supremum from a quadratic energy bound.