Avoid square roots in ENNReal analysis: AM-GM with a free parameter

For bilinear estimates (Cauchy-Schwarz/Hoelder steps) in ℝ≥0∞, use x*y <= ε⁻¹*x^2*v + ε*y^2/v pointwise instead of Hölder. Proof by cases: if y <= ε⁻¹ x v it is immediate; otherwise x <= ε y / v (via ENNReal.le_div_iff_mul_le and mul_inv_cancel). Keep ε (and a scaling τ for f ↦ τ f) free through the whole proof and carry them into the theorem statement. Optimize only at the very end in a separate real lemma: lift to NNReal with lift X to ℝ≥0 using hX, exact_mod_cast after rewriting ← ENNReal.coe_inv, then push_cast to ℝ and choose δ = Real.sqrt(...). Scale only f by τ (not by sqrt τ): τ·Σ ≤ R and then divide by τ.