Basic supremum and rpow lemmas for ENNReal

This file collects auxiliary lemmas about suprema, indexed suprema, and real powers of ENNReal-valued functions used throughout the formalization of the Prékopa–Leindler, Brunn–Minkowski, and isoperimetric inequalities.

theorem biSup_add_biSup {ι : Sort u_1} {κ : Sort u_2} {p : ι → Prop} {q : κ → Prop} (hp : ∃ (i : ι), p i) (hq : ∃ (j : κ), q j) {f : ι → ENNReal} {g : κ → ENNReal} : (⨆ (i : ι), ⨆ (_ : p i), f i) + ⨆ (j : κ), ⨆ (_ : q j), g j = ⨆ (i : ι), ⨆ (j : κ), ⨆ (_ : p i), ⨆ (_ : q j), f i + g j

The sum of two bounded indexed suprema in ENNReal equals the indexed supremum of the pointwise sums.

theorem iSup_nonzero_of_nonzero {f : ℝ → ENNReal} (hf_nonzero : f ≠ 0) : iSup f ≠ 0

A nonzero ENNReal-valued function on ℝ has a nonzero supremum.

theorem iSup_min_nat (a : ENNReal) : ⨆ (n : ℕ), min a ↑n = a

The supremum of min a n over n : ℕ recovers a.

theorem iSup_min_nat_ne_top {ι : Sort u_1} (n : ℕ) (f : ι → ENNReal) : ⨆ (x : ι), min (f x) ↑n ≠ ⊤

The supremum of min (f x) n over a parameter is bounded by n, hence not ⊤.

theorem iSup_rpow_of_pos {ι : Sort u_1} {r : ℝ} (hr : r > 0) (f : ι → ENNReal) : (⨆ (i : ι), f i) ^ r = ⨆ (i : ι), f i ^ r

rpow by a positive real commutes with suprema in ENNReal.