Probability · medium

Statement, exactly as the model and Lean see it

theorem lg_target {b x : ℝ} (hb : 0 < b) : MeasureTheory.IntegrableOn (fun x => Real.exp (-(b * x))) (Set.Ioc 0 x) MeasureTheory.volume := by

Mathlib declaration: ProbabilityTheory.exp_neg_integrableOn_Ioc
Held-out module: Mathlib.Probability.Distributions.Exponential
Banned modules (itself + downstream): 1
Reference proof premises (reachable / held-out): 4 / 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.00004

Attempts

sample 0 · round 0Wrong tactic2.1 s model time

Proof

intro hb
apply MeasureTheory.integrableOn_exp_neg_linear
exact hb

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

b x : ℝ
hb : 0 < b
⊢ MeasureTheory.IntegrableOn (fun x => Real.exp (-(b * x))) (Set.Ioc 0 x) MeasureTheory.volume

Reference proof

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

/-- A negative exponential function is integrable on intervals in `R≥0` -/
lemma exp_neg_integrableOn_Ioc {b x : ℝ} (hb : 0 < b) :
    IntegrableOn (fun x ↦ rexp (-(b * x))) (Ioc 0 x) := by
  simp only [neg_mul_eq_neg_mul]
  exact (exp_neg_integrableOn_Ioi _ hb).mono_set Ioc_subset_Ioi_self