General utilities for Real, EReal, and ENNReal

This file contains general-purpose lemmas about Real, EReal, and ENNReal that are not specific to measure theory but are used throughout the formalization.

theorem max_div_two (x : ℝ) : max x 0 / 2 = max (x / 2) 0

max distributes over division by 2

theorem Real.sqrt_add_le_add_sqrt {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) : √(x + y) ≤ √x + √y

The square root function is subadditive: √(x + y) ≤ √x + √y for non-negative reals. This follows from the fact that (√x + √y)² = x + y + 2√(xy) ≥ x + y.

theorem Real.sqrt_sum_le_sum_sqrt {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : ι → ℝ) (hf : ∀ (i : ι), 0 ≤ f i) : √(∑ i : ι, f i) ≤ ∑ i : ι, √(f i)

The square root function is subadditive over finite sums: √(∑ᵢ xᵢ) ≤ ∑ᵢ √xᵢ for non-negative terms. This is a consequence of the concavity of sqrt.

theorem EReal.lt_add_of_pos_coe {x : EReal} {ε : ℝ} (hε : 0 < ε) (h_ne_bot : x ≠ ⊥) (h_ne_top : x ≠ ⊤) : x < x + ↑ε

For EReal, adding a positive real value to a value that is neither ⊥ nor ⊤ gives a strictly greater result.

theorem EReal.le_of_forall_pos_le_add' {a b : EReal} (h : ∀ (ε : ℝ), 0 < ε → a ≤ b + ↑ε) : a ≤ b

EReal epsilon argument: if for all positive ε, a ≤ b + ε, then a ≤ b. This holds when b ≠ ⊤ (if b = ⊤, the implication is trivially true).

theorem EReal.coe_finset_sum {α : Type u_1} {s : Finset α} {f : α → ℝ} (hf : ∀ a ∈ s, 0 ≤ f a) : ↑(∑ a ∈ s, f a) = ∑ a ∈ s, ↑(f a)

For non-negative reals, toEReal commutes with finite sums. Uses induction on the finset with EReal.coe_add.

theorem Summable.coe_ennreal {α : Type u_1} {f : α → ENNReal} : Summable fun (x : α) => ↑(f x)

Helper: Coercion from ENNReal to EReal preserves summability. All ENNReal sequences are summable, and their coercions to EReal are also summable.

theorem EReal.tsum_add_coe_ennreal {α : Type u_1} {a b : α → ENNReal} : ∑' (n : α), ↑(a n) + ∑' (n : α), ↑(b n) = ∑' (n : α), ↑(a n + b n)

Helper: Addition of tsums of ENNReal values coerced to EReal. (∑' n, ↑(a n) : EReal) + (∑' n, ↑(b n) : EReal) = (∑' n, ↑(a n + b n) : EReal)

This follows from ENNReal.tsum_add and the fact that coercion commutes with addition.

theorem EReal.coe_ennreal_finset_sum {α : Type u_1} {s : Finset α} {f : α → ENNReal} : ↑(∑ a ∈ s, f a) = ∑ a ∈ s, ↑(f a)

ENNReal coercion to EReal commutes with finite sums

theorem EReal.finset_sum_le_tsum {f : ℕ → ℝ} (hf : ∀ (n : ℕ), 0 ≤ f n) (t : Finset ℕ) : ∑ n ∈ t, ↑(f n) ≤ ∑' (n : ℕ), ↑(f n)

Finite sum embedded in EReal is bounded by tsum. For nonnegative reals, finite partial sums are always ≤ the infinite sum. Strategy: Convert to ENNReal where sum_le_tsum holds, then transfer via coercion.

theorem EReal.tsum_add_le_of_nonneg_pointwise {f g h : ℕ → ℝ} (hf_nn : ∀ (n : ℕ), 0 ≤ f n) (hg_nn : ∀ (n : ℕ), 0 ≤ g n) (h_pw : ∀ (n : ℕ), f n + g n ≤ h n) : ∑' (n : ℕ), ↑(f n) + ∑' (n : ℕ), ↑(g n) ≤ ∑' (n : ℕ), ↑(h n)

Helper: For non-negative real sequences, tsum addition inequality in EReal. If f n + g n ≤ h n pointwise, then ∑' f.toEReal + ∑' g.toEReal ≤ ∑' h.toEReal.

theorem EReal.tsum_le_coe_tsum_of_forall_le {f : ℕ → EReal} {g : ℕ → ℝ} (hf_nn : ∀ (n : ℕ), 0 ≤ f n) (hg_nn : ∀ (n : ℕ), 0 ≤ g n) (hg_sum : Summable g) (h_le : ∀ (n : ℕ), f n ≤ ↑(g n)) : ∑' (n : ℕ), f n ≤ ∑' (n : ℕ), ↑(g n)

Pointwise EReal ≤ nonneg Real implies tsum inequality. If 0 ≤ f n ≤ ↑(g n) for all n, where g n ≥ 0 and g summable, then ∑' f ≤ ↑(∑' g). Routes through ENNReal where tsum comparison is unconditional.

theorem EReal.coe_tsum_of_nonneg {g : ℕ → ℝ} (hg_nn : ∀ (n : ℕ), 0 ≤ g n) (hg_sum : Summable g) : ↑(∑' (n : ℕ), g n) = ∑' (n : ℕ), ↑(g n)

Coercion from ℝ to EReal commutes with tsum for nonneg summable sequences. For nonneg g with Summable g: ↑(∑' n, g n : ℝ) = ∑' n, ↑(g n) : EReal