Probability · hard

Statement, exactly as the model and Lean see it

theorem lg_target {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (hXmeas : AEMeasurable X μ) (hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1) : ∫ (x : Ω), X x ∂μ = μ.real {ω | X ω = 1} := by

Mathlib declaration: MeasureTheory.integral_of_ae_eq_zero_or_one
Held-out module: Mathlib.Probability.Distributions.TwoValued
Banned modules (itself + downstream): 1
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.

No configuration has attempted this theorem yet.

Reference proof

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

/-- If an `AEMeasurable` function is ae equal to `0` or `1`, then its integral is equal to the
measure of the set where it equals `1`. -/
lemma integral_of_ae_eq_zero_or_one (hXmeas : AEMeasurable X μ) (hX : ∀ᵐ ω ∂μ, X ω = 0 ∨ X ω = 1) :
    μ[X] = μ.real {ω | X ω = 1} := by
  refine (integral_map (f := id) hXmeas <| by fun_prop).symm.trans ?_
  rw [(Measure.ae_eq_or_eq_iff_map_eq_dirac_add_dirac hXmeas zero_ne_one).1 hX]
  by_cases h : μ {ω | X ω = 1} = ⊤
  · simp [h, Measure.real, Set.preimage, integral_undef, Integrable, HasFiniteIntegral]
  rw [integral_add_measure ⟨by fun_prop, by simp [HasFiniteIntegral]⟩ <|
    .smul_measure (by simp [integrable_dirac]) h]
  simp [Measure.real, Set.preimage]