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 : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
h :
  ∀ (a_1 : γ),
    Membership.mem (γ := Set γ)
      {x : γ |
        Membership.mem (γ := Set γ) {x : γ | (fun (x : γ) ↦ κ.rnDeriv η a x < ∞) x} x →
          Membership.mem (γ := Set γ) {x : γ | (fun (x : γ) ↦ κ.rnDeriv η a x ≠ ∞) x} x}
      a_1
h₁ h₂ : ∀ (a_1 : γ) (h : κ.rnDeriv η a a_1 < ∞), κ.rnDeriv η a a_1 ≠ ∞
⊢ ∀ᵐ (x : γ) ∂((η : (a : α) → Measure γ) a : Measure γ), κ.rnDeriv η a x ≠ ∞

Tactic:
filter_upwards [κ.rnDeriv_lt_top η] with a h using h.ne

Premises used: ProbabilityTheory.Kernel.rnDeriv_lt_top
-- 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 : α
ha : Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
x : γ
heq : κ.rnDeriv η a x = Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x
hpos : 0 < Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x
⊢ 0 < κ.rnDeriv η a x

Tactic:
heq ▸ hpos

Premises used: Eq.rec, 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 : α
ha : Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) 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 : γ) ↦
                        0 < Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x)
                      x}
                  x →
                Membership.mem (γ := Set γ) {x : γ | (fun (x : γ) ↦ 0 < κ.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)
    (hpos : 0 < Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x),
    0 < κ.rnDeriv η a x
⊢ ∀ᵐ (x : γ) ∂((κ : (a : α) → Measure γ) a : Measure γ), 0 < κ.rnDeriv η a x

Tactic:
filter_upwards [ha.ae_le κ.rnDeriv_eq_rnDeriv_measure, Measure.rnDeriv_pos ha]
    with x heq hpos using heq ▸ hpos

Premises used: ProbabilityTheory.Kernel.rnDeriv_eq_rnDeriv_measure, MeasureTheory.Measure.rnDeriv_pos, MeasureTheory.Measure.AbsolutelyContinuous.ae_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 : α
h : Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
h₁ : ∀ (x : γ) (h0 : 0 < κ.rnDeriv η a x) (htop : κ.rnDeriv η a x ≠ ∞), 0 < (κ.rnDeriv η a x).toReal
⊢ ∀ᵐ (x : γ) ∂((κ : (a : α) → Measure γ) a : Measure γ), 0 < (κ.rnDeriv η a x).toReal

Tactic:
filter_upwards [rnDeriv_pos h, h.ae_le (rnDeriv_ne_top κ _)] with x h0 htop

Premises used: ProbabilityTheory.Kernel.rnDeriv_ne_top, ProbabilityTheory.Kernel.rnDeriv_pos, MeasureTheory.Measure.AbsolutelyContinuous.ae_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 : α
h : Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
x : γ
h0 : 0 < κ.rnDeriv η a x
htop : κ.rnDeriv η a x ≠ ∞
⊢ 0 < (κ.rnDeriv η a x).toReal

Tactic:
simp_all only [pos_iff_ne_zero, ne_eq, ENNReal.toReal_pos, not_false_eq_true]

Premises used: ne_eq, ENNReal.toReal_pos, not_false_eq_true, pos_iff_ne_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 ν
inst_2 : IsFiniteKernel η
a : α
h :
  ∀ (x : γ)
    (h1 :
      (κ + ν).rnDeriv η a x =
        Measure.rnDeriv (m := mγ) ((κ + ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x)
    (h2 : κ.rnDeriv η a x = Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x)
    (h3 : ν.rnDeriv η a x = Measure.rnDeriv (m := mγ) ((ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x)
    (h4 :
      (∂HAdd.hAdd (α := Measure γ) (β := Measure γ) ((κ : (a : α) → Measure γ) a : Measure γ)
              ((ν : (a : α) → Measure γ) a : Measure γ)/∂(η : (a : α) → Measure γ) a)
          x =
        HAdd.hAdd (α := γ → ℝ≥0∞) (β := γ → ℝ≥0∞)
          (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a))
          (Measure.rnDeriv (m := mγ) ((ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)) x),
    (κ + ν).rnDeriv η a x = (κ.rnDeriv η a + ν.rnDeriv η a) x
⊢ (κ + ν).rnDeriv η a =ᶠ[ae (F := Measure γ) ((η : (a : α) → Measure γ) a : Measure γ)] κ.rnDeriv η a + ν.rnDeriv η a

Tactic:
filter_upwards [(κ + ν).rnDeriv_eq_rnDeriv_measure, κ.rnDeriv_eq_rnDeriv_measure,
    ν.rnDeriv_eq_rnDeriv_measure, (κ a).rnDeriv_add (ν a) (η a)] with x h1 h2 h3 h4

Premises used: ProbabilityTheory.Kernel.rnDeriv_eq_rnDeriv_measure, MeasureTheory.Measure.rnDeriv_add, 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 : α
s : Set γ
hs : MeasurableSet s
rw :
  LE.le (α := ℝ≥0∞)
    (((Measure.withDensity ((η : (a : α) → Measure γ) a)
              (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)) :
            Measure γ) :
          (a : Set γ) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ∫⁻ (c : γ) in s, κ.rnDeriv η a c ∂(η : (a : α) → Measure γ) a ≤
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s

Tactic:
rw [setLIntegral_congr_fun_ae hs ((κ.rnDeriv_eq_rnDeriv_measure).mono (fun x hx _ ↦ hx)),
    ← withDensity_apply' _ s]

Premises used: ProbabilityTheory.Kernel.rnDeriv_eq_rnDeriv_measure, MeasureTheory.setLIntegral_congr_fun_ae, Filter.Eventually.mono, MeasureTheory.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 : α
s : Set γ
hs : MeasurableSet s
⊢ LE.le (α := ℝ≥0∞)
    (((Measure.withDensity ((η : (a : α) → Measure γ) a)
              (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)) :
            Measure γ) :
          (a : Set γ) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
(κ a).withDensity_rnDeriv_le _ _

Premises used: MeasureTheory.Measure.withDensity_rnDeriv_le, 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 : α
s : Set γ
hs : MeasurableSet s
⊢ LE.le (α := ℝ≥0∞)
    (((Measure.withDensity ((η : (a : α) → Measure γ) a)
              (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)) :
            Measure γ) :
          (a : Set γ) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
exact (κ a).withDensity_rnDeriv_le _ _

Premises used: MeasureTheory.Measure.withDensity_rnDeriv_le, 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 : Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
s : Set γ
hs : MeasurableSet s
rw :
  ∫⁻ (x : γ) in s,
      Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
        x ∂(η : (a : α) → Measure γ) a =
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s
rw₁ :
  Eq (α := ℝ≥0∞)
    (((Measure.withDensity ((η : (a : α) → Measure γ) a)
              (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)) :
            Measure γ) :
          (a : Set γ) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
rw₂ rw₃ :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ∫⁻ (c : γ) in s, κ.rnDeriv η a c ∂(η : (a : α) → Measure γ) a =
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s

Tactic:
rw [setLIntegral_congr_fun_ae hs ((κ.rnDeriv_eq_rnDeriv_measure).mono (fun x hx _ ↦ hx)),
    ← withDensity_apply _ hs, (κ a).withDensity_rnDeriv_eq _ h]

Premises used: ProbabilityTheory.Kernel.rnDeriv_eq_rnDeriv_measure, MeasureTheory.setLIntegral_congr_fun_ae, Filter.Eventually.mono, DFunLike.coe, MeasureTheory.withDensity_apply, MeasureTheory.Measure.withDensity_rnDeriv_eq
-- 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 : Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
rw :
  ∫⁻ (x : γ) in univ, κ.rnDeriv η a x ∂(η : (a : α) → Measure γ) a =
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ
rw₁ rw₂ :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ : ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ ∫⁻ (c : γ), κ.rnDeriv η a c ∂(η : (a : α) → Measure γ) a =
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ

Tactic:
rw [← setLIntegral_univ, setLIntegral_rnDeriv h MeasurableSet.univ]

Premises used: ProbabilityTheory.Kernel.setLIntegral_rnDeriv, MeasurableSet.univ, MeasureTheory.setLIntegral_univ
-- 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 : α
⊢ LE.le.{u_2} (α := Measure γ) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ)
    ((κ : (a : α) → Measure γ) a : Measure γ)

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

Premises used: MeasureTheory.Measure.le_intro
-- 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 : α
refine :
  ∀ (s : Set γ) (hs : MeasurableSet s),
    s.Nonempty →
      LE.le (α := ℝ≥0∞)
        ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
        ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ LE.le.{u_2} (α := Measure γ) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ)
    ((κ : (a : α) → Measure γ) a : Measure γ)

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

Premises used: MeasureTheory.Measure.le_intro
-- 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 : α
s : Set γ
hs : MeasurableSet s
h : s.Nonempty
rw :
  ∫⁻ (b : γ) in s, κ.rnDeriv η a b ∂(η : (a : α) → Measure γ) a ≤
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s
hf : Measurable (Function.uncurry (κ.rnDeriv η))
⊢ LE.le (α := ℝ≥0∞)
    ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥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 : α
s : Set γ
hs : MeasurableSet s
h : s.Nonempty
⊢ ∫⁻ (b : γ) in s, κ.rnDeriv η a b ∂(η : (a : α) → Measure γ) a ≤
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s

Tactic:
setLIntegral_rnDeriv_le hs

Premises used: ProbabilityTheory.Kernel.setLIntegral_rnDeriv_le
-- 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 : α
s : Set γ
hs : MeasurableSet s
h : s.Nonempty
⊢ ∫⁻ (b : γ) in s, κ.rnDeriv η a b ∂(η : (a : α) → Measure γ) a ≤
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s

Tactic:
exact setLIntegral_rnDeriv_le hs

Premises used: ProbabilityTheory.Kernel.setLIntegral_rnDeriv_le
-- 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 : α
s : Set γ
hs : MeasurableSet s
h : s.Nonempty
⊢ 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 : α
s : Set γ
hs : MeasurableSet s
h : s.Nonempty
⊢ 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 : α
h : Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
rw :
  Eq (α := Measure γ) (Measure.withDensity ((η : (a : α) → Measure γ) a) (κ.rnDeriv η a)) ((κ : (a : α) → Measure γ) a)
hf : Measurable (Function.uncurry (κ.rnDeriv η))
⊢ Eq.{u_2 + 1} (α := Measure γ) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ)
    ((κ : (a : α) → Measure γ) a : Measure γ)

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 γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
h : Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) 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 α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
h : Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) 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 : α
h : Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
⊢ κ.rnDeriv η a =ᶠ[ae (F := Measure γ) ((η : (a : α) → Measure γ) a : Measure γ)]
    Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)

Tactic:
have h_ae := κ.rnDeriv_eq_rnDeriv_measure (η := η) (a := a)
-- 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 : α
h : Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
h_ae :
  κ.rnDeriv η a =ᶠ[ae (F := Measure γ) ((η : (a : α) → Measure γ) a : Measure γ)]
    Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
rw :
  Eq.{u_2 + 1} (α := Measure γ)
    (Measure.withDensity ((η : (a : α) → Measure γ) a)
      (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)))
    ((κ : (a : α) → Measure γ) a)
rw₁ rw₂ :
  Eq.{u_2 + 1} (α := Measure γ) ((κ : (a : α) → Measure γ) a : Measure γ) ((κ : (a : α) → Measure γ) a : Measure γ)
⊢ Eq (α := Measure γ) (Measure.withDensity ((η : (a : α) → Measure γ) a) (κ.rnDeriv η a)) ((κ : (a : α) → Measure γ) a)

Tactic:
rw [MeasureTheory.withDensity_congr_ae h_ae, (κ a).withDensity_rnDeriv_eq _ h]

Premises used: MeasureTheory.withDensity_congr_ae, DFunLike.coe, MeasureTheory.Measure.withDensity_rnDeriv_eq
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
f : α → γ → ℝ≥0∞
inst_1 : IsFiniteKernel (κ.withDensity f)
hf : Measurable (Function.uncurry f)
a : α
⊢ (κ.withDensity f).rnDeriv κ a =ᶠ[ae (F := Measure γ) ((κ : (a : α) → Measure γ) a : Measure γ)]
    Measure.rnDeriv (m := mγ) ((κ.withDensity f : (a : α) → Measure γ) a) ((κ : (a : α) → Measure γ) a)

Tactic:
have h_ae := (κ.withDensity f).rnDeriv_eq_rnDeriv_measure (η := κ) (a := a)
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
f : α → γ → ℝ≥0∞
inst_1 : IsFiniteKernel (κ.withDensity f)
hf : Measurable (Function.uncurry f)
a : α
h_ae :
  (κ.withDensity f).rnDeriv κ a =ᶠ[ae (F := Measure γ) ((κ : (a : α) → Measure γ) a : Measure γ)]
    Measure.rnDeriv (m := mγ) ((κ.withDensity f : (a : α) → Measure γ) a) ((κ : (a : α) → Measure γ) a)
⊢ ∀ (a : α), Measurable (f a)

Tactic:
have hf' : ∀ a, Measurable (f a) := fun _ ↦ hf.of_uncurry_left
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
f : α → γ → ℝ≥0∞
inst_1 : IsFiniteKernel (κ.withDensity f)
hf : Measurable (Function.uncurry f)
a : α
h_ae :
  (κ.withDensity f).rnDeriv κ a =ᶠ[ae (F := Measure γ) ((κ : (a : α) → Measure γ) a : Measure γ)]
    Measure.rnDeriv (m := mγ) ((κ.withDensity f : (a : α) → Measure γ) a) ((κ : (a : α) → Measure γ) a)
hf' : ∀ (a : α), Measurable (f a)
h :
  ∀ (x : γ)
    (hx1 :
      (κ.withDensity f).rnDeriv κ a x =
        Measure.rnDeriv (m := mγ) ((κ.withDensity f : (a : α) → Measure γ) a) ((κ : (a : α) → Measure γ) a) x)
    (hx2 :
      Measure.rnDeriv (m := mγ) (Measure.withDensity ((κ : (a : α) → Measure γ) a) (f a)) ((κ : (a : α) → Measure γ) a)
          x =
        f a x),
    (κ.withDensity f).rnDeriv κ a x = f a x
⊢ (κ.withDensity f).rnDeriv κ a =ᶠ[ae (F := Measure γ) ((κ : (a : α) → Measure γ) a : Measure γ)] f a

Tactic:
filter_upwards [h_ae, (κ a).rnDeriv_withDensity (hf' a)] with x hx1 hx2

Premises used: MeasureTheory.Measure.rnDeriv_withDensity, DFunLike.coe
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
f : α → γ → ℝ≥0∞
inst_1 : IsFiniteKernel (κ.withDensity f)
hf : Measurable (Function.uncurry f)
a : α
h_ae :
  (κ.withDensity f).rnDeriv κ a =ᶠ[ae (F := Measure γ) ((κ : (a : α) → Measure γ) a : Measure γ)]
    Measure.rnDeriv (m := mγ) ((κ.withDensity f : (a : α) → Measure γ) a) ((κ : (a : α) → Measure γ) a)
hf' : ∀ (a : α), Measurable (f a)
x : γ
hx1 :
  (κ.withDensity f).rnDeriv κ a x =
    Measure.rnDeriv (m := mγ) ((κ.withDensity f : (a : α) → Measure γ) a) ((κ : (a : α) → Measure γ) a) x
hx2 :
  Measure.rnDeriv (m := mγ) (Measure.withDensity ((κ : (a : α) → Measure γ) a) (f a)) ((κ : (a : α) → Measure γ) a) x =
    f a x
h : Measure.rnDeriv (m := mγ) ((κ.withDensity f : (a : α) → Measure γ) a) ((κ : (a : α) → Measure γ) a) x = f a x
h₁ :
  Measure.rnDeriv (m := mγ) (Measure.withDensity ((κ : (a : α) → Measure γ) a) (f a)) ((κ : (a : α) → Measure γ) a) x =
    f a x
h₂ h₃ : f a x = f a x
⊢ (κ.withDensity f).rnDeriv κ a x = f a x

Tactic:
rw [hx1, κ.withDensity_apply hf, hx2]

Premises used: 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 : α
h_ac :
  Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
rw :
  (∀ᵐ (b : γ) ∂((η : (a : α) → Measure γ) a : Measure γ), κ.rnDeriv η a b = 1) ↔
    Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a)
        ((η : (a : α) → Measure γ) a) =ᶠ[ae (F := Measure γ) ((η : (a : α) → Measure γ) a : Measure γ)]
      1
⊢ (∀ᵐ (b : γ) ∂((η : (a : α) → Measure γ) a : Measure γ), κ.rnDeriv η a b = 1) ↔
    Eq.{u_2 + 1} (α := Measure γ) ((κ : (a : α) → Measure γ) a : Measure γ) ((η : (a : α) → Measure γ) a : Measure γ)

Tactic:
rw [← Measure.rnDeriv_eq_one_iff_eq h_ac]

Premises used: MeasureTheory.Measure.rnDeriv_eq_one_iff_eq