Probability · hard

Statement, exactly as the model and Lean see it

theorem lg_target {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ η : ProbabilityTheory.Kernel α γ) [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] : Measurable fun a => (κ a).singularPart (η a) := by

Mathlib declaration: ProbabilityTheory.Kernel.measurable_singularPart
Held-out module: Mathlib.Probability.Kernel.RadonNikodym
Banned modules (itself + downstream): 7
Reference proof premises (reachable / held-out): 4 / 2

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.00006

Attempts

sample 0 · round 0Hallucinated theorem2.0 s model time

Proof

intro a
apply ProbabilityTheory.singularPart_measurable
exact (ProbabilityTheory.isFiniteKernel.singularPart_measurable κ).2
exact (ProbabilityTheory.isFiniteKernel.singularPart_measurable η).2

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

5:8: error: Unknown identifier `ProbabilityTheory.singularPart_measurable`
6:2: error: No goals to be solved

Reference proof

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

/-- For two kernels `κ, η`, the singular part of `κ a` with respect to `η a` is a measurable
function of `a`. -/
lemma measurable_singularPart (κ η : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel η] :
    Measurable (fun a ↦ (κ a).singularPart (η a)) := by
  refine Measure.measurable_of_measurable_coe _ (fun s hs ↦ ?_)
  simp_rw [← κ.singularPart_eq_singularPart_measure, κ.singularPart_def η]
  exact Kernel.measurable_coe _ hs