Abstract real step for the sup-in-time stream-difference estimate #
theorem
AVenhance.Infra.FullTheorem.Uniform.forced_sup_real
{κ η A B C E l : ℝ}
(hκ : 0 < κ)
(hη : 0 ≤ η)
(hA : 0 ≤ A)
(hB : 0 ≤ B)
(hE0 : 0 ≤ E)
(hid : l + 2 * κ * A = -2 * C)
(hCE : C ^ 2 ≤ E * A)
(hE : E ≤ η ^ 2 * B)
:
From the energy balance l + 2κA = -2C, Cauchy–Schwarz C² ≤ E A, and E ≤ η² B,
conclude √l ≤ (η/κ) (√κ √B).