awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.RadonNikodym
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
⊢ 0 ≤ 1 - κ.rnDerivAux (κ + η) a x

Tactic:
simp only [sub_nonneg, hx.le]

Premises used: LT.lt.le, sub_nonneg
-- Module: Mathlib.Probability.Kernel.RadonNikodym
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
⊢ 0 < 1 - κ.rnDerivAux (κ + η) a x

Tactic:
simp only [sub_pos, hx]

Premises used: sub_pos
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsSFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
s : Set γ
hs : s ⊆ (κ.mutuallySingularSetSlice η a)ᶜ
⊢ Eq (α := ℝ≥0∞) ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
measure_mono_null hs (singularPart_compl_mutuallySingularSetSlice κ η a)

Premises used: MeasureTheory.measure_mono_null, ProbabilityTheory.Kernel.singularPart_compl_mutuallySingularSetSlice
-- Module: Mathlib.Probability.Kernel.RadonNikodym
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
⊢ ∀ x ∈ s, 1 ≤ κ.rnDerivAux (κ + η) a x

Tactic:
have hs' : ∀ x ∈ s, 1 ≤ rnDerivAux κ (κ + η) a x := fun _ hx ↦ hs hx
-- Module: Mathlib.Probability.Kernel.RadonNikodym
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
hf :
  Measurable (α := α × γ) (β := ℝ≥0∞)
    (Function.uncurry fun (a : α) (x : γ) ↦
      (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) -
        (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) * κ.rnDeriv η a x)
⊢ Eq (α := ℝ≥0∞) ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [singularPart, Kernel.withDensity_apply']

Premises used: ProbabilityTheory.Kernel.singularPart, ProbabilityTheory.Kernel.withDensity_apply'
-- Module: Mathlib.Probability.Kernel.RadonNikodym
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
⊢ Measurable (α := α × γ) (β := ℝ≥0∞)
    (Function.uncurry fun (a : α) (x : γ) ↦
      (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) -
        (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) * κ.rnDeriv η a x)

Tactic:
measurable_singularPart_fun κ η

Premises used: ProbabilityTheory.Kernel.measurable_singularPart_fun
-- Module: Mathlib.Probability.Kernel.RadonNikodym
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
⊢ Measurable (α := α × γ) (β := ℝ≥0∞)
    (Function.uncurry fun (a : α) (x : γ) ↦
      (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) -
        (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) * κ.rnDeriv η a x)

Tactic:
exact measurable_singularPart_fun κ η

Premises used: ProbabilityTheory.Kernel.measurable_singularPart_fun
-- Module: Mathlib.Probability.Kernel.RadonNikodym
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

Tactic:
setLIntegral_congr_fun_ae hsm ?_

Premises used: MeasureTheory.setLIntegral_congr_fun_ae
-- Module: Mathlib.Probability.Kernel.RadonNikodym
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
refine :
  ∀ᵐ (x : γ) ∂((κ + η : (a : α) → Measure γ) a : Measure γ),
    x ∈ s →
      (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) -
          (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) * κ.rnDeriv η a x =
        1
⊢ ∫⁻ (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:
refine setLIntegral_congr_fun_ae hsm ?_

Premises used: MeasureTheory.setLIntegral_congr_fun_ae
-- Module: Mathlib.Probability.Kernel.RadonNikodym
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
⊢ κ ≤ κ + η

Tactic:
have h_le : κ ≤ κ + η := le_add_of_nonneg_right bot_le
-- Module: Mathlib.Probability.Kernel.RadonNikodym
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 : κ ≤ κ + η
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
⊢ ∀ᵐ (x : γ) ∂((κ + η : (a : α) → Measure γ) a : Measure γ),
    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

Premises used: ProbabilityTheory.Kernel.rnDerivAux_le_one
-- Module: Mathlib.Probability.Kernel.RadonNikodym
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 = 1

Tactic:
have h_eq_one : rnDerivAux κ (κ + η) a x = 1 := le_antisymm hx (hs' x hxs)
-- Module: Mathlib.Probability.Kernel.RadonNikodym
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
h_eq_one : κ.rnDerivAux (κ + η) a x = 1
⊢ (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) - (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) * κ.rnDeriv η a x =
    1

Tactic:
simp [h_eq_one]
-- Module: Mathlib.Probability.Kernel.RadonNikodym
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, 1 ∂(κ + η : (a : α) → Measure γ) a =
    (((κ + η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.RadonNikodym
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
this : Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ + η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp [this]
-- Module: Mathlib.Probability.Kernel.RadonNikodym
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
suffices : Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ + η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
suffices η a s = 0 by simp [this]
-- Module: Mathlib.Probability.Kernel.RadonNikodym
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∞) (0 : ℝ≥0∞)

Tactic:
measure_mono_null hs (measure_mutuallySingularSetSlice κ η a)

Premises used: MeasureTheory.measure_mono_null, ProbabilityTheory.Kernel.measure_mutuallySingularSetSlice
-- Module: Mathlib.Probability.Kernel.RadonNikodym
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∞) (0 : ℝ≥0∞)

Tactic:
exact measure_mono_null hs (measure_mutuallySingularSetSlice κ η a)

Premises used: MeasureTheory.measure_mono_null, ProbabilityTheory.Kernel.measure_mutuallySingularSetSlice
-- Module: Mathlib.Probability.Kernel.RadonNikodym
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
x₂ :
  Eq (α := ℝ≥0∞) ((((κ + η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ∫⁻ (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:
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)

Premises used: HAdd.hAdd, DFunLike.coe
-- Module: Mathlib.Probability.Kernel.RadonNikodym
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
hf : Measurable (Function.uncurry (κ.rnDeriv η))
⊢ Eq (α := ℝ≥0∞)
    ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (κ.mutuallySingularSetSlice η a) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
rw [Kernel.withDensity_apply']

Premises used: ProbabilityTheory.Kernel.withDensity_apply'
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
⊢ ∫⁻ (b : γ) in κ.mutuallySingularSetSlice η a, κ.rnDeriv η a b ∂(η : (a : α) → Measure γ) a = 0

Tactic:
setLIntegral_measure_zero _ _ (measure_mutuallySingularSetSlice κ η a)

Premises used: ProbabilityTheory.Kernel.measure_mutuallySingularSetSlice, MeasureTheory.setLIntegral_measure_zero
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
⊢ ∫⁻ (b : γ) in κ.mutuallySingularSetSlice η a, κ.rnDeriv η a b ∂(η : (a : α) → Measure γ) a = 0

Tactic:
exact setLIntegral_measure_zero _ _ (measure_mutuallySingularSetSlice κ η a)

Premises used: ProbabilityTheory.Kernel.measure_mutuallySingularSetSlice, MeasureTheory.setLIntegral_measure_zero
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
⊢ Measurable (Function.uncurry (κ.rnDeriv η))

Tactic:
measurable_rnDeriv κ η

Premises used: ProbabilityTheory.Kernel.measurable_rnDeriv
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
⊢ Measurable (Function.uncurry (κ.rnDeriv η))

Tactic:
exact measurable_rnDeriv κ η

Premises used: ProbabilityTheory.Kernel.measurable_rnDeriv
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
s : Set γ
hs : s ⊆ κ.mutuallySingularSetSlice η a
⊢ Eq (α := ℝ≥0∞) ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
measure_mono_null hs (withDensity_rnDeriv_mutuallySingularSetSlice κ η a)

Premises used: MeasureTheory.measure_mono_null, ProbabilityTheory.Kernel.withDensity_rnDeriv_mutuallySingularSetSlice
-- Module: Mathlib.Probability.Kernel.RadonNikodym
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)ᶜ
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)
⊢ η.withDensity (κ.rnDeriv η) =
    ((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)).withDensity
      (κ.rnDeriv η)

Tactic:
rw [rnDeriv_def']

Premises used: ProbabilityTheory.Kernel.rnDeriv_def'
-- Module: Mathlib.Probability.Kernel.RadonNikodym
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)ᶜ
e_κ : η = (κ + η).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)) =
    ((κ + η).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:
congr
-- Module: Mathlib.Probability.Kernel.RadonNikodym
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 fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)

Tactic:
(withDensity_one_sub_rnDerivAux κ η).symm

Premises used: ProbabilityTheory.Kernel.withDensity_one_sub_rnDerivAux, Eq.symm
-- Module: Mathlib.Probability.Kernel.RadonNikodym
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 fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)

Tactic:
exact (withDensity_one_sub_rnDerivAux κ η).symm

Premises used: ProbabilityTheory.Kernel.withDensity_one_sub_rnDerivAux, Eq.symm
-- Module: Mathlib.Probability.Kernel.RadonNikodym
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 η)

Tactic:
have : withDensity η (rnDeriv κ η)
      = withDensity (withDensity (κ + η)
        (fun a x ↦ Real.toNNReal (1 - rnDerivAux κ (κ + η) a x))) (rnDeriv κ η) := by
    rw [rnDeriv_def']
    congr
    exact (withDensity_one_sub_rnDerivAux κ η).symm
-- Module: Mathlib.Probability.Kernel.RadonNikodym
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)ᶜ
this :
  η.withDensity (κ.rnDeriv η) =
    ((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)).withDensity
      (κ.rnDeriv η)
rw :
  ∫⁻ (b : γ) in s,
      (↑(1 - κ.rnDerivAux (κ + η) a b).toNNReal : ℝ≥0∞) * κ.rnDeriv η a b ∂(κ + η : (a : α) → Measure γ) a =
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s
hf :
  Measurable (α := α × γ) (β := ℝ≥0∞)
    (Function.uncurry fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) * κ.rnDeriv η a x)
hf₁ :
  Measurable (α := α × γ) (β := ℝ≥0) (Function.uncurry fun (a : α) (x : γ) ↦ (1 - κ.rnDerivAux (κ + η) a x).toNNReal)
hg : Measurable (Function.uncurry (κ.rnDeriv η))
⊢ Eq (α := ℝ≥0∞) ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [this, ← withDensity_mul, Kernel.withDensity_apply']

Premises used: ProbabilityTheory.Kernel.withDensity_apply', ProbabilityTheory.Kernel.withDensity_mul
-- Module: Mathlib.Probability.Kernel.RadonNikodym
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)ᶜ
this :
  η.withDensity (κ.rnDeriv η) =
    ((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)).withDensity
      (κ.rnDeriv η)
⊢ Measurable (α := α × γ) (β := ℝ≥0∞)
    (Function.uncurry fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) * κ.rnDeriv η a x)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.RadonNikodym
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)ᶜ
this :
  η.withDensity (κ.rnDeriv η) =
    ((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)).withDensity
      (κ.rnDeriv η)
⊢ Measurable (α := α × γ) (β := ℝ≥0) (Function.uncurry fun (a : α) (x : γ) ↦ (1 - κ.rnDerivAux (κ + η) a x).toNNReal)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.RadonNikodym
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)ᶜ
this :
  η.withDensity (κ.rnDeriv η) =
    ((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)).withDensity
      (κ.rnDeriv η)
⊢ Measurable (Function.uncurry (κ.rnDeriv η))

Tactic:
measurable_rnDeriv _ _

Premises used: ProbabilityTheory.Kernel.measurable_rnDeriv