awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
a : α
x : γ
rw : (a, x) ∈ κ.mutuallySingularSet η ↔ x ∈ κ.mutuallySingularSetSlice η a
rw₁ :
  Membership.mem (γ := Set (α × γ)) {p : α × γ | 1 ≤ κ.rnDerivAux (κ + η) p.1 p.2} (a, x) ↔
    x ∈ κ.mutuallySingularSetSlice η a
rw₂ :
  Membership.mem (γ := Set (α × γ)) {p : α × γ | 1 ≤ κ.rnDerivAux (κ + η) p.1 p.2} (a, x) ↔
    Membership.mem (γ := Set γ) {x : γ | 1 ≤ κ.rnDerivAux (κ + η) a x} x
rw₃ : 1 ≤ κ.rnDerivAux (κ + η) (a, x).1 (a, x).2 ↔ Membership.mem (γ := Set γ) {x : γ | 1 ≤ κ.rnDerivAux (κ + η) a x} x
⊢ κ.rnDeriv η a x = ∞ ↔ x ∈ κ.mutuallySingularSetSlice η a
have rw₄ : 1 ≤ κ.rnDerivAux (κ + η) (a, x).1 (a, x).2 ↔ 1 ≤ κ.rnDerivAux (κ + η) a x
Tactic: rw [rnDeriv_eq_top_iff, mutuallySingularSet, mutuallySingularSetSlice, mem_setOf, mem_setOf]
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
a : α
⊢ Measurable (β := ℝ≥0∞) fun (x : γ) ↦
    (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) - (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) * κ.rnDeriv η a x
have change : Measurable.{u_2, 0} (α := γ) (β := ℝ≥0∞)
  (Function.comp (β := α × γ)
    (Function.uncurry fun (a : α) (b : γ) ↦
      ENNReal.ofReal (κ.rnDerivAux (κ + η) a b) - ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a b) * κ.rnDeriv η a b)
    fun (b : γ) ↦ (a, b))
Tactic: change Measurable ((Function.uncurry fun a b ↦
    ENNReal.ofReal (rnDerivAux κ (κ + η) a b)
    - ENNReal.ofReal (1 - rnDerivAux κ (κ + η) a b) * rnDeriv κ η a b) ∘ (fun b ↦ (a, b)))
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
a : α
⊢ Eq (α := ℝ≥0∞)
    ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a)ᶜ :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
have rw : ∀ᵐ (x : γ) ∂((κ + η : (a : α) → Measure γ) a : Measure γ),
  x ∈ (κ.mutuallySingularSetSlice η a)ᶜ →
    (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) -
        (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) * κ.rnDeriv η a x =
      0 x
Tactic: rw [singularPart, Kernel.withDensity_apply', lintegral_eq_zero_iff, EventuallyEq,
    ae_restrict_iff]
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
a : α
rw :
  ∀ᵐ (x : γ) ∂((κ + η : (a : α) → Measure γ) a : Measure γ),
    x ∈ (κ.mutuallySingularSetSlice η a)ᶜ →
      (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) -
          (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) * κ.rnDeriv η a x =
        0 x
⊢ Eq (α := ℝ≥0∞)
    ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a)ᶜ :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
have rw₁ : MeasurableSet.{u_2} (α := γ)
  {x : γ |
    (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) -
        (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) * κ.rnDeriv η a x =
      0 x}
Tactic: rw [singularPart, Kernel.withDensity_apply', lintegral_eq_zero_iff, EventuallyEq,
    ae_restrict_iff]
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
a : α
rw :
  ∀ᵐ (x : γ) ∂((κ + η : (a : α) → Measure γ) a : Measure γ),
    x ∈ (κ.mutuallySingularSetSlice η a)ᶜ →
      (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) -
          (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) * κ.rnDeriv η a x =
        0 x
rw₁ :
  MeasurableSet.{u_2} (α := γ)
    {x : γ |
      (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) -
          (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) * κ.rnDeriv η a x =
        0 x}
⊢ Eq (α := ℝ≥0∞)
    ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a)ᶜ :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
have rw₂ : Measurable (β := ℝ≥0∞) fun (b : γ) ↦
  (↑(κ.rnDerivAux (κ + η) a b).toNNReal : ℝ≥0∞) - (↑(1 - κ.rnDerivAux (κ + η) a b).toNNReal : ℝ≥0∞) * κ.rnDeriv η a b
Tactic: rw [singularPart, Kernel.withDensity_apply', lintegral_eq_zero_iff, EventuallyEq,
    ae_restrict_iff]
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
a : α
rw :
  ∀ᵐ (x : γ) ∂((κ + η : (a : α) → Measure γ) a : Measure γ),
    x ∈ (κ.mutuallySingularSetSlice η a)ᶜ →
      (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) -
          (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) * κ.rnDeriv η a x =
        0 x
rw₁ :
  MeasurableSet.{u_2} (α := γ)
    {x : γ |
      (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) -
          (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) * κ.rnDeriv η a x =
        0 x}
rw₂ :
  Measurable (β := ℝ≥0∞) fun (b : γ) ↦
    (↑(κ.rnDerivAux (κ + η) a b).toNNReal : ℝ≥0∞) - (↑(1 - κ.rnDerivAux (κ + η) a b).toNNReal : ℝ≥0∞) * κ.rnDeriv η a b
⊢ Eq (α := ℝ≥0∞)
    ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a)ᶜ :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
have hf : Measurable (α := α × γ) (β := ℝ≥0∞)
  (Function.uncurry fun (a : α) (x : γ) ↦
    (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) - (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) * κ.rnDeriv η a x)
Tactic: rw [singularPart, Kernel.withDensity_apply', lintegral_eq_zero_iff, EventuallyEq,
    ae_restrict_iff]
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
a : α
⊢ ∀ᵐ (x : γ) ∂((κ + η : (a : α) → Measure γ) a : Measure γ),
    x ∈ (κ.mutuallySingularSetSlice η a)ᶜ →
      ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) - ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) * κ.rnDeriv η a x = 0 x
have refine : ∀ (x : γ) (hx : x ∈ (κ.mutuallySingularSetSlice η a)ᶜ),
  ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) - ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) * κ.rnDeriv η a x = 0 x
Tactic: refine ae_of_all _ (fun x hx ↦ ?_)
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (hypothesis)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
a : α
x : γ
hx : x ∈ (κ.mutuallySingularSetSlice η a)ᶜ
⊢ ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) - ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) * κ.rnDeriv η a x = 0 x
have hx₁ : κ.rnDerivAux (κ + η) a x < 1
Tactic: simp only [mem_compl_iff, mutuallySingularSetSlice, mem_setOf, not_le] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
a : α
x : γ
hx : κ.rnDerivAux (κ + η) a x < 1
⊢ ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) - ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) * κ.rnDeriv η a x = 0 x
have simp_rw : ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) -
    ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) *
      (ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x)) =
  0 x
Tactic: simp_rw [rnDeriv]
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
a : α
x : γ
hx : κ.rnDerivAux (κ + η) a x < 1
⊢ ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) -
      ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) *
        (ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x)) =
    0 x
have rw : 1 - κ.rnDerivAux (κ + η) a x ≠ 0
Tactic: rw [← ENNReal.ofReal_div_of_pos, div_eq_inv_mul, ← ENNReal.ofReal_mul, ← mul_assoc,
    mul_inv_cancel₀, one_mul, tsub_self, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
a : α
x : γ
hx : κ.rnDerivAux (κ + η) a x < 1
rw : 1 - κ.rnDerivAux (κ + η) a x ≠ 0
⊢ ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) -
      ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) *
        (ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x)) =
    0 x
have rw₁ : 0 ≤ 1 - κ.rnDerivAux (κ + η) a x
Tactic: rw [← ENNReal.ofReal_div_of_pos, div_eq_inv_mul, ← ENNReal.ofReal_mul, ← mul_assoc,
    mul_inv_cancel₀, one_mul, tsub_self, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
a : α
x : γ
hx : κ.rnDerivAux (κ + η) a x < 1
rw : 1 - κ.rnDerivAux (κ + η) a x ≠ 0
rw₁ : 0 ≤ 1 - κ.rnDerivAux (κ + η) a x
⊢ ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) -
      ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) *
        (ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x)) =
    0 x
have rw₂ : 0 < 1 - κ.rnDerivAux (κ + η) a x
Tactic: rw [← ENNReal.ofReal_div_of_pos, div_eq_inv_mul, ← ENNReal.ofReal_mul, ← mul_assoc,
    mul_inv_cancel₀, one_mul, tsub_self, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (hypothesis)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
s : Set γ
hsm : MeasurableSet s
hs : s ⊆ κ.mutuallySingularSetSlice η a
⊢ Eq (α := ℝ≥0∞) ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
have hs' : ∀ x ∈ s, 1 ≤ κ.rnDerivAux (κ + η) a x
Tactic: have hs' : ∀ x ∈ s, 1 ≤ rnDerivAux κ (κ + η) a x := fun _ hx ↦ hs hx
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
s : Set γ
hsm : MeasurableSet s
hs : s ⊆ κ.mutuallySingularSetSlice η a
hs' : ∀ x ∈ s, 1 ≤ κ.rnDerivAux (κ + η) a x
⊢ Eq (α := ℝ≥0∞) ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
have rw : ∫⁻ (b : γ) in s,
    (↑(κ.rnDerivAux (κ + η) a b).toNNReal : ℝ≥0∞) -
      (↑(1 - κ.rnDerivAux (κ + η) a b).toNNReal : ℝ≥0∞) * κ.rnDeriv η a b ∂(κ + η : (a : α) → Measure γ) a =
  (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s
Tactic: rw [singularPart, Kernel.withDensity_apply']
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
s : Set γ
hsm : MeasurableSet s
hs : s ⊆ κ.mutuallySingularSetSlice η a
hs' : ∀ x ∈ s, 1 ≤ κ.rnDerivAux (κ + η) a x
rw :
  ∫⁻ (b : γ) in s,
      (↑(κ.rnDerivAux (κ + η) a b).toNNReal : ℝ≥0∞) -
        (↑(1 - κ.rnDerivAux (κ + η) a b).toNNReal : ℝ≥0∞) * κ.rnDeriv η a b ∂(κ + η : (a : α) → Measure γ) a =
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s
⊢ Eq (α := ℝ≥0∞) ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
have hf : Measurable (α := α × γ) (β := ℝ≥0∞)
  (Function.uncurry fun (a : α) (x : γ) ↦
    (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) - (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) * κ.rnDeriv η a x)
Tactic: rw [singularPart, Kernel.withDensity_apply']
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
s : Set γ
hsm : MeasurableSet s
hs : s ⊆ κ.mutuallySingularSetSlice η a
hs' : ∀ x ∈ s, 1 ≤ κ.rnDerivAux (κ + η) a x
⊢ ∫⁻ (x : γ) in s,
      (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) -
        (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) * κ.rnDeriv η a x ∂(κ + η : (a : α) → Measure γ) a =
    ∫⁻ (x : γ) in s, 1 ∂(κ + η : (a : α) → Measure γ) a
have refine : ∀ᵐ (x : γ) ∂((κ + η : (a : α) → Measure γ) a : Measure γ),
  x ∈ s →
    (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) -
        (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) * κ.rnDeriv η a x =
      1
Tactic: refine setLIntegral_congr_fun_ae hsm ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (hypothesis)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
s : Set γ
hsm : MeasurableSet s
hs : s ⊆ κ.mutuallySingularSetSlice η a
hs' : ∀ x ∈ s, 1 ≤ κ.rnDerivAux (κ + η) a x
⊢ ∀ᵐ (x : γ) ∂((κ + η : (a : α) → Measure γ) a : Measure γ),
    x ∈ s →
      (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) -
          (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) * κ.rnDeriv η a x =
        1
have h_le : κ ≤ κ + η
Tactic: have h_le : κ ≤ κ + η := le_add_of_nonneg_right bot_le
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
s : Set γ
hsm : MeasurableSet s
hs : s ⊆ κ.mutuallySingularSetSlice η a
hs' : ∀ x ∈ s, 1 ≤ κ.rnDerivAux (κ + η) a x
h_le : κ ≤ κ + η
⊢ ∀ᵐ (x : γ) ∂((κ + η : (a : α) → Measure γ) a : Measure γ),
    x ∈ s →
      (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) -
          (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) * κ.rnDeriv η a x =
        1
have h : ∀ (x : γ) (hx : κ.rnDerivAux (κ + η) a x ≤ 1 x) (hxs : x ∈ s),
  (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) - (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) * κ.rnDeriv η a x =
    1
Tactic: filter_upwards [rnDerivAux_le_one h_le] with x hx hxs
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (hypothesis)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
s : Set γ
hsm : MeasurableSet s
hs : s ⊆ κ.mutuallySingularSetSlice η a
hs' : ∀ x ∈ s, 1 ≤ κ.rnDerivAux (κ + η) a x
h_le : κ ≤ κ + η
x : γ
hx : κ.rnDerivAux (κ + η) a x ≤ 1 x
hxs : x ∈ s
⊢ (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) - (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) * κ.rnDeriv η a x =
    1
have h_eq_one : κ.rnDerivAux (κ + η) a x = 1
Tactic: have h_eq_one : rnDerivAux κ (κ + η) a x = 1 := le_antisymm hx (hs' x hxs)
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
s : Set γ
hsm : MeasurableSet s
hs : s ⊆ κ.mutuallySingularSetSlice η a
hs' : ∀ x ∈ s, 1 ≤ κ.rnDerivAux (κ + η) a x
⊢ Eq (α := ℝ≥0∞) ((((κ + η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
have suffices : Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: suffices η a s = 0 by simp [this]
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
s : Set γ
hsm : MeasurableSet s
hs : s ⊆ κ.mutuallySingularSetSlice η a
hs' : ∀ x ∈ s, 1 ≤ κ.rnDerivAux (κ + η) a x
⊢ ∫⁻ (b : γ) in s,
      (↑(κ.rnDerivAux (κ + η) a b).toNNReal : ℝ≥0∞) -
        (↑(1 - κ.rnDerivAux (κ + η) a b).toNNReal : ℝ≥0∞) * κ.rnDeriv η a b ∂(κ + η : (a : α) → Measure γ) a =
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s
have x : ∫⁻ (x : γ) in s,
    (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) -
      (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) * κ.rnDeriv η a x ∂(κ + η : (a : α) → Measure γ) a =
  ∫⁻ (x : γ) in s, 1 ∂(κ + η : (a : α) → Measure γ) a
Tactic: calc
    ∫⁻ x in s, ↑(Real.toNNReal (rnDerivAux κ (κ + η) a x)) -
      ↑(Real.toNNReal (1 - rnDerivAux κ (κ + η) a x)) * rnDeriv κ η a x
      ∂(κ + η) a
    = ∫⁻ _ in s, 1 ∂(κ + η) a := by
        refine setLIntegral_congr_fun_ae hsm ?_
        have h_le : κ ≤ κ + η := le_add_of_nonneg_right bot_le
        filter_upwards [rnDerivAux_le_one h_le] with x hx hxs
        have h_eq_one : rnDerivAux κ (κ + η) a x = 1 := le_antisymm hx (hs' x hxs)
        simp [h_eq_one]
  _ = (κ + η) a s := by simp
  _ = κ a s := by
        suffices η a s = 0 by simp [this]
        exact measure_mono_null hs (measure_mutuallySingularSetSlice κ η a)
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
s : Set γ
hsm : MeasurableSet s
hs : s ⊆ κ.mutuallySingularSetSlice η a
hs' : ∀ x ∈ s, 1 ≤ κ.rnDerivAux (κ + η) a x
x :
  ∫⁻ (x : γ) in s,
      (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) -
        (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) * κ.rnDeriv η a x ∂(κ + η : (a : α) → Measure γ) a =
    ∫⁻ (x : γ) in s, 1 ∂(κ + η : (a : α) → Measure γ) a
⊢ ∫⁻ (b : γ) in s,
      (↑(κ.rnDerivAux (κ + η) a b).toNNReal : ℝ≥0∞) -
        (↑(1 - κ.rnDerivAux (κ + η) a b).toNNReal : ℝ≥0∞) * κ.rnDeriv η a b ∂(κ + η : (a : α) → Measure γ) a =
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s
have x₁ : ∫⁻ (x : γ) in s, 1 ∂(κ + η : (a : α) → Measure γ) a =
  (((κ + η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s
Tactic: calc
    ∫⁻ x in s, ↑(Real.toNNReal (rnDerivAux κ (κ + η) a x)) -
      ↑(Real.toNNReal (1 - rnDerivAux κ (κ + η) a x)) * rnDeriv κ η a x
      ∂(κ + η) a
    = ∫⁻ _ in s, 1 ∂(κ + η) a := by
        refine setLIntegral_congr_fun_ae hsm ?_
        have h_le : κ ≤ κ + η := le_add_of_nonneg_right bot_le
        filter_upwards [rnDerivAux_le_one h_le] with x hx hxs
        have h_eq_one : rnDerivAux κ (κ + η) a x = 1 := le_antisymm hx (hs' x hxs)
        simp [h_eq_one]
  _ = (κ + η) a s := by simp
  _ = κ a s := by
        suffices η a s = 0 by simp [this]
        exact measure_mono_null hs (measure_mutuallySingularSetSlice κ η a)
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
s : Set γ
hsm : MeasurableSet s
hs : s ⊆ κ.mutuallySingularSetSlice η a
hs' : ∀ x ∈ s, 1 ≤ κ.rnDerivAux (κ + η) a x
x :
  ∫⁻ (x : γ) in s,
      (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) -
        (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) * κ.rnDeriv η a x ∂(κ + η : (a : α) → Measure γ) a =
    ∫⁻ (x : γ) in s, 1 ∂(κ + η : (a : α) → Measure γ) a
x₁ :
  ∫⁻ (x : γ) in s, 1 ∂(κ + η : (a : α) → Measure γ) a =
    (((κ + η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s
⊢ ∫⁻ (b : γ) in s,
      (↑(κ.rnDerivAux (κ + η) a b).toNNReal : ℝ≥0∞) -
        (↑(1 - κ.rnDerivAux (κ + η) a b).toNNReal : ℝ≥0∞) * κ.rnDeriv η a b ∂(κ + η : (a : α) → Measure γ) a =
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s
have x₂ : Eq (α := ℝ≥0∞) ((((κ + η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
  ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: calc
    ∫⁻ x in s, ↑(Real.toNNReal (rnDerivAux κ (κ + η) a x)) -
      ↑(Real.toNNReal (1 - rnDerivAux κ (κ + η) a x)) * rnDeriv κ η a x
      ∂(κ + η) a
    = ∫⁻ _ in s, 1 ∂(κ + η) a := by
        refine setLIntegral_congr_fun_ae hsm ?_
        have h_le : κ ≤ κ + η := le_add_of_nonneg_right bot_le
        filter_upwards [rnDerivAux_le_one h_le] with x hx hxs
        have h_eq_one : rnDerivAux κ (κ + η) a x = 1 := le_antisymm hx (hs' x hxs)
        simp [h_eq_one]
  _ = (κ + η) a s := by simp
  _ = κ a s := by
        suffices η a s = 0 by simp [this]
        exact measure_mono_null hs (measure_mutuallySingularSetSlice κ η a)
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
⊢ Eq (α := ℝ≥0∞)
    ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (κ.mutuallySingularSetSlice η a) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
have rw : ∫⁻ (b : γ) in κ.mutuallySingularSetSlice η a, κ.rnDeriv η a b ∂(η : (a : α) → Measure γ) a = 0
Tactic: rw [Kernel.withDensity_apply']
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
rw : ∫⁻ (b : γ) in κ.mutuallySingularSetSlice η a, κ.rnDeriv η a b ∂(η : (a : α) → Measure γ) a = 0
⊢ Eq (α := ℝ≥0∞)
    ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (κ.mutuallySingularSetSlice η a) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
have hf : Measurable (Function.uncurry (κ.rnDeriv η))
Tactic: rw [Kernel.withDensity_apply']
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
s : Set γ
hsm : MeasurableSet s
hs : s ⊆ (κ.mutuallySingularSetSlice η a)ᶜ
⊢ η.withDensity (κ.rnDeriv η) =
    ((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)).withDensity
      (κ.rnDeriv η)
have rw : (η.withDensity fun (a : α) (x : γ) ↦
    ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x)) =
  ((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)).withDensity
    fun (a : α) (x : γ) ↦ ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x)
Tactic: rw [rnDeriv_def']