Probability · medium

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.hasSum_one_poissonMeasure
Held-out module: Mathlib.Probability.Distributions.Poisson.Basic
Banned modules (itself + downstream): 2
Reference proof premises (reachable / held-out): 13 / 0

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.

lemma hasSum_one_poissonMeasure (r : ℝ≥0) : HasSum (fun n ↦ exp (-r) * r ^ n / (n)!) 1 := by
  convert! (NormedSpace.expSeries_div_hasSum_exp (r : ℝ)).mul_left (exp (-r)) using 1
  · simp_rw [mul_div_assoc]
  · simp [← exp_eq_exp_ℝ, ← exp_add]