awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (hypothesis)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel η
hκη : κ ≤ η
a : α
x : γ
hx_le_one : Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x ≤ 1 x
hα : ¬Countable α
⊢ density (β := Unit) (mβ := PUnit.instMeasurableSpace) (κ.map fun (a : γ) ↦ (a, ())) η a x univ ≤ 1 x
have this : MeasurableSpace.CountablyGenerated γ
Tactic: have := hαγ.countableOrCountablyGenerated.resolve_left hα
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
⊢ 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
have pos : ∀ (hα : Countable α),
  Measurable (β := ℝ) fun (p : α × γ) ↦
    (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) p.1) ((η : (a : α) → Measure γ) p.1) p.2).toReal
Tactic: split_ifs with hα
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
pos :
  ∀ (hα : Countable α),
    Measurable (β := ℝ) fun (p : α × γ) ↦
      (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) p.1) ((η : (a : α) → Measure γ) p.1) p.2).toReal
⊢ 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
have neg : ∀ (hα : ¬Countable α),
  Measurable (β := ℝ) fun (p : α × γ) ↦
    density (β := Unit) (mβ := PUnit.instMeasurableSpace) (κ.map fun (a : γ) ↦ (a, ())) η p.1 p.2 univ
Tactic: split_ifs with hα
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
hα : Countable α
⊢ Measurable (β := ℝ) fun (p : α × γ) ↦
    (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) p.1) ((η : (a : α) → Measure γ) p.1) p.2).toReal
have 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
Tactic: refine Measurable.ennreal_toReal <| measurable_from_prod_countable_right'
      (fun a ↦ Measure.measurable_rnDeriv (κ a) (η a)) fun a a' c ha'_mem_a ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ_1 η : 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 γ)
have 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∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (hypothesis)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
hα : Countable α
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
have h_eq : ∀ (κ : 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
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
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 γ)
⊢ 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
have 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
Tactic: rw [h_eq κ, h_eq η]
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
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
⊢ 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
have 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
Tactic: rw [h_eq κ, h_eq η]
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (hypothesis)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
hα : ¬Countable α
⊢ Measurable (β := ℝ) fun (p : α × γ) ↦
    density (β := Unit) (mβ := PUnit.instMeasurableSpace) (κ.map fun (a : γ) ↦ (a, ())) η p.1 p.2 univ
have this : MeasurableSpace.CountablyGenerated γ
Tactic: have := hαγ.countableOrCountablyGenerated.resolve_left hα
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (hypothesis)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (x : γ) in s, ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) ∂(κ + η : (a : α) → Measure γ) a =
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s
have h_le : κ ≤ κ + η
Tactic: have h_le : κ ≤ κ + η := le_add_of_nonneg_right bot_le
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
h_le : κ ≤ κ + η
⊢ ∫⁻ (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
have 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
Tactic: split_ifs with hα
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
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
⊢ ∫⁻ (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
have 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
Tactic: split_ifs with hα
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (hypothesis)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
h_le : κ ≤ κ + η
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
have h_ac : 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)
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
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 =
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s
have 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
Tactic: rw [← Measure.setLIntegral_rnDeriv h_ac]
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
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
have 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
Tactic: refine setLIntegral_congr_fun_ae hs ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
h_le : κ ≤ κ + η
hα : Countable α
h_ac :
  Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a)
    ((κ + η : (a : α) → Measure γ) a)
⊢ ∀ᵐ (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
have h : ∀ (x : γ) (hx_lt : 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: filter_upwards [Measure.rnDeriv_lt_top (κ a) ((κ + η) a)] with x hx_lt _
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
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
have h : Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((κ + η : (a : α) → Measure γ) a) x =
  Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((κ + η : (a : α) → Measure γ) a) x
Tactic: rw [ENNReal.ofReal_toReal hx_lt.ne]
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (hypothesis)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
h_le : κ ≤ κ + η
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
have this : MeasurableSpace.CountablyGenerated γ
Tactic: have := hαγ.countableOrCountablyGenerated.resolve_left hα
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
h_le : κ ≤ κ + η
hα : ¬Countable α
this : MeasurableSpace.CountablyGenerated γ
⊢ ∫⁻ (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
have neg : Eq (α := ℝ≥0∞)
  ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
      ((fun (a : γ) ↦ (a, ())) ⁻¹' SProd.sprod (β := Set Unit) s univ) :
    ℝ≥0∞)
  ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [setLIntegral_density ((fst_map_id_prod _ measurable_const).trans_le h_le) _
      MeasurableSet.univ hs, map_apply' _ (by fun_prop) _ (hs.prod MeasurableSet.univ)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
h_le : κ ≤ κ + η
hα : ¬Countable α
this : MeasurableSpace.CountablyGenerated γ
⊢ Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
        ((fun (a : γ) ↦ (a, ())) ⁻¹' SProd.sprod (β := Set Unit) s univ) :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
have neg : ∀ (x : γ), Membership.mem (γ := Set γ) ((fun (a : γ) ↦ (a, ())) ⁻¹' SProd.sprod (β := Set Unit) s univ) x ↔ x ∈ s
Tactic: congr 1 with x
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
⊢ ((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)) = κ
have h : ∀ (a : α) (s : Set γ) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞)
    (((((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) : (a : α) → Measure γ)
              a :
            Measure γ) :
          (a : Set γ) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext a s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    (((((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) : (a : α) → Measure γ)
              a :
            Measure γ) :
          (a : Set γ) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
have h : ∫⁻ (b : γ) in s, (↑(κ.rnDerivAux (κ + η) a b).toNNReal : ℝ≥0∞) ∂(κ + η : (a : α) → Measure γ) a =
  (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s
Tactic: rw [Kernel.withDensity_apply']
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
h :
  ∫⁻ (b : γ) in s, (↑(κ.rnDerivAux (κ + η) a b).toNNReal : ℝ≥0∞) ∂(κ + η : (a : α) → Measure γ) a =
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s
⊢ Eq (α := ℝ≥0∞)
    (((((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) : (a : α) → Measure γ)
              a :
            Measure γ) :
          (a : Set γ) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : Measurable (α := α × γ) (β := ℝ≥0∞)
  (Function.uncurry fun (a : α) (x : γ) ↦ (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞))
Tactic: rw [Kernel.withDensity_apply']
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (hypothesis)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
⊢ ((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)) = η
have h_le : κ ≤ κ + η
Tactic: have h_le : κ ≤ κ + η := le_add_of_nonneg_right bot_le
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
h_le : κ ≤ κ + η
this :
  (((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)) +
      (κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)) =
    κ + η
⊢ ((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)) = η
have h : ∀ (a : α) (s : Set γ),
  MeasurableSet s →
    Eq (α := ℝ≥0∞)
      (((((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) :
                  (a : α) → Measure γ)
                a :
              Measure γ) :
            (a : Set γ) → ℝ≥0∞)
          s :
        ℝ≥0∞)
      ((((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext a s
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
h_le : κ ≤ κ + η
this :
  (((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)) +
      (κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)) =
    κ + η
a : α
s : Set γ
h : MeasurableSet s
⊢ (((((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)) +
                (κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) :
              (a : α) → Measure γ)
            a :
          Measure γ) :
        (a : Set γ) → ℝ≥0∞)
      s =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
      ((((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
have rw : (((κ + η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s =
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [this]