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.mul_finset_sum_of_nonneg (n : ℕ) (c : EReal) (f : Fin n → EReal) (hf : ∀ (i : Fin n), 0 ≤ f i) : c * ∑ i : Fin n, f i = ∑ i : Fin n, c * f i

Multiplication distributes over finite sums for EReal when all summands are non-negative. This is needed because EReal lacks a general LeftDistribClass instance.

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, Real.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 sumletsum 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

theorem EReal.tsum_le_of_sum_range_le_of_nonneg {f : ℕ → EReal} {M : EReal} (h_nn : ∀ (n : ℕ), 0 ≤ f n) (h : ∀ (N : ℕ), ∑ n ∈ Finset.range N, f n ≤ M) : ∑' (n : ℕ), f n ≤ M

If all partial sums of a nonnegative EReal sequence are bounded by M, then the tsum is bounded by M. This is a generalization of ENNReal.tsum_le_of_sum_range_le to EReal.

theorem EReal.tsum_coe_ennreal_eq_top_of_tsum_eq_top {α : Type u_1} {f : α → ENNReal} (h : ∑' (i : α), f i = ⊤) : ∑' (i : α), ↑(f i) = ⊤

If tsum in ENNReal equals ⊤, then tsum of coerced values in EReal equals ⊤. Uses that ENNReal → EReal coercion is continuous and additive.

theorem EReal.tsum_const_eq_top_of_pos {α : Type u_1} [Infinite α] {c : EReal} (hc : 0 < c) : ∑' (x : α), c = ⊤

Tsum of a positive constant over an infinite type is ⊤ in EReal