Probability · hard

Statement, exactly as the model and Lean see it

theorem lg_target {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} {a b t : ℝ} (hm : AEMeasurable X μ) (hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b) : MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ := by

Mathlib declaration: ProbabilityTheory.integrable_exp_mul_of_mem_Icc
Held-out module: Mathlib.Probability.Moments.Basic
Banned modules (itself + downstream): 21
Reference proof premises (reachable / held-out): 73 / 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.00008

Attempts

sample 0 · round 0Wrong tactic4.7 s model time

Proof

intro t
have hX := hm
have hX_bounded := hb
have h_exp_integrable : MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ :=
  MeasureTheory.integrable_exp_of_bounded_ae hX hX_bounded
exact h_exp_integrable

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 Ω
μ : MeasureTheory.Measure Ω
inst✝ : MeasureTheory.IsFiniteMeasure μ
X : Ω → ℝ
a b t : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
⊢ MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ

Reference proof

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

lemma integrable_exp_mul_of_mem_Icc [IsFiniteMeasure μ] {X : Ω → ℝ} {a b t : ℝ}
    (hm : AEMeasurable X μ) (hb : ∀ᵐ ω ∂μ, X ω ∈ Set.Icc a b) :
    Integrable (fun ω ↦ exp (t * X ω)) μ := by
  apply Integrable.of_mem_Icc (exp (min (a * t) (b * t))) (exp (max (a * t) (b * t)))
  · exact (measurable_exp.comp_aemeasurable (hm.const_mul t))
  filter_upwards [hb] with ω ⟨hl, hr⟩
  simp only [Set.mem_Icc, exp_le_exp, inf_le_iff, le_sup_iff]
  by_cases ht : 0 ≤ t
  · exact ⟨Or.inl (by nlinarith), Or.inr (by nlinarith)⟩
  · exact ⟨Or.inr (by nlinarith), Or.inl (by nlinarith)⟩