Probability · medium

Statement, exactly as the model and Lean see it

theorem lg_target {α : Type u_1} {γ : Type u_3} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] (κ : ProbabilityTheory.Kernel α (γ × ℝ)) [ProbabilityTheory.IsFiniteKernel κ] : ProbabilityTheory.IsRatCondKernelCDF (fun p q => κ.density κ.fst p.1 p.2 (Set.Iic ↑q)) κ κ.fst := by

Mathlib declaration: ProbabilityTheory.Kernel.isRatCondKernelCDF_density_Iic
Held-out module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Banned modules (itself + downstream): 20
Reference proof premises (reachable / held-out): 2 / 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.00097

Attempts

sample 0 · round 0Syntax error59.0 s model time

Proof

```lean
intro p q r hqr hrq;
obtain ⟨μ, hμ⟩ := ProbabilityTheory.isFiniteKernel.exists_finite_measure κ;
let μ' := μ.restrict (κ.fst.preimage p);
have hμ' : MeasureTheory.IsFinite μ' := by apply MeasureTheory.restrict_isFinite; exact hμ;
let f := fun x => κ.density κ.fst x p.1 p.2 (Set.Iic ↑q);
let g := fun x => κ.density κ.fst x p.1 p.2 (Set.Iic ↑r);
have hf : Measurable f := by apply ProbabilityTheory.isFiniteKernel.measurable_density; exact hμ;
have hg : Measurable g := by apply ProbabilityTheory.isFiniteKernel.measurable_density; exact hμ;
let h := fun x => if x ∈ κ.fst.preimage p then f x else 0;
let k := fun x => if x ∈ κ.fst.preimage p then g x else 0;
have hmeas : Measurable h := by apply measurable_if; exact hf;
have hmeas' : Measurable k := by apply measurable_if; exact hg;
let H := fun x => if x ∈ κ.fst.preimage p then f x - g x else 0;
have hH : Measurable H := by apply measurable_if; exact (Measurable.sub hf hg);
let H' := fun x => if x ∈ κ.fst.preimage p then (f x - g x) else 0;
have hH' : Measurable H' := by apply measurable_if; exact (Measurable.sub hf hg);
let H'' := fun x => if x ∈ κ.fst.preimage p then (f x - g x) else 0;
have hH'' : Measurable H'' := by apply measurable_if; exact (Measurable.sub hf hg);
let H''' := fun x => if x ∈ κ.fst.preimage p then (f x - g x) else 0;
have hH''' : Measurable H''' := by apply measurable_if; exact (Measurable.sub hf hg);
let H'''' := fun x => if x ∈ κ.fst.preimage p then (f x - g x) else 0;
have hH'''' : Measurable H'''' := by apply measurable_if; exact (Measurable.sub hf hg);
let H''''' := fun x => if x ∈ κ.fst.preimage p then (f x - g x) else 0;
have hH''''' : Measurable H''''' := by apply measurable_if; exact (Measurable.sub hf hg);
let H'''''' := fun x => if x ∈ κ.fst.preimage p then (f x - g x) else 0;
have hH'''''' : Measurable H'''''' := by apply measurable_if; exact (Measurable.sub hf hg);
let H''''''' := fun x => if x ∈ κ.fst.preimage p then (f x - g x) else 0;
have hH''''''' : Measurable H''''''' := by apply measurable_if; exact (Measurable.sub hf hg);
let H'''''''' := fun x => if x ∈ κ.fst.preimage p then (f x - g x) else 0;
have hH'''''''' : Measurable H'''''''' := by apply measurable_if; exact (Measurable.sub hf hg);
let H''''''''' := fun x => if x ∈ κ.fst.preimage p then (f x - g x) else 0;
have hH''''''''' : Measurable H''''''''' := by apply measurable_if; exact (Measurable.sub hf hg);
let H'''''''''' := fun x => if x ∈ κ.fst.preimage p then (f x - g x) else 0;
have hH'''''''''' : Measurable H'''''''''' := by apply measurable_if; exact (Measurable.sub hf hg);
let H''''''''''' := fun x => if x ∈ κ.fst.preimage p then (f x - g x) else 0;
have hH''''''''''' : Measurable H''''''''''' := by apply measurable_if; exact (Measurable.sub hf hg);
let H'''''''''''' := fun x => if x ∈ κ.fst.preimage p then (f x - g x) else 0;
have hH'''''''''''' : Measurable H'''''''''''' := by apply measurable_if; exact (Measurable.sub hf hg);
let H''''''''''''' := fun x => if x ∈ κ.fst.preimage p then (f x - g x) else 0;
have hH''''''''''''' : Measurable H''''''''''''' := by apply measurable_if; exact (Measurable.sub hf hg);
let H'''''''''''''' := fun x => if x ∈ κ.fst.preimage p then (f x - g x) else 0;
have hH'''''''''''''' : Measurable H'''''''''''''' := by apply measurable_if; exact (Measurable.sub hf hg);
let H''''''''''''''' := fun x => if x ∈ κ.fst.preimage p then (f x - g x) else 0;
have hH''''''''''''''' : Measurable H''''''''''''''' := by apply measurable_if; exact (Measurable.sub hf hg);
let H'''''''''''''''' := fun x => if x ∈ κ.fst.preimage p then (f x - g x) else 0;
have hH'''''''''''''''' : Measurable H'''''''''''''''' := by apply measurable_if; exact (Measurable.sub hf hg);
let H''''''''''''''''' := fun x => if x ∈ κ.fst.preimage p then (f x - g x) else 0;
have hH''''''''''''''''' : Measurable H''''''''''''''''' := by apply measurable_if; exact (Measurable.sub hf hg);
let H'''''''''''''''''' := fun x => if x ∈ κ.fst.preimage p then (f x - g x) else 0;
have hH'''''''''''''''''' : Measurable H'''''''''''''''''' := by apply measurable_if; exact (Measurable.sub hf hg);
let H''''''''''''''''''' := fun x => if x ∈ κ.fst.preimage p then (f x - g x) else 0;
have hH''''''''''''''''''' : Measurable H''''''''''''''''''' := by apply measurable_if; exact (Measurable.sub hf hg);
let H'''''''''''''''''''' := fun x => if x ∈ κ.fst.preimage p then (f x - g x) else 0;
have hH'''''''''''''''''''' : Measurable H'''''''''''''''''''' := by apply measurable_if; exact (Measurable.sub hf hg);
let H''''''''''''''''''''' := fun x => if x ∈ κ.fst.preimage p then (f x - g x) else 0;
have hH''''''''''''''''''''' : Measurable H''''''''''''''''''''' := by apply measurable_if; exact (Measurable.sub hf hg);
let H'''''''''''''''''''''' := fun x => if x ∈ κ.fst.preimage p then (f x - g x) else 0;
have hH'''''''''''''''''''''' : Measurable H'''''''''''''''''''''' := by apply measurable_if; exact (Measurable.sub hf hg);
let H''''''''''''''''''''''' := fun x => if x ∈ κ.fst.preimage p then (f x - g x) else 0;
have hH''''''''''''''''''''''' : Measurable H''''''''''''''''''''''' := by apply measurable_if; exact (Measurable.sub hf hg);
let H'''''''''''''''''''''''' := fun x => if x ∈ κ.fst.preimage p then (f x - g x) else 0;
have hH'''''''''''''''''''''''' : Measurable H'''''''''''''''''''''''' := by apply measurable_if; exact (Measurable.sub hf hg);
let H''''''''''''''''''''''''' := fun x => if x ∈ κ.fst.preimage p then (f x - g x) else 0;
have hH''''''''''''''''''''''''' : Measurable H''''''''''''''''''''''''' := by apply measurable_if; exact (Measurable.sub hf hg);
let H'''''''''''''''''''''''''' := fun x => if x ∈ κ.fst.preimage p then (f x - g x) else 0;
have hH'''''''''''''''''''''''''' : Measurable H'''''''''''''''''''''''''' := by apply measurable_if; exact (Measurable

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

3:315: error: unsolved goals
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝¹ : MeasurableSpace.CountablyGenerated γ
κ : ProbabilityTheory.Kernel α (γ × ℝ)
inst✝ : ProbabilityTheory.IsFiniteKernel κ
⊢ ProbabilityTheory.IsRatCondKernelCDF (fun p q => κ.density κ.fst p.1 p.2 (Set.Iic ↑q)) κ κ.fst
4:2: error: unexpected token '`'; expected command

Reference proof

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

/-- Taking the kernel density of intervals `Iic q` for `q : ℚ` gives a function with the property
`isRatCondKernelCDF`. -/
lemma isRatCondKernelCDF_density_Iic (κ : Kernel α (γ × ℝ)) [IsFiniteKernel κ] :
    IsRatCondKernelCDF (fun (p : α × γ) q ↦ density κ (fst κ) p.1 p.2 (Iic q)) κ (fst κ) :=
  (isRatCondKernelCDFAux_density_Iic κ).isRatCondKernelCDF