Heavy ENNReal Arithmetic Lemmas

Extended-nonnegative-real arithmetic identities whose proofs bridge through ENNReal.toReal and invoke push_cast, ring, nlinarith, or aesop. These proofs are several times more expensive to elaborate than the general-purpose helpers in ToMathlib.General, so they live in a separate module that only the files that need them pull in.

Contents

• ENNReal.one_sub_one_sub_mul_one_sub — the identity 1 - (1-x)(1-y) = x + y - xy used when combining two bounded failure probabilities.
• ENNReal.toReal_sub_le_abs_toReal_sub — real-valued bridge for truncated subtraction.
• ENNReal.gauss_sum_inv_le and ENNReal.gauss_sum_inv_eq — the Gauss sum ∑_{k<n} k/N ≤ n²/(2N) (and its equality variant), the arithmetic core of the birthday bound.
• ENNReal.add_div_two_mul_nat — a nat-cast identity pairing a/(2N) with b/N over the common denominator 2N.

theorem ENNReal.one_sub_one_sub_mul_one_sub {x y : ENNReal} (hx : x ≤ 1) (hy : y ≤ 1) : 1 - (1 - x) * (1 - y) = x + y - x * y

theorem ENNReal.toReal_sub_le_abs_toReal_sub (a b : ENNReal) : (a - b).toReal ≤ |a.toReal - b.toReal|

Real bridge for truncated ENNReal subtraction: (a - b).toReal is bounded by |a.toReal - b.toReal|.

theorem ENNReal.gauss_sum_inv_le (n : ℕ) (N : ENNReal) (_hN : 0 < N) : ∑ k ∈ Finset.range n, ↑k * N⁻¹ ≤ ↑n ^ 2 / (2 * N)

The Gauss sum ∑_{k=0}^{n-1} k/N ≤ n²/(2N), the arithmetic core of the birthday bound.

theorem ENNReal.gauss_sum_inv_eq (n : ℕ) (N : ENNReal) : ∑ k ∈ Finset.range n, ↑k * N⁻¹ = ↑(n * (n - 1)) / (2 * N)

Tight Gauss sum: ∑_{k=0}^{n-1} k/N = n*(n-1)/(2N).

theorem ENNReal.add_div_two_mul_nat (a b N : ℕ) : ↑a / (2 * ↑N) + ↑b * (↑N)⁻¹ = ↑(a + 2 * b) / (2 * ↑N)

a/(2N) + b/N = (a + 2b)/(2N) for natural-number casts to ℝ≥0∞.