Probability · hard

Statement, exactly as the model and Lean see it

theorem lg_target {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} (ht_int_pos : MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ) (ht_int_neg : MeasureTheory.Integrable (fun ω => Real.exp (-t * X ω)) μ) : MeasureTheory.Integrable (fun ω => Real.exp (|t| * |X ω|)) μ := by

Mathlib declaration: ProbabilityTheory.integrable_exp_abs_mul_abs
Held-out module: Mathlib.Probability.Moments.IntegrableExpMul
Banned modules (itself + downstream): 20
Reference proof premises (reachable / held-out): 6 / 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.00007

Attempts

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

Proof

intros ht_int_pos ht_int_neg
apply MeasureTheory.integrable_norm
exact (MeasureTheory.integrable_abs ht_int_pos).1
exact (MeasureTheory.integrable_abs ht_int_neg).1

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

4:2: 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 Ω
t : ℝ
ht_int_pos : MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ
ht_int_neg : MeasureTheory.Integrable (fun ω => Real.exp (-t * X ω)) μ
⊢ 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.

/-- If `ω ↦ exp (t * X ω)` is integrable at `t` and `-t`, then `ω ↦ exp (|t| * |X ω|)` is
integrable. -/
lemma integrable_exp_abs_mul_abs (ht_int_pos : Integrable (fun ω ↦ exp (t * X ω)) μ)
    (ht_int_neg : Integrable (fun ω ↦ exp (-t * X ω)) μ) :
    Integrable (fun ω ↦ exp (|t| * |X ω|)) μ := by
  rcases le_total 0 t with ht_nonneg | ht_nonpos
  · simp_rw [abs_of_nonneg ht_nonneg]
    exact integrable_exp_mul_abs ht_int_pos ht_int_neg
  · simp_rw [abs_of_nonpos ht_nonpos]
    exact integrable_exp_mul_abs ht_int_neg (by simpa using ht_int_pos)