awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκη : κ ≤ η
a : α
x : γ
pos :
  ∀ (hα : Countable α),
    0 ≤ (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x).toReal
neg :
  ∀ (hα : ¬Countable α),
    0 ≤ density (β := Unit) (mβ := PUnit.instMeasurableSpace) (κ.map fun (a : γ) ↦ (a, ())) η a x univ
⊢ LE.le (α := ℝ) 0
    (if hα : Countable α then
      (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x).toReal
    else density (β := Unit) (mβ := PUnit.instMeasurableSpace) (κ.map fun (a : γ) ↦ (a, ())) η a x univ)

Tactic:
split_ifs with hα
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκη : κ ≤ η
a : α
x : γ
hα : Countable α
⊢ 0 ≤ (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x).toReal

Tactic:
ENNReal.toReal_nonneg

Premises used: ENNReal.toReal_nonneg
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκη : κ ≤ η
a : α
x : γ
hα : Countable α
⊢ 0 ≤ (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x).toReal

Tactic:
exact ENNReal.toReal_nonneg

Premises used: ENNReal.toReal_nonneg
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκη : κ ≤ η
a : α
x : γ
hα : ¬Countable α
⊢ MeasurableSpace.CountablyGenerated γ

Tactic:
have := hαγ.countableOrCountablyGenerated.resolve_left hα
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκη : κ ≤ η
a : α
x : γ
hα : ¬Countable α
this : MeasurableSpace.CountablyGenerated γ
⊢ 0 ≤ density (β := Unit) (mβ := PUnit.instMeasurableSpace) (κ.map fun (a : γ) ↦ (a, ())) η a x univ

Tactic:
density_nonneg ((fst_map_id_prod _ measurable_const).trans_le hκη) _ _ _

Premises used: Eq.trans_le, ProbabilityTheory.Kernel.fst_map_id_prod, measurable_const, ProbabilityTheory.Kernel.density_nonneg
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκη : κ ≤ η
a : α
x : γ
hα : ¬Countable α
this : MeasurableSpace.CountablyGenerated γ
⊢ 0 ≤ density (β := Unit) (mβ := PUnit.instMeasurableSpace) (κ.map fun (a : γ) ↦ (a, ())) η a x univ

Tactic:
exact density_nonneg ((fst_map_id_prod _ measurable_const).trans_le hκη) _ _ _

Premises used: Eq.trans_le, ProbabilityTheory.Kernel.fst_map_id_prod, measurable_const, ProbabilityTheory.Kernel.density_nonneg
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel η
hκη : κ ≤ η
a : α
h :
  ∀ (x : γ) (hx_le_one : Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x ≤ 1 x),
    κ.rnDerivAux η a x ≤ 1 x
⊢ κ.rnDerivAux η a ≤ᶠ[ae (F := Measure γ) ((η : (a : α) → Measure γ) a : Measure γ)] 1

Tactic:
filter_upwards [Measure.rnDeriv_le_one_of_le (hκη a)] with x hx_le_one

Premises used: MeasureTheory.Measure.rnDeriv_le_one_of_le
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel η
hκη : κ ≤ η
a : α
x : γ
hx_le_one : Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x ≤ 1 x
pos :
  ∀ (hα : Countable α),
    (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x).toReal ≤ 1 x
neg :
  ∀ (hα : ¬Countable α),
    density (β := Unit) (mβ := PUnit.instMeasurableSpace) (κ.map fun (a : γ) ↦ (a, ())) η a x univ ≤ 1 x
⊢ LE.le (α := ℝ)
    (if hα : Countable α then
      (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x).toReal
    else density (β := Unit) (mβ := PUnit.instMeasurableSpace) (κ.map fun (a : γ) ↦ (a, ())) η a x univ)
    (1 x)

Tactic:
split_ifs with hα
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel η
hκη : κ ≤ η
a : α
x : γ
hx_le_one : Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x ≤ 1 x
hα : Countable α
⊢ (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x).toReal ≤ 1 x

Tactic:
ENNReal.toReal_le_of_le_ofReal zero_le_one ?_

Premises used: zero_le_one, ENNReal.toReal_le_of_le_ofReal
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel η
hκη : κ ≤ η
a : α
x : γ
hx_le_one : Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x ≤ 1 x
hα : Countable α
pos : Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x ≤ ENNReal.ofReal (1 x)
⊢ (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x).toReal ≤ 1 x

Tactic:
refine ENNReal.toReal_le_of_le_ofReal zero_le_one ?_

Premises used: zero_le_one, ENNReal.toReal_le_of_le_ofReal
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel η
hκη : κ ≤ η
a : α
x : γ
hx_le_one : Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x ≤ 1 x
hα : Countable α
pos : Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x ≤ 1
⊢ Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x ≤ ENNReal.ofReal (1 x)

Tactic:
simp only [Pi.one_apply, ENNReal.ofReal_one]

Premises used: Pi.one_apply, ENNReal.ofReal_one
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel η
hκη : κ ≤ η
a : α
x : γ
hx_le_one : Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x ≤ 1 x
hα : Countable α
⊢ Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x ≤ 1

Tactic:
hx_le_one
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel η
hκη : κ ≤ η
a : α
x : γ
hx_le_one : Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x ≤ 1 x
hα : Countable α
⊢ Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x ≤ 1

Tactic:
exact hx_le_one
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel η
hκη : κ ≤ η
a : α
x : γ
hx_le_one : Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x ≤ 1 x
hα : ¬Countable α
⊢ MeasurableSpace.CountablyGenerated γ

Tactic:
have := hαγ.countableOrCountablyGenerated.resolve_left hα
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel η
hκη : κ ≤ η
a : α
x : γ
hx_le_one : Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x ≤ 1 x
hα : ¬Countable α
this : MeasurableSpace.CountablyGenerated γ
⊢ density (β := Unit) (mβ := PUnit.instMeasurableSpace) (κ.map fun (a : γ) ↦ (a, ())) η a x univ ≤ 1 x

Tactic:
density_le_one ((fst_map_id_prod _ measurable_const).trans_le hκη) _ _ _

Premises used: ProbabilityTheory.Kernel.density_le_one, Eq.trans_le, ProbabilityTheory.Kernel.fst_map_id_prod, measurable_const
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel η
hκη : κ ≤ η
a : α
x : γ
hx_le_one : Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x ≤ 1 x
hα : ¬Countable α
this : MeasurableSpace.CountablyGenerated γ
⊢ density (β := Unit) (mβ := PUnit.instMeasurableSpace) (κ.map fun (a : γ) ↦ (a, ())) η a x univ ≤ 1 x

Tactic:
exact density_le_one ((fst_map_id_prod _ measurable_const).trans_le hκη) _ _ _

Premises used: ProbabilityTheory.Kernel.density_le_one, Eq.trans_le, ProbabilityTheory.Kernel.fst_map_id_prod, measurable_const
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
pos :
  ∀ (hα : Countable α),
    Measurable (β := ℝ) fun (p : α × γ) ↦
      (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) p.1) ((η : (a : α) → Measure γ) p.1) p.2).toReal
neg :
  ∀ (hα : ¬Countable α),
    Measurable (β := ℝ) fun (p : α × γ) ↦
      density (β := Unit) (mβ := PUnit.instMeasurableSpace) (κ.map fun (a : γ) ↦ (a, ())) η p.1 p.2 univ
⊢ Measurable (β := ℝ) fun (p : α × γ) ↦
    if hα : Countable α then
      (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) p.1) ((η : (a : α) → Measure γ) p.1) p.2).toReal
    else density (β := Unit) (mβ := PUnit.instMeasurableSpace) (κ.map fun (a : γ) ↦ (a, ())) η p.1 p.2 univ

Tactic:
split_ifs with hα
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
hα : Countable α
⊢ Measurable (β := ℝ) fun (p : α × γ) ↦
    (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) p.1) ((η : (a : α) → Measure γ) p.1) p.2).toReal

Tactic:
Measurable.ennreal_toReal <| measurable_from_prod_countable_right'
      (fun a ↦ Measure.measurable_rnDeriv (κ a) (η a)) fun a a' c ha'_mem_a ↦ ?_

Premises used: measurable_from_prod_countable_right', Measurable.ennreal_toReal, MeasureTheory.Measure.measurable_rnDeriv, DFunLike.coe
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
hα : Countable α
pos :
  ∀ (a a' : α) (c : γ) (ha'_mem_a : a' ∈ measurableAtom a),
    Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) (a', c).1) ((η : (a : α) → Measure γ) (a', c).1) (a', c).2 =
      Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) (a, c).1) ((η : (a : α) → Measure γ) (a, c).1) (a, c).2
⊢ Measurable (β := ℝ) fun (p : α × γ) ↦
    (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) p.1) ((η : (a : α) → Measure γ) p.1) p.2).toReal

Tactic:
refine Measurable.ennreal_toReal <| measurable_from_prod_countable_right'
      (fun a ↦ Measure.measurable_rnDeriv (κ a) (η a)) fun a a' c ha'_mem_a ↦ ?_

Premises used: measurable_from_prod_countable_right', Measurable.ennreal_toReal
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ_1 η : Kernel α γ
hα : Countable α
a a' : α
c : γ
ha'_mem_a : a' ∈ measurableAtom a
κ : Kernel α γ
h :
  ∀ (s : Set γ) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure γ) a' : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
      ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq.{u_2 + 1} (α := Measure γ) ((κ : (a : α) → Measure γ) a' : Measure γ) ((κ : (a : α) → Measure γ) a : Measure γ)

Tactic:
ext s hs
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ_1 η : Kernel α γ
hα : Countable α
a a' : α
c : γ
ha'_mem_a : a' ∈ measurableAtom a
κ : Kernel α γ
s : Set γ
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure γ) a' : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
mem_of_mem_measurableAtom ha'_mem_a
        (Kernel.measurable_coe κ hs (measurableSet_singleton (κ a s))) rfl

Premises used: MeasurableSingletonClass.measurableSet_singleton, Set.Mem, setOf, Set.preimage, Set.singleton, ProbabilityTheory.Kernel.measurable_coe, mem_of_mem_measurableAtom, DFunLike.coe, rfl
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ_1 η : Kernel α γ
hα : Countable α
a a' : α
c : γ
ha'_mem_a : a' ∈ measurableAtom a
κ : Kernel α γ
s : Set γ
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure γ) a' : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
exact mem_of_mem_measurableAtom ha'_mem_a
        (Kernel.measurable_coe κ hs (measurableSet_singleton (κ a s))) rfl

Premises used: MeasurableSingletonClass.measurableSet_singleton, ProbabilityTheory.Kernel.measurable_coe, mem_of_mem_measurableAtom, DFunLike.coe, rfl
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
hα : Countable α
a a' : α
c : γ
ha'_mem_a : a' ∈ measurableAtom a
⊢ ∀ (κ : Kernel α γ),
    Eq.{u_2 + 1} (α := Measure γ) ((κ : (a : α) → Measure γ) a' : Measure γ) ((κ : (a : α) → Measure γ) a : Measure γ)

Tactic:
have h_eq : ∀ κ : Kernel α γ, κ a' = κ a := fun κ ↦ by
      ext s hs
      exact mem_of_mem_measurableAtom ha'_mem_a
        (Kernel.measurable_coe κ hs (measurableSet_singleton (κ a s))) rfl
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
hα : Countable α
a a' : α
c : γ
ha'_mem_a : a' ∈ measurableAtom a
h_eq :
  ∀ (κ : Kernel α γ),
    Eq.{u_2 + 1} (α := Measure γ) ((κ : (a : α) → Measure γ) a' : Measure γ) ((κ : (a : α) → Measure γ) a : Measure γ)
pos :
  Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) (a', c).1) (a', c).2 =
    Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) (a, c).1) ((η : (a : α) → Measure γ) (a, c).1) (a, c).2
pos₁ pos₂ :
  Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) (a', c).2 =
    Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) (a, c).1) ((η : (a : α) → Measure γ) (a, c).1) (a, c).2
⊢ Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) (a', c).1) ((η : (a : α) → Measure γ) (a', c).1) (a', c).2 =
    Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) (a, c).1) ((η : (a : α) → Measure γ) (a, c).1) (a, c).2

Tactic:
rw [h_eq κ, h_eq η]
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
hα : ¬Countable α
⊢ MeasurableSpace.CountablyGenerated γ

Tactic:
have := hαγ.countableOrCountablyGenerated.resolve_left hα
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
hα : ¬Countable α
this : MeasurableSpace.CountablyGenerated γ
⊢ Measurable (β := ℝ) fun (p : α × γ) ↦
    density (β := Unit) (mβ := PUnit.instMeasurableSpace) (κ.map fun (a : γ) ↦ (a, ())) η p.1 p.2 univ

Tactic:
measurable_density _ η MeasurableSet.univ

Premises used: ProbabilityTheory.Kernel.measurable_density, MeasurableSet.univ
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
hα : ¬Countable α
this : MeasurableSpace.CountablyGenerated γ
⊢ Measurable (β := ℝ) fun (p : α × γ) ↦
    density (β := Unit) (mβ := PUnit.instMeasurableSpace) (κ.map fun (a : γ) ↦ (a, ())) η p.1 p.2 univ

Tactic:
exact measurable_density _ η MeasurableSet.univ

Premises used: ProbabilityTheory.Kernel.measurable_density, MeasurableSet.univ
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
a : α
⊢ Measurable (β := ℝ) fun (x : γ) ↦ κ.rnDerivAux η a x

Tactic:
fun_prop
-- 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
⊢ κ ≤ κ + η

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 γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
h_le : κ ≤ κ + η
pos :
  ∀ (hα : Countable α),
    ∫⁻ (x : γ) in s,
        ENNReal.ofReal
          (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((κ + η : (a : α) → Measure γ) a)
              x).toReal ∂(κ + η : (a : α) → Measure γ) a =
      (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s
neg :
  ∀ (hα : ¬Countable α),
    ∫⁻ (x : γ) in s,
        ENNReal.ofReal
          (density (β := Unit) (mβ := PUnit.instMeasurableSpace) (κ.map fun (a : γ) ↦ (a, ())) (κ + η) a x
            univ) ∂(κ + η : (a : α) → Measure γ) a =
      (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s
⊢ ∫⁻ (x : γ) in s,
      ENNReal.ofReal
        (if hα : Countable α then
          (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((κ + η : (a : α) → Measure γ) a) x).toReal
        else
          density (β := Unit) (mβ := PUnit.instMeasurableSpace) (κ.map fun (a : γ) ↦ (a, ())) (κ + η) a x
            univ) ∂(κ + η : (a : α) → Measure γ) a =
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s

Tactic:
split_ifs with hα
-- 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_le : κ ≤ κ + η
hα : Countable α
⊢ Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a)
    ((κ + η : (a : α) → Measure γ) a)

Tactic:
have h_ac : κ a ≪ (κ + η) a := Measure.absolutelyContinuous_of_le (h_le a)
-- 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_le : κ ≤ κ + η
hα : Countable α
h_ac :
  Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a)
    ((κ + η : (a : α) → Measure γ) a)
pos :
  ∫⁻ (x : γ) in s,
      ENNReal.ofReal
        (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((κ + η : (a : α) → Measure γ) a)
            x).toReal ∂(κ + η : (a : α) → Measure γ) a =
    ∫⁻ (x : γ) in s,
      Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((κ + η : (a : α) → Measure γ) a)
        x ∂(κ + η : (a : α) → Measure γ) a
⊢ ∫⁻ (x : γ) in s,
      ENNReal.ofReal
        (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((κ + η : (a : α) → Measure γ) a)
            x).toReal ∂(κ + η : (a : α) → Measure γ) a =
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s

Tactic:
rw [← Measure.setLIntegral_rnDeriv h_ac]

Premises used: MeasureTheory.Measure.setLIntegral_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_le : κ ≤ κ + η
hα : Countable α
h_ac :
  Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a)
    ((κ + η : (a : α) → Measure γ) a)
⊢ ∫⁻ (x : γ) in s,
      ENNReal.ofReal
        (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((κ + η : (a : α) → Measure γ) a)
            x).toReal ∂(κ + η : (a : α) → Measure γ) a =
    ∫⁻ (x : γ) in s,
      Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((κ + η : (a : α) → Measure γ) a)
        x ∂(κ + η : (a : α) → Measure γ) a

Tactic:
setLIntegral_congr_fun_ae hs ?_

Premises used: MeasureTheory.setLIntegral_congr_fun_ae
-- 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_le : κ ≤ κ + η
hα : Countable α
h_ac :
  Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a)
    ((κ + η : (a : α) → Measure γ) a)
pos :
  ∀ᵐ (x : γ) ∂((κ + η : (a : α) → Measure γ) a : Measure γ),
    x ∈ s →
      ENNReal.ofReal
          (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((κ + η : (a : α) → Measure γ) a) x).toReal =
        Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((κ + η : (a : α) → Measure γ) a) x
⊢ ∫⁻ (x : γ) in s,
      ENNReal.ofReal
        (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((κ + η : (a : α) → Measure γ) a)
            x).toReal ∂(κ + η : (a : α) → Measure γ) a =
    ∫⁻ (x : γ) in s,
      Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((κ + η : (a : α) → Measure γ) a)
        x ∂(κ + η : (a : α) → Measure γ) a

Tactic:
refine setLIntegral_congr_fun_ae hs ?_

Premises used: MeasureTheory.setLIntegral_congr_fun_ae
-- 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_le : κ ≤ κ + η
hα : Countable α
h_ac :
  Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a)
    ((κ + η : (a : α) → Measure γ) a)
x : γ
hx_lt : Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((κ + η : (a : α) → Measure γ) a) x < ∞
h :
  x ∈ s →
    ENNReal.ofReal
        (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((κ + η : (a : α) → Measure γ) a) x).toReal =
      Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((κ + η : (a : α) → Measure γ) a) x
⊢ x ∈ s →
    ENNReal.ofReal
        (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((κ + η : (a : α) → Measure γ) a) x).toReal =
      Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((κ + η : (a : α) → Measure γ) a) x

Tactic:
_