Documentation

Lean 4 Proof

theorem uniform_collision_probability {J : ℕ} (hJ : 0 < J) :
    ∑ _j : Fin J, ((1 : ℝ) / ↑J) ^ 2 = 1 / (↑J : ℝ) := by
  simp [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
  have hJr : (↑J : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (by omega)
  field_simp

Dependency Graph

Location

thesis/CESProofs/Foundations/AggregationInvariantClass.lean:78

Module Section

Aggregation-invariant class results from Paper 1, Section 5:

In the same file