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 γ
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
⊢ 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∞)
have h : (((((κ + η).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∞)
Tactic: have h : (withDensity (κ + η) (fun a x ↦ Real.toNNReal (1 - rnDerivAux κ (κ + η) a x))
          + withDensity (κ + η) (fun a x ↦ Real.toNNReal (rnDerivAux κ (κ + η) a x))) a s
        = κ a s + η a s := by
      rw [this]
      simp
-- 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_1 : MeasurableSet s
h :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      (((((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) :
                  (a : α) → Measure γ)
                a :
              Measure γ) :
            (a : Set γ) → ℝ≥0∞)
          s :
        ℝ≥0∞)
      (((((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) : (a : α) → Measure γ)
                a :
              Measure γ) :
            (a : Set γ) → ℝ≥0∞)
          s :
        ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
      ((((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ 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∞)
have h₁ : ∀
  (h :
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥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∞) =
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
        ((((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)),
  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: rwa [withDensity_rnDerivAux, add_comm, ENNReal.add_right_inj (measure_ne_top _ _)] at h
Cleared hypotheses: 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 η
h_le : κ ≤ κ + η
⊢ ((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)) = η
have suffices : (((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)) +
    (κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)) =
  κ + η
Tactic: suffices withDensity (κ + η) (fun a x ↦ Real.toNNReal (1 - rnDerivAux κ (κ + η) a x))
      + withDensity (κ + η) (fun a x ↦ Real.toNNReal (rnDerivAux κ (κ + η) a x))
      = κ + η by
    ext a s
    have h : (withDensity (κ + η) (fun a x ↦ Real.toNNReal (1 - rnDerivAux κ (κ + η) a x))
          + withDensity (κ + η) (fun a x ↦ Real.toNNReal (rnDerivAux κ (κ + η) a x))) a s
        = κ a s + η a s := by
      rw [this]
      simp
    simp only [coe_add, Pi.add_apply, Measure.coe_add] at h
    rwa [withDensity_rnDerivAux, add_comm, ENNReal.add_right_inj (measure_ne_top _ _)] at 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 η
h_le : κ ≤ κ + η
⊢ (((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)) +
      (κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)) =
    κ + η
have simp_rw : (((κ + η).withDensity fun (a : α) (x : γ) ↦ 1 - ENNReal.ofReal (κ.rnDerivAux (κ + η) a x)) +
    (κ + η).withDensity fun (a : α) (x : γ) ↦ ENNReal.ofReal (κ.rnDerivAux (κ + η) a x)) =
  κ + η
Tactic: simp_rw [ofNNReal_toNNReal, ENNReal.ofReal_sub _ (rnDerivAux_nonneg h_le), ENNReal.ofReal_one]
-- 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 : κ ≤ κ + η
⊢ (((κ + η).withDensity fun (a : α) (x : γ) ↦ 1 - ENNReal.ofReal (κ.rnDerivAux (κ + η) a x)) +
      (κ + η).withDensity fun (a : α) (x : γ) ↦ ENNReal.ofReal (κ.rnDerivAux (κ + η) a x)) =
    κ + η
have rw : ((κ + η).withDensity fun (a : α) (x : γ) ↦ 1) = κ + η
Tactic: rw [withDensity_sub_add_cancel]
-- 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 : κ ≤ κ + η
rw : ((κ + η).withDensity fun (a : α) (x : γ) ↦ 1) = κ + η
⊢ (((κ + η).withDensity fun (a : α) (x : γ) ↦ 1 - ENNReal.ofReal (κ.rnDerivAux (κ + η) a x)) +
      (κ + η).withDensity fun (a : α) (x : γ) ↦ ENNReal.ofReal (κ.rnDerivAux (κ + η) a x)) =
    κ + η
have hf : Measurable (α := α × γ) (β := ℝ≥0∞) (Function.uncurry fun (a : α) (x : γ) ↦ 1)
Tactic: rw [withDensity_sub_add_cancel]
-- 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 : κ ≤ κ + η
rw : ((κ + η).withDensity fun (a : α) (x : γ) ↦ 1) = κ + η
hf : Measurable (α := α × γ) (β := ℝ≥0∞) (Function.uncurry fun (a : α) (x : γ) ↦ 1)
⊢ (((κ + η).withDensity fun (a : α) (x : γ) ↦ 1 - ENNReal.ofReal (κ.rnDerivAux (κ + η) a x)) +
      (κ + η).withDensity fun (a : α) (x : γ) ↦ ENNReal.ofReal (κ.rnDerivAux (κ + η) a x)) =
    κ + η
have hg : Measurable (α := α × γ) (β := ℝ≥0∞) (Function.uncurry fun (a : α) (x : γ) ↦ ENNReal.ofReal (κ.rnDerivAux (κ + η) a x))
Tactic: rw [withDensity_sub_add_cancel]
-- 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 : κ ≤ κ + η
rw : ((κ + η).withDensity fun (a : α) (x : γ) ↦ 1) = κ + η
hf : Measurable (α := α × γ) (β := ℝ≥0∞) (Function.uncurry fun (a : α) (x : γ) ↦ 1)
hg :
  Measurable (α := α × γ) (β := ℝ≥0∞) (Function.uncurry fun (a : α) (x : γ) ↦ ENNReal.ofReal (κ.rnDerivAux (κ + η) a x))
⊢ (((κ + η).withDensity fun (a : α) (x : γ) ↦ 1 - ENNReal.ofReal (κ.rnDerivAux (κ + η) a x)) +
      (κ + η).withDensity fun (a : α) (x : γ) ↦ ENNReal.ofReal (κ.rnDerivAux (κ + η) a x)) =
    κ + η
have hfg : ∀ (a : α),
  (ae (F := Measure γ) ((κ + η : (a : α) → Measure γ) a : Measure γ)).EventuallyLE (β := ℝ≥0∞)
    (fun (x : γ) ↦ ENNReal.ofReal (κ.rnDerivAux (κ + η) a x)) fun (x : γ) ↦ 1
Tactic: rw [withDensity_sub_add_cancel]
-- 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 : κ ≤ κ + η
⊢ ((κ + η).withDensity fun (a : α) (x : γ) ↦ 1) = κ + η
have rw : κ + η = κ + η
Tactic: rw [withDensity_one']
-- 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 : κ ≤ κ + η
a : α
⊢ (ae (F := Measure γ) ((κ + η : (a : α) → Measure γ) a : Measure γ)).EventuallyLE (β := ℝ≥0∞)
    (fun (x : γ) ↦ ENNReal.ofReal (κ.rnDerivAux (κ + η) a x)) fun (x : γ) ↦ 1
have h : ∀ (x : γ) (hx : κ.rnDerivAux (κ + η) a x ≤ 1 x), ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) ≤ 1
Tactic: filter_upwards [rnDerivAux_le_one h_le] with x hx
-- 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 : κ ≤ κ + η
a : α
x : γ
hx : κ.rnDerivAux (κ + η) a x ≤ 1 x
⊢ ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) ≤ 1
have h : κ.rnDerivAux (κ + η) a x ≤ 1
Tactic: simp only [ENNReal.ofReal_le_one]
-- 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 α γ
a : α
x : γ
⊢ x ∈ κ.mutuallySingularSetSlice η a ↔ 1 ≤ κ.rnDerivAux (κ + η) a x
have rw : Membership.mem (γ := Set γ) {x : γ | 1 ≤ κ.rnDerivAux (κ + η) a x} x ↔ 1 ≤ κ.rnDerivAux (κ + η) a x
Tactic: rw [mutuallySingularSetSlice, mem_setOf]
-- 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 α γ
a : α
x : γ
rw : Membership.mem (γ := Set γ) {x : γ | 1 ≤ κ.rnDerivAux (κ + η) a x} x ↔ 1 ≤ κ.rnDerivAux (κ + η) a x
⊢ x ∈ κ.mutuallySingularSetSlice η a ↔ 1 ≤ κ.rnDerivAux (κ + η) a x
have rw₁ : 1 ≤ κ.rnDerivAux (κ + η) a x ↔ 1 ≤ κ.rnDerivAux (κ + η) a x
Tactic: rw [mutuallySingularSetSlice, mem_setOf]
-- 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 : α
this :
  Eq (α := ℝ≥0∞)
    (((((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) :
                (a : α) → Measure γ)
              a :
            Measure γ) :
          (a : Set γ) → ℝ≥0∞)
        {x : γ | 1 ≤ κ.rnDerivAux (κ + η) a x} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
    (0 : ℝ≥0∞)
have rwa : ∀
  (this :
    Eq (α := ℝ≥0∞)
      ((((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) {x : γ | 1 ≤ κ.rnDerivAux (κ + η) a x} : ℝ≥0∞)
      (0 : ℝ≥0∞)),
  Eq (α := ℝ≥0∞)
    ((((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
    (0 : ℝ≥0∞)
Tactic: rwa [withDensity_one_sub_rnDerivAux κ η] at this
Cleared hypotheses: this
-- 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 : α
⊢ Eq (α := ℝ≥0∞)
    ((((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
    (0 : ℝ≥0∞)
have suffices : Eq (α := ℝ≥0∞)
  (((((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) : (a : α) → Measure γ)
            a :
          Measure γ) :
        (a : Set γ) → ℝ≥0∞)
      {x : γ | 1 ≤ κ.rnDerivAux (κ + η) a x} :
    ℝ≥0∞)
  (0 : ℝ≥0∞)
Tactic: suffices withDensity (κ + η) (fun a x ↦ Real.toNNReal
      (1 - rnDerivAux κ (κ + η) a x)) a {x | 1 ≤ rnDerivAux κ (κ + η) a x} = 0 by
    rwa [withDensity_one_sub_rnDerivAux κ η] at this
-- 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 : α
⊢ Eq (α := ℝ≥0∞)
    (((((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) :
                (a : α) → Measure γ)
              a :
            Measure γ) :
          (a : Set γ) → ℝ≥0∞)
        {x : γ | 1 ≤ κ.rnDerivAux (κ + η) a x} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
have simp_rw : Eq (α := ℝ≥0∞)
  (((((κ + η).withDensity fun (a : α) (x : γ) ↦ ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) : (a : α) → Measure γ) a :
          Measure γ) :
        (a : Set γ) → ℝ≥0∞)
      {x : γ | 1 ≤ κ.rnDerivAux (κ + η) a x} :
    ℝ≥0∞)
  (0 : ℝ≥0∞)
Tactic: simp_rw [ofNNReal_toNNReal]
-- 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 : α
⊢ Eq (α := ℝ≥0∞)
    (((((κ + η).withDensity fun (a : α) (x : γ) ↦ ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) : (a : α) → Measure γ)
              a :
            Measure γ) :
          (a : Set γ) → ℝ≥0∞)
        {x : γ | 1 ≤ κ.rnDerivAux (κ + η) a x} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
have rw : ∀ᵐ (x : γ) ∂((κ + η : (a : α) → Measure γ) a : Measure γ),
  Membership.mem (γ := Set γ) {x : γ | 1 ≤ κ.rnDerivAux (κ + η) a x} x →
    ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) = 0 x
Tactic: rw [Kernel.withDensity_apply', lintegral_eq_zero_iff, EventuallyEq, ae_restrict_iff]
-- 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 : α
rw :
  ∀ᵐ (x : γ) ∂((κ + η : (a : α) → Measure γ) a : Measure γ),
    Membership.mem (γ := Set γ) {x : γ | 1 ≤ κ.rnDerivAux (κ + η) a x} x →
      ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) = 0 x
⊢ Eq (α := ℝ≥0∞)
    (((((κ + η).withDensity fun (a : α) (x : γ) ↦ ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) : (a : α) → Measure γ)
              a :
            Measure γ) :
          (a : Set γ) → ℝ≥0∞)
        {x : γ | 1 ≤ κ.rnDerivAux (κ + η) a x} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
have rw₁ : MeasurableSet.{u_2} (α := γ) {x : γ | ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) = 0 x}
Tactic: rw [Kernel.withDensity_apply', lintegral_eq_zero_iff, EventuallyEq, ae_restrict_iff]
-- 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 : α
rw :
  ∀ᵐ (x : γ) ∂((κ + η : (a : α) → Measure γ) a : Measure γ),
    Membership.mem (γ := Set γ) {x : γ | 1 ≤ κ.rnDerivAux (κ + η) a x} x →
      ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) = 0 x
rw₁ : MeasurableSet.{u_2} (α := γ) {x : γ | ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) = 0 x}
⊢ Eq (α := ℝ≥0∞)
    (((((κ + η).withDensity fun (a : α) (x : γ) ↦ ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) : (a : α) → Measure γ)
              a :
            Measure γ) :
          (a : Set γ) → ℝ≥0∞)
        {x : γ | 1 ≤ κ.rnDerivAux (κ + η) a x} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
have rw₂ : Measurable (β := ℝ≥0∞) fun (b : γ) ↦ ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a b)
Tactic: rw [Kernel.withDensity_apply', lintegral_eq_zero_iff, EventuallyEq, ae_restrict_iff]
-- 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 : α
rw :
  ∀ᵐ (x : γ) ∂((κ + η : (a : α) → Measure γ) a : Measure γ),
    Membership.mem (γ := Set γ) {x : γ | 1 ≤ κ.rnDerivAux (κ + η) a x} x →
      ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) = 0 x
rw₁ : MeasurableSet.{u_2} (α := γ) {x : γ | ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) = 0 x}
rw₂ : Measurable (β := ℝ≥0∞) fun (b : γ) ↦ ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a b)
⊢ Eq (α := ℝ≥0∞)
    (((((κ + η).withDensity fun (a : α) (x : γ) ↦ ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) : (a : α) → Measure γ)
              a :
            Measure γ) :
          (a : Set γ) → ℝ≥0∞)
        {x : γ | 1 ≤ κ.rnDerivAux (κ + η) a x} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
have hf : Measurable (α := α × γ) (β := ℝ≥0∞)
  (Function.uncurry fun (a : α) (x : γ) ↦ ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x))
Tactic: rw [Kernel.withDensity_apply', lintegral_eq_zero_iff, EventuallyEq, ae_restrict_iff]
-- 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 : α
⊢ ∀ᵐ (x : γ) ∂((κ + η : (a : α) → Measure γ) a : Measure γ),
    Membership.mem (γ := Set γ) {x : γ | 1 ≤ κ.rnDerivAux (κ + η) a x} x →
      ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) = 0 x
have refine : ∀ (x : γ) (hx : Membership.mem (γ := Set γ) {x : γ | 1 ≤ κ.rnDerivAux (κ + η) a x} x),
  ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) = 0 x
Tactic: refine ae_of_all _ (fun x hx ↦ ?_)
-- 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 α γ
⊢ κ.rnDeriv η = fun (a : α) (x : γ) ↦
    ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x)
have h : ∀ (x : α) (x_1 : γ),
  κ.rnDeriv η x x_1 = ENNReal.ofReal (κ.rnDerivAux (κ + η) x x_1) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) x x_1)
Tactic: ext
-- 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 α γ
x : α
x_1 : γ
⊢ κ.rnDeriv η x x_1 = ENNReal.ofReal (κ.rnDerivAux (κ + η) x x_1) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) x x_1)
have h : ENNReal.ofReal (κ.rnDerivAux (κ + η) x x_1) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) x x_1) =
  ENNReal.ofReal (κ.rnDerivAux (κ + η) x x_1) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) x x_1)
Tactic: rw [rnDeriv_def]
-- 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 (β := ℝ≥0∞) fun (p : α × γ) ↦ κ.rnDeriv η p.1 p.2
have simp_rw : Measurable (β := ℝ≥0∞) fun (p : α × γ) ↦
  ENNReal.ofReal (κ.rnDerivAux (κ + η) p.1 p.2) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) p.1 p.2)
Tactic: simp_rw [rnDeriv_def]
-- 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 α γ
a : α
x : γ
⊢ κ.rnDeriv η a x = ∞ ↔ (a, x) ∈ κ.mutuallySingularSet η
have simp : 1 ≤ κ.rnDerivAux (κ + η) a x → 0 < κ.rnDerivAux (κ + η) a x
Tactic: simp only [rnDeriv, ENNReal.div_eq_top, ne_eq, ENNReal.ofReal_eq_zero, not_le,
    tsub_le_iff_right, zero_add, ENNReal.ofReal_ne_top, not_false_eq_true, and_true, or_false,
    mutuallySingularSet, mem_setOf_eq, and_iff_right_iff_imp]
-- 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 α γ
a : α
x : γ
⊢ κ.rnDeriv η a x = ∞ ↔ x ∈ κ.mutuallySingularSetSlice η a
have rw : (a, x) ∈ κ.mutuallySingularSet η ↔ x ∈ κ.mutuallySingularSetSlice η a
Tactic: rw [rnDeriv_eq_top_iff, mutuallySingularSet, mutuallySingularSetSlice, mem_setOf, mem_setOf]
-- 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 α γ
a : α
x : γ
rw : (a, x) ∈ κ.mutuallySingularSet η ↔ x ∈ κ.mutuallySingularSetSlice η a
⊢ κ.rnDeriv η a x = ∞ ↔ x ∈ κ.mutuallySingularSetSlice η a
have rw₁ : Membership.mem (γ := Set (α × γ)) {p : α × γ | 1 ≤ κ.rnDerivAux (κ + η) p.1 p.2} (a, x) ↔
  x ∈ κ.mutuallySingularSetSlice η a
Tactic: rw [rnDeriv_eq_top_iff, mutuallySingularSet, mutuallySingularSetSlice, mem_setOf, mem_setOf]
-- 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 α γ
a : α
x : γ
rw : (a, x) ∈ κ.mutuallySingularSet η ↔ x ∈ κ.mutuallySingularSetSlice η a
rw₁ :
  Membership.mem (γ := Set (α × γ)) {p : α × γ | 1 ≤ κ.rnDerivAux (κ + η) p.1 p.2} (a, x) ↔
    x ∈ κ.mutuallySingularSetSlice η a
⊢ κ.rnDeriv η a x = ∞ ↔ x ∈ κ.mutuallySingularSetSlice η a
have rw₂ : Membership.mem (γ := Set (α × γ)) {p : α × γ | 1 ≤ κ.rnDerivAux (κ + η) p.1 p.2} (a, x) ↔
  Membership.mem (γ := Set γ) {x : γ | 1 ≤ κ.rnDerivAux (κ + η) a x} x
Tactic: rw [rnDeriv_eq_top_iff, mutuallySingularSet, mutuallySingularSetSlice, mem_setOf, mem_setOf]
-- 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 α γ
a : α
x : γ
rw : (a, x) ∈ κ.mutuallySingularSet η ↔ x ∈ κ.mutuallySingularSetSlice η a
rw₁ :
  Membership.mem (γ := Set (α × γ)) {p : α × γ | 1 ≤ κ.rnDerivAux (κ + η) p.1 p.2} (a, x) ↔
    x ∈ κ.mutuallySingularSetSlice η a
rw₂ :
  Membership.mem (γ := Set (α × γ)) {p : α × γ | 1 ≤ κ.rnDerivAux (κ + η) p.1 p.2} (a, x) ↔
    Membership.mem (γ := Set γ) {x : γ | 1 ≤ κ.rnDerivAux (κ + η) a x} x
⊢ κ.rnDeriv η a x = ∞ ↔ x ∈ κ.mutuallySingularSetSlice η a
have rw₃ : 1 ≤ κ.rnDerivAux (κ + η) (a, x).1 (a, x).2 ↔ Membership.mem (γ := Set γ) {x : γ | 1 ≤ κ.rnDerivAux (κ + η) a x} x
Tactic: rw [rnDeriv_eq_top_iff, mutuallySingularSet, mutuallySingularSetSlice, mem_setOf, mem_setOf]