theorem ENNReal.rpow_max {x y : ENNReal} {p : ℝ} (hp : 0 ≤ p) : max x y ^ p = max (x ^ p) (y ^ p)

theorem ENNReal.rpow_add_le_two_rpow_mul_add_rpow {p : ℝ} (a b : ENNReal) (hp : 0 ≤ p) : (a + b) ^ p ≤ 2 ^ p * (a ^ p + b ^ p)

theorem ENNReal.sum_geometric_two_le (n : ℕ) : ∑ i ∈ Finset.range n, (1 / 2) ^ i ≤ 2

theorem ENNReal.ofReal_one_div {x : ℝ} (hx : 0 < x) : ENNReal.ofReal (1 / x) = 1 / ENNReal.ofReal x

theorem ENNReal.le_one_div_iff {x y : ENNReal} : x ≤ 1 / y ↔ y ≤ 1 / x

theorem ENNReal.rpow_add_of_add_pos {x : ENNReal} (hx : x ≠ ⊤) (y z : ℝ) (hyz : 0 < y + z) : x ^ (y + z) = x ^ y * x ^ z