awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η ξ : Kernel α γ
f : α → γ → ℝ≥0∞
inst : IsFiniteKernel η
h : κ = η.withDensity f + ξ
hf : Measurable (Function.uncurry f)
a : α
hξ : @Measure.MutuallySingular.{u_2} γ mγ ((ξ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
this :
  (κ : (a : α) → Measure γ) a =
    HAdd.hAdd (α := Measure γ) (β := Measure γ) ((ξ : (a : α) → Measure γ) a : Measure γ)
      (Measure.withDensity ((η : (a : α) → Measure γ) a) (f a))
⊢ f a =ᶠ[ae (F := Measure γ) ((η : (a : α) → Measure γ) a : Measure γ)]
    Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)

Tactic:
exact (κ a).eq_rnDeriv₀ (hf.comp measurable_prodMk_left).aemeasurable hξ this

Premises used: Measurable.aemeasurable, Measurable.comp, MeasureTheory.Measure.eq_rnDeriv₀, measurable_prodMk_left
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η ξ : Kernel α γ
f : α → γ → ℝ≥0∞
inst : IsFiniteKernel η
h : κ = η.withDensity f + ξ
hf : Measurable (Function.uncurry f)
a : α
hξ : @Measure.MutuallySingular.{u_2} γ mγ ((ξ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
this :
  (κ : (a : α) → Measure γ) a =
    HAdd.hAdd (α := Measure γ) (β := Measure γ) ((ξ : (a : α) → Measure γ) a : Measure γ)
      (Measure.withDensity ((η : (a : α) → Measure γ) a) (f a))
⊢ Eq.{u_2 + 1} (α := Measure γ) ((ξ : (a : α) → Measure γ) a : Measure γ)
    (Measure.singularPart ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) : Measure γ)

Tactic:
(κ a).eq_singularPart (hf.comp measurable_prodMk_left) hξ this

Premises used: Measurable.comp, MeasureTheory.Measure.eq_singularPart, measurable_prodMk_left
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η ξ : Kernel α γ
f : α → γ → ℝ≥0∞
inst : IsFiniteKernel η
h : κ = η.withDensity f + ξ
hf : Measurable (Function.uncurry f)
a : α
hξ : @Measure.MutuallySingular.{u_2} γ mγ ((ξ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
this :
  (κ : (a : α) → Measure γ) a =
    HAdd.hAdd (α := Measure γ) (β := Measure γ) ((ξ : (a : α) → Measure γ) a : Measure γ)
      (Measure.withDensity ((η : (a : α) → Measure γ) a) (f a))
⊢ Eq.{u_2 + 1} (α := Measure γ) ((ξ : (a : α) → Measure γ) a : Measure γ)
    (Measure.singularPart ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) : Measure γ)

Tactic:
exact (κ a).eq_singularPart (hf.comp measurable_prodMk_left) hξ this

Premises used: Measurable.comp, MeasureTheory.Measure.eq_singularPart, measurable_prodMk_left
-- 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 : α
⊢ κ.rnDeriv η a =ᶠ[ae (F := Measure γ) ((η : (a : α) → Measure γ) a : Measure γ)]
    Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)

Tactic:
eq_rnDeriv_measure (rnDeriv_add_singularPart κ η).symm (measurable_rnDeriv κ η) a
    (mutuallySingular_singularPart κ η a)

Premises used: ProbabilityTheory.Kernel.rnDeriv_add_singularPart, ProbabilityTheory.Kernel.mutuallySingular_singularPart, ProbabilityTheory.Kernel.measurable_rnDeriv, ProbabilityTheory.Kernel.eq_rnDeriv_measure, 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 : α
⊢ Eq.{u_2 + 1} (α := Measure γ) ((κ.singularPart η : (a : α) → Measure γ) a : Measure γ)
    (Measure.singularPart ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) : Measure γ)

Tactic:
eq_singularPart_measure (rnDeriv_add_singularPart κ η).symm (measurable_rnDeriv κ η) a
    (mutuallySingular_singularPart κ η a)

Premises used: ProbabilityTheory.Kernel.rnDeriv_add_singularPart, ProbabilityTheory.Kernel.mutuallySingular_singularPart, ProbabilityTheory.Kernel.measurable_rnDeriv, ProbabilityTheory.Kernel.eq_singularPart_measure, Eq.symm
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
ξ : Kernel α γ
f : α → γ → ℝ≥0∞
inst : IsFiniteKernel η
inst_1 : IsFiniteKernel κ
h : κ = η.withDensity f + ξ
hf : Measurable (Function.uncurry f)
a : α
hξ : @Measure.MutuallySingular.{u_2} γ mγ ((ξ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
⊢ f a =ᶠ[ae (F := Measure γ) ((η : (a : α) → Measure γ) a : Measure γ)] κ.rnDeriv η a

Tactic:
(eq_rnDeriv_measure h hf a hξ).trans rnDeriv_eq_rnDeriv_measure.symm

Premises used: Filter.EventuallyEq.trans, ProbabilityTheory.Kernel.rnDeriv_eq_rnDeriv_measure, ProbabilityTheory.Kernel.eq_rnDeriv_measure, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
ξ : Kernel α γ
f : α → γ → ℝ≥0∞
inst : IsFiniteKernel η
inst_1 : IsFiniteKernel κ
h : κ = η.withDensity f + ξ
hf : Measurable (Function.uncurry f)
a : α
hξ : @Measure.MutuallySingular.{u_2} γ mγ ((ξ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
⊢ Eq.{u_2 + 1} (α := Measure γ) ((ξ : (a : α) → Measure γ) a : Measure γ)
    ((κ.singularPart η : (a : α) → Measure γ) a : Measure γ)

Tactic:
(eq_singularPart_measure h hf a hξ).trans singularPart_eq_singularPart_measure.symm

Premises used: ProbabilityTheory.Kernel.eq_singularPart_measure, ProbabilityTheory.Kernel.singularPart_eq_singularPart_measure, Eq.symm, Eq.trans
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκ : IsFiniteKernel κ
inst : IsFiniteKernel η
⊢ IsFiniteKernel (η.withDensity (κ.rnDeriv η))

Tactic:
⟨κ.bound, κ.bound_lt_top, fun a ↦ ?_⟩

Premises used: ProbabilityTheory.IsFiniteKernel.mk, ProbabilityTheory.Kernel.bound_lt_top, And.intro, Exists.intro, ProbabilityTheory.Kernel.bound
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκ : IsFiniteKernel κ
inst : IsFiniteKernel η
refine :
  ∀ (a : α), (((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ ≤ κ.bound
⊢ IsFiniteKernel (η.withDensity (κ.rnDeriv η))

Tactic:
refine ⟨κ.bound, κ.bound_lt_top, fun a ↦ ?_⟩
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκ : IsFiniteKernel κ
inst : IsFiniteKernel η
a : α
rw : ∫⁻ (x : γ), κ.rnDeriv η a x ∂(η : (a : α) → Measure γ) a ≤ κ.bound
hf : Measurable (Function.uncurry (κ.rnDeriv η))
⊢ (((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ ≤ κ.bound

Tactic:
rw [Kernel.withDensity_apply', setLIntegral_univ]

Premises used: ProbabilityTheory.Kernel.withDensity_apply', MeasureTheory.setLIntegral_univ
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκ : IsFiniteKernel κ
inst : 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 γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκ : IsFiniteKernel κ
inst : 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 α γ
hκ : IsFiniteKernel κ
inst : IsFiniteKernel η
a : α
rw :
  ∫⁻ (a_1 : γ),
      Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
        a_1 ∂(η : (a : α) → Measure γ) a ≤
    κ.bound
⊢ ∫⁻ (x : γ), κ.rnDeriv η a x ∂(η : (a : α) → Measure γ) a ≤ κ.bound

Tactic:
rw [lintegral_congr_ae rnDeriv_eq_rnDeriv_measure]

Premises used: ProbabilityTheory.Kernel.rnDeriv_eq_rnDeriv_measure, MeasureTheory.lintegral_congr_ae
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκ : IsFiniteKernel κ
inst : IsFiniteKernel η
a : α
⊢ ∫⁻ (a_1 : γ),
      Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
        a_1 ∂(η : (a : α) → Measure γ) a ≤
    κ.bound

Tactic:
Measure.lintegral_rnDeriv_le.trans (measure_le_bound _ _ _)

Premises used: MeasureTheory.Measure.lintegral_rnDeriv_le, ProbabilityTheory.Kernel.measure_le_bound, LE.le.trans
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκ : IsFiniteKernel κ
inst : IsFiniteKernel η
a : α
⊢ ∫⁻ (a_1 : γ),
      Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
        a_1 ∂(η : (a : α) → Measure γ) a ≤
    κ.bound

Tactic:
exact Measure.lintegral_rnDeriv_le.trans (measure_le_bound _ _ _)

Premises used: MeasureTheory.Measure.lintegral_rnDeriv_le, ProbabilityTheory.Kernel.measure_le_bound, LE.le.trans
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκ : IsFiniteKernel κ
inst : IsFiniteKernel η
⊢ IsFiniteKernel (κ.singularPart η)

Tactic:
⟨κ.bound, κ.bound_lt_top, fun a ↦ ?_⟩

Premises used: ProbabilityTheory.IsFiniteKernel.mk, ProbabilityTheory.Kernel.bound_lt_top, And.intro, Exists.intro, ProbabilityTheory.Kernel.bound
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκ : IsFiniteKernel κ
inst : IsFiniteKernel η
refine : ∀ (a : α), (((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ ≤ κ.bound
⊢ IsFiniteKernel (κ.singularPart η)

Tactic:
refine ⟨κ.bound, κ.bound_lt_top, fun a ↦ ?_⟩
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκ : IsFiniteKernel κ
inst : IsFiniteKernel η
a : α
rw :
  ((((η.withDensity (κ.rnDeriv η) + κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ :
    ℝ≥0∞)
| ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
rw [← rnDeriv_add_singularPart κ η]

Premises used: ProbabilityTheory.Kernel.rnDeriv_add_singularPart
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκ : IsFiniteKernel κ
inst : IsFiniteKernel η
a : α
conv_rhs :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ : ℝ≥0∞) =
    (((η.withDensity (κ.rnDeriv η) + κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ : ℝ≥0∞) =
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ

Tactic:
conv_rhs => rw [← rnDeriv_add_singularPart κ η]

Premises used: ProbabilityTheory.Kernel.rnDeriv_add_singularPart
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκ : IsFiniteKernel κ
inst : IsFiniteKernel η
a : α
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ : ℝ≥0∞) =
    (((η.withDensity (κ.rnDeriv η) + κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκ : IsFiniteKernel κ
inst : IsFiniteKernel η
a : α
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ : ℝ≥0∞) =
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ

Tactic:
have h : withDensity η (rnDeriv κ η) a univ + singularPart κ η a univ = κ a univ := by
    conv_rhs => rw [← rnDeriv_add_singularPart κ η]
    simp
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκ : IsFiniteKernel κ
inst : IsFiniteKernel η
a : α
h :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ : ℝ≥0∞) =
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ
⊢ (((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ ≤ κ.bound

Tactic:
(self_le_add_left _ _).trans (h.le.trans (measure_le_bound _ _ _))

Premises used: self_le_add_left, Eq.le, ProbabilityTheory.Kernel.measure_le_bound, LE.le.trans
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκ : IsFiniteKernel κ
inst : IsFiniteKernel η
a : α
h :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ : ℝ≥0∞) =
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ
⊢ (((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ ≤ κ.bound

Tactic:
exact (self_le_add_left _ _).trans (h.le.trans (measure_le_bound _ _ _))

Premises used: self_le_add_left, Eq.le, ProbabilityTheory.Kernel.measure_le_bound, LE.le.trans
-- 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 η
⊢ Measurable.{u_1, u_2} (β := Measure γ) fun (a : α) ↦
    Measure.singularPart ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)

Tactic:
Measure.measurable_of_measurable_coe _ (fun s hs ↦ ?_)

Premises used: MeasureTheory.Measure.measurable_of_measurable_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 η
refine :
  ∀ (s : Set γ) (hs : MeasurableSet s),
    Measurable (β := ℝ≥0∞) fun (b : α) ↦
      ((Measure.singularPart ((κ : (a : α) → Measure γ) b) ((η : (a : α) → Measure γ) b) : Measure γ) :
          (a : Set γ) → ℝ≥0∞)
        s
⊢ Measurable.{u_1, u_2} (β := Measure γ) fun (a : α) ↦
    Measure.singularPart ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)

Tactic:
refine Measure.measurable_of_measurable_coe _ (fun s hs ↦ ?_)

Premises used: MeasureTheory.Measure.measurable_of_measurable_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 η
s : Set γ
hs : MeasurableSet s
simp_rw :
  Measurable (β := ℝ≥0∞) fun (b : α) ↦
    ((((κ + η).withDensity fun (a : α) (x : γ) ↦
                (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) -
                  (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) * κ.rnDeriv η a x :
              (a : α) → Measure γ)
            b :
          Measure γ) :
        (a : Set γ) → ℝ≥0∞)
      s
⊢ Measurable (β := ℝ≥0∞) fun (b : α) ↦
    ((Measure.singularPart ((κ : (a : α) → Measure γ) b) ((η : (a : α) → Measure γ) b) : Measure γ) :
        (a : Set γ) → ℝ≥0∞)
      s

Tactic:
simp_rw [← κ.singularPart_eq_singularPart_measure, κ.singularPart_def η]

Premises used: ProbabilityTheory.Kernel.singularPart_eq_singularPart_measure, ProbabilityTheory.Kernel.singularPart_def
-- 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 η
s : Set γ
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : α) ↦
    ((((κ + η).withDensity fun (a : α) (x : γ) ↦
                (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) -
                  (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) * κ.rnDeriv η a x :
              (a : α) → Measure γ)
            b :
          Measure γ) :
        (a : Set γ) → ℝ≥0∞)
      s

Tactic:
Kernel.measurable_coe _ hs

Premises used: ProbabilityTheory.Kernel.measurable_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 η
s : Set γ
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : α) ↦
    ((((κ + η).withDensity fun (a : α) (x : γ) ↦
                (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) -
                  (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) * κ.rnDeriv η a x :
              (a : α) → Measure γ)
            b :
          Measure γ) :
        (a : Set γ) → ℝ≥0∞)
      s

Tactic:
exact Kernel.measurable_coe _ hs

Premises used: ProbabilityTheory.Kernel.measurable_coe
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ : Kernel α γ
inst : IsFiniteKernel κ
a : α
⊢ κ.rnDeriv κ a =ᶠ[ae (F := Measure γ) ((κ : (a : α) → Measure γ) a : Measure γ)] 1

Tactic:
(κ.rnDeriv_eq_rnDeriv_measure).trans (κ a).rnDeriv_self

Premises used: Filter.EventuallyEq.trans, ProbabilityTheory.Kernel.rnDeriv_eq_rnDeriv_measure, MeasureTheory.Measure.rnDeriv_self, 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 : α
h :
  ∀ (x : γ)
    (h1 :
      (κ.singularPart ν).rnDeriv ν a x =
        Measure.rnDeriv (m := mγ) ((κ.singularPart ν : (a : α) → Measure γ) a) ((ν : (a : α) → Measure γ) a) x)
    (h2 : Measure.rnDeriv (m := mγ) ((κ.singularPart ν : (a : α) → Measure γ) a) ((ν : (a : α) → Measure γ) a) x = 0 x),
    (κ.singularPart ν).rnDeriv ν a x = 0 x
⊢ (κ.singularPart ν).rnDeriv ν a =ᶠ[ae (F := Measure γ) ((ν : (a : α) → Measure γ) a : Measure γ)] 0

Tactic:
filter_upwards [(singularPart κ ν).rnDeriv_eq_rnDeriv_measure,
    (Measure.rnDeriv_eq_zero _ _).mpr (mutuallySingular_singularPart κ ν a)] with x h1 h2

Premises used: Iff.mpr, ProbabilityTheory.Kernel.mutuallySingular_singularPart, ProbabilityTheory.Kernel.rnDeriv_eq_rnDeriv_measure, MeasureTheory.Measure.rnDeriv_eq_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 : α
x : γ
h1 :
  (κ.singularPart ν).rnDeriv ν a x =
    Measure.rnDeriv (m := mγ) ((κ.singularPart ν : (a : α) → Measure γ) a) ((ν : (a : α) → Measure γ) a) x
h2 h : Measure.rnDeriv (m := mγ) ((κ.singularPart ν : (a : α) → Measure γ) a) ((ν : (a : α) → Measure γ) a) x = 0 x
h₁ h₂ : Eq (α := ℝ≥0∞) (0 x) (0 x)
⊢ (κ.singularPart ν).rnDeriv ν a x = 0 x

Tactic:
rw [h1, h2]
-- 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 : α
x : γ
heq : κ.rnDeriv η a x = Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x
htop : Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x ≠ ∞
⊢ κ.rnDeriv η a x < ∞

Tactic:
heq ▸ htop.lt_top

Premises used: Eq.rec, Ne.lt_top, Eq.symm
-- 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 : α
h :
  ∀ (a_1 : γ),
    Membership.mem (γ := Set γ)
      {x : γ |
        Membership.mem (γ := Set γ)
            {x : γ |
              (fun (x : γ) ↦
                  κ.rnDeriv η a x =
                    Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x)
                x}
            x →
          Membership.mem (γ := Set γ)
            {x : γ |
              Membership.mem (γ := Set γ)
                  {x : γ |
                    (fun (x : γ) ↦
                        Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x ≠ ∞)
                      x}
                  x →
                Membership.mem (γ := Set γ) {x : γ | (fun (x : γ) ↦ κ.rnDeriv η a x < ∞) x} x}
            x}
      a_1
h₁ h₂ :
  ∀ (x : γ)
    (heq : κ.rnDeriv η a x = Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x)
    (htop : Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x ≠ ∞),
    κ.rnDeriv η a x < ∞
⊢ ∀ᵐ (x : γ) ∂((η : (a : α) → Measure γ) a : Measure γ), κ.rnDeriv η a x < ∞

Tactic:
filter_upwards [κ.rnDeriv_eq_rnDeriv_measure, (κ a).rnDeriv_ne_top _]
    with x heq htop using heq ▸ htop.lt_top

Premises used: ProbabilityTheory.Kernel.rnDeriv_eq_rnDeriv_measure, MeasureTheory.Measure.rnDeriv_ne_top, 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_1 : α
a : γ
h : κ.rnDeriv η a_1 a < ∞
⊢ κ.rnDeriv η a_1 a ≠ ∞

Tactic:
h.ne

Premises used: LT.lt.ne