FormalConjecturesForMathlib/Probability/FiniteMethod.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

2 declarations, 0 contain sorry, 0 declared as axioms

The finite probabilistic method (averaging / pigeonhole primitive)

This file provides the core averaging lemma underlying the elementary form of Erdős's probabilistic method:

If the sum of a ℕ-valued function f over a finite set s is strictly less than the cardinality of s, then f vanishes somewhere on s.

Interpreting f a as "the number of bad configurations caused by choice a", and sampling a uniformly from s, the expected number of bad configurations is (∑ f) / |s| < 1, so there must exist at least one a ∈ s with f a = 0.

This is used by:

Both the ℕ-form and a convenience ℝ-form are provided; the latter is useful when the expectation bound is derived via rpow/log manipulations on the reals and only later cast back to counting.

References

Imports (3)
Imported by 1 file
  1. theorem FormalConjecturesForMathlib.Probability.Finset.exists_eq_zero_of_sum_lt_card Finite probabilistic method (integer form) line 63 source

    Source documentation

    Finite probabilistic method (integer form).

    If ∑ x ∈ s, f x < s.card, then there exists a ∈ s with f a = 0.

    Proof idea. Contrapositive: if every value is at least 1, the sum is at least s.card · 1 = s.card, contradicting the hypothesis.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Finset, Nat, LT.lt, Finset.sum, Finset.card, Exists, And, Membership.mem, Eq, OfNat.ofNat

    Proof uses: Decidable.byContradiction, Not, LE.le, Iff.mpr, Ne, Nat.one_le_iff_ne_zero, Eq.mp, Eq.trans, binderNameHint, forall_congr, Mathlib.Tactic.Push.not_and_eq, Trans.trans, Eq.mpr, HSMul.hSMul, id, congrArg, Finset.sum_const, HMul.hMul, smul_eq_mul, mul_one and 2 more

    31 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

    Open to load the checked before-and-after goal states.

    theorem Finset.exists_eq_zero_of_sum_lt_card
    {α : Type*} {s : Finset α} {f : α → ℕ} (h : ∑ x ∈ s, f x < s.card) :
    ∃ a ∈ s, f a = 0 := by
…
  2. theorem FormalConjecturesForMathlib.Probability.Finset.exists_eq_zero_of_real_sum_lt_card Finite probabilistic method (real form) line 82 source

    Source documentation

    Finite probabilistic method (real form).

    If (∑ x ∈ s, (f x : ℝ)) < s.card, then there exists a ∈ s with f a = 0.

    This is the same statement as Finset.exists_eq_zero_of_sum_lt_card after casting the counting inequality to ℝ; it is the convenient entry point when f arises as an expectation whose bound was computed in the reals (e.g. via Real.rpow / Real.log).

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Finset, Nat, LT.lt, Real, Finset.sum, Finset.card, Exists, And, Membership.mem, Eq, OfNat.ofNat

    Proof uses: FormalConjecturesForMathlib.Probability.Finset.exists_eq_zero_of_sum_lt_card, Nat.cast_sum, Eq.rec, Eq.symm, cast

    31 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

    Open to load the checked before-and-after goal states.

    theorem Finset.exists_eq_zero_of_real_sum_lt_card
    {α : Type*} {s : Finset α} {f : α → ℕ}
    (h : (∑ x ∈ s, (f x : ℝ)) < s.card) : ∃ a ∈ s, f a = 0 := by
…