Probability · easy

Statement, exactly as the model and Lean see it

theorem lg_target (r : NNReal) : HasSum (fun n => Real.exp (-↑r) * ↑r ^ n / ↑n.factorial) 1 := by

Mathlib declaration: ProbabilityTheory.poissonPMFRealSum
Held-out module: Mathlib.Probability.Distributions.Poisson.Basic
Banned modules (itself + downstream): 2
Reference proof premises (reachable / held-out): 0 / 1

Traces

Each configuration's full record: what was retrieved, what the model wrote, what Lean said back.

Not verified1 model calls · 1 Lean checks · $0.00016

Attempts

sample 0 · round 0Syntax error5.1 s model time

Proof

let f := fun n => Real.exp (-↑r) * ↑r ^ n / ↑n.factorial
let s := ∑' f
have h0 : 0 < r := by simp [NNReal.pos]
let hf : ∀ n, 0 < f n :=
  fun n => (Real.exp_pos _).mul (Nat.pow_pos r n).div (Nat.factorial_pos n)
have h1 : ∑' f = Real.exp (-↑r) * ∑' (fun n => ↑r ^ n / ↑n.factorial) :=
  by rw [sum_const_mul]
have h2 : ∑' (fun n => ↑r ^ n / ↑n.factorial) = Real.exp ↑r :=
  by
    let g := fun n => ↑r ^ n / ↑n.factorial
    have hg : ∀ n, 0 < g n :=
      fun n => (Nat.pow_pos r n).div (Nat.factorial_pos n)
    have h3 : ∑' g = Real.exp ↑r :=
      by
        apply sum_exp_series
        exact h0
    exact h3
rw [h1, h2]
exact Real.exp_neg_eq_inv (Real.exp ↑r)

What Lean printed (this is all the model sees on repair)

5:15: error: unexpected token 'have'; expected ','

Reference proof

Mathlib's own source for this declaration, shown for comparison. It may use lemmas the prover is not allowed to use.

@[deprecated (since := "2026-03-08")]
alias poissonPMFRealSum := hasSum_one_poissonMeasure