Probability · medium

Statement, exactly as the model and Lean see it

theorem lg_target {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (h : 0 ∈ interior (ProbabilityTheory.integrableExpSet X μ)) (n : ℕ) : iteratedDeriv n (ProbabilityTheory.mgf X μ) 0 = ∫ (x : Ω), (X ^ n) x ∂μ := by

Mathlib declaration: ProbabilityTheory.iteratedDeriv_mgf_zero
Held-out module: Mathlib.Probability.Moments.MGFAnalytic
Banned modules (itself + downstream): 18
Reference proof premises (reachable / held-out): 3 / 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.00005

Attempts

sample 0 · round 0Wrong tactic1.3 s model time

Proof

intro n
apply ProbabilityTheory.mgf_deriv_at_zero
exact h

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

4:8: error: Tactic `introN` failed: There are no additional binders or `let` bindings in the goal to introduce

Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : MeasureTheory.Measure Ω
h : 0 ∈ interior (ProbabilityTheory.integrableExpSet X μ)
n : ℕ
⊢ iteratedDeriv n (ProbabilityTheory.mgf X μ) 0 = ∫ (x : Ω), (X ^ n) x ∂μ

Reference proof

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

/-- The derivatives of the moment-generating function at zero are the moments. -/
lemma iteratedDeriv_mgf_zero (h : 0 ∈ interior (integrableExpSet X μ)) (n : ℕ) :
    iteratedDeriv n (mgf X μ) 0 = μ[X ^ n] := by
  simp [iteratedDeriv_mgf h n]