Probability · hard

Statement, exactly as the model and Lean see it

theorem lg_target {y z : ℝ} (f : ℝ → ENNReal) (hzy : z ≤ y) : ∫⁻ (x : ℝ) in Set.Iic y, f x = (∫⁻ (x : ℝ) in Set.Iio z, f x) + ∫⁻ (x : ℝ) in Set.Icc z y, f x := by

Mathlib declaration: lintegral_Iic_eq_lintegral_Iio_add_Icc
Held-out module: Mathlib.Probability.Distributions.Gamma
Banned modules (itself + downstream): 2
Reference proof premises (reachable / held-out): 44 / 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.00005

Attempts

sample 0 · round 0Hallucinated theorem10.1 s model time

Proof

rw [Iic_eq_Iio_union_Icc, integral_add]

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

4:6: error: Unknown identifier `Iic_eq_Iio_union_Icc`
3:160: error: unsolved goals
y z : ℝ
f : ℝ → ENNReal
hzy : z ≤ y
⊢ ∫⁻ (x : ℝ) in Set.Iic y, f x = (∫⁻ (x : ℝ) in Set.Iio z, f x) + ∫⁻ (x : ℝ) in Set.Icc z y, f x

Reference proof

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

/-- A Lebesgue Integral from -∞ to y can be expressed as the sum of one from -∞ to 0 and 0 to x -/
lemma lintegral_Iic_eq_lintegral_Iio_add_Icc {y z : ℝ} (f : ℝ → ℝ≥0∞) (hzy : z ≤ y) :
    ∫⁻ x in Iic y, f x = (∫⁻ x in Iio z, f x) + ∫⁻ x in Icc z y, f x := by
  rw [← Iio_union_Icc_eq_Iic hzy, lintegral_union measurableSet_Icc]
  simp_rw [Set.disjoint_iff_forall_ne, mem_Iio, mem_Icc]
  intros
  linarith