Utility lemmas

theorem exp_neg_le_one_sub_add_sq_div_two (x : ℝ) (hx : 0 ≤ x) : Real.exp (-x) ≤ 1 - x + x ^ 2 / 2

exp(-x) ≤ 1 - x + x²/2 for x ≥ 0. Second-order Taylor upper bound for exp(-x).

theorem rpow_one_sub_le_exp_neg (p t : ℝ) (hp1 : p ≤ 1) (ht : 0 ≤ t) : (1 - p) ^ t ≤ Real.exp (-p * t)

(1 - p) ^ t ≤ exp(-p * t) for 0 ≤ p, p ≤ 1, and t ≥ 0.

theorem rpow_upper_bound_quadratic (p t : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (ht : 0 ≤ t) : (1 - p) ^ t ≤ 1 - p * t + (p * t) ^ 2 / 2

Second-order quadratic upper bound: (1 - p) ^ t ≤ 1 - p*t + (p*t)²/2 for 0 ≤ p ≤ 1 and t ≥ 0.

theorem quadratic_le_zero_of_le_sqrt_two_sub_one (s : ℝ) (hs0 : 0 ≤ s) (hs : s ≤ √2 - 1) : s ^ 2 + 2 * s - 1 ≤ 0

s² + 2s - 1 ≤ 0 when 0 ≤ s ≤ √2 - 1. The quadratic s² + 2s - 1 = (s + 1)² - 2 has positive root √2 - 1.

theorem one_sub_ge_rpow_of_pk_le_sqrt2_sub_one (p k : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (gnn : 0 ≤ k) (h : p * k ≤ √2 - 1) : 1 - p * k ≥ (1 - p) ^ ((1 + p * k) * k)

Lemma 21 from Pǎtraşcu and Thorup, "The Power of Simple Tabulation Hashing" (arXiv:1011.5200). The paper states a strict inequality, but the proof only establishes ≥: equality holds at the boundary cases p = 0 or k = 0.

theorem sum_fiber_card {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq β] (f : α → β) : ∑ b : β, Fintype.card ↑{a : α | f a = b} = Fintype.card α

The fiber cardinalities of a function partition the domain: ∑ b, |f⁻¹(b)| = |α|.

This is the Fintype version of Finset.card_eq_sum_card_fiberwise over the full universe.