Sum-of-squares inequalities for ℝ≥0∞

Cauchy-Schwarz-style inequalities relating sums, products, and squares over ℝ≥0∞. These are used in the forking lemma and other game-hopping arguments.

theorem ENNReal.two_mul_le_add_sq (a b : ENNReal) : 2 * a * b ≤ a ^ 2 + b ^ 2

theorem ENNReal.sq_sum_le_card_mul_sum_sq {ι' : Type u_1} (s : Finset ι') (f : ι' → ENNReal) : (∑ i ∈ s, f i) ^ 2 ≤ ↑s.card * ∑ i ∈ s, f i ^ 2

theorem ENNReal.sq_sum_div_card_le_sum_sq {ι' : Type u_1} (s : Finset ι') (f : ι' → ENNReal) : (∑ i ∈ s, f i) ^ 2 / ↑s.card ≤ ∑ i ∈ s, f i ^ 2

Divided Cauchy-Schwarz: (∑ i, f i)² / card ≤ ∑ i, (f i)². Derived from sq_sum_le_card_mul_sum_sq by dividing both sides by s.card. Holds unconditionally in ℝ≥0∞: when s = ∅ the left-hand side reduces to 0 / 0 = 0.

theorem ENNReal.sq_tsum_le_tsum_mul_tsum {α : Type u_1} (w f : α → ENNReal) : (∑' (a : α), w a * f a) ^ 2 ≤ (∑' (a : α), w a) * ∑' (a : α), w a * f a ^ 2

theorem ENNReal.sq_tsum_le_tsum_sq {α : Type u_1} (w f : α → ENNReal) (hw : ∑' (a : α), w a ≤ 1) : (∑' (a : α), w a * f a) ^ 2 ≤ ∑' (a : α), w a * f a ^ 2

theorem ENNReal.mul_tsub_div_le_one {a q r : ENNReal} (ha : a ≤ 1) (hq : 1 ≤ q) : a * (a / q - r) ≤ 1

A simple ENNReal upper bound used in the forking lemma: if a ≤ 1 and q ≥ 1, then a * (a / q - r) is still bounded by 1, regardless of r.