Conversion of actual quadratic energies to the norm used in l.V. The differentiated PDE energy inequality must still be derived separately.

theorem AVenhance.Infra.Section4.iterate_norm_sum_sq_le_energy {e g κ : ℝ} (he : 0 ≤ e) (hg : 0 ≤ g) (hκ : 0 ≤ κ) : (√e + √κ * √g) ^ 2 ≤ 2 * (e + κ * g)

The sum of the two nonnegative norm components costs at most twice its quadratic energy. This isolates square roots from energy bookkeeping.