awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.RadonNikodym (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
⊢ (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) =ᶠ[ae (ν ⊗ₘ κ)] fun (p : α × β) ↦ μ.rnDeriv ν p.1
have refine : ∀ (s : Set (α × β)) (hs : MeasurableSet s),
  LT.lt (α := ℝ≥0∞) ((ν ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
    ∫⁻ (x : α × β) in s, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in s, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
Tactic: refine ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite (by fun_prop) (by fun_prop) fun s hs _ ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.RadonNikodym (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ν ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t₁ : Set α
t₂ : Set β
ht₁ : MeasurableSet t₁
ht₂ : MeasurableSet t₂
⊢ ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
have rw : (μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) (t₁ ×ˢ t₂) =
  ∫⁻ (a : α) in t₁, ∫⁻ (b : β) in t₂, μ.rnDeriv ν (a, b).1 ∂(κ : (a : α) → Measure β) a ∂ν
Tactic: rw [Measure.setLIntegral_rnDeriv (hμν.compProd_left _),
      Measure.setLIntegral_compProd (by fun_prop) ht₁ ht₂]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.RadonNikodym (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ν ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t₁ : Set α
t₂ : Set β
ht₁ : MeasurableSet t₁
ht₂ : MeasurableSet t₂
⊢ (μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) (t₁ ×ˢ t₂) =
    ∫⁻ (a : α) in t₁, ∫⁻ (b : β) in t₂, μ.rnDeriv ν (a, b).1 ∂(κ : (a : α) → Measure β) a ∂ν
have simp : (μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) (t₁ ×ˢ t₂) =
  ∫⁻ (a : α) in t₁,
    HMul.hMul (β := ℝ≥0∞) (μ.rnDeriv ν a)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t₂ : ℝ≥0∞) ∂ν
Tactic: simp only [MeasureTheory.lintegral_const, MeasurableSet.univ, Measure.restrict_apply,
      univ_inter]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.RadonNikodym (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ν ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t₁ : Set α
t₂ : Set β
ht₁ : MeasurableSet t₁
ht₂ : MeasurableSet t₂
⊢ (μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) (t₁ ×ˢ t₂) =
    ∫⁻ (a : α) in t₁,
      HMul.hMul (β := ℝ≥0∞) (μ.rnDeriv ν a)
        ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t₂ : ℝ≥0∞) ∂ν
have rw : (μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) (t₁ ×ˢ t₂) =
  ∫⁻ (x : α) in t₁, (((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) t₂ ∂μ
Tactic: rw [setLIntegral_rnDeriv_mul hμν (κ.measurable_coe ht₂).aemeasurable ht₁,
      Measure.compProd_apply_prod ht₁ ht₂]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.RadonNikodym (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ν ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t₁ : Set α
t₂ : Set β
ht₁ : MeasurableSet t₁
ht₂ : MeasurableSet t₂
rw :
  (μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) (t₁ ×ˢ t₂) =
    ∫⁻ (x : α) in t₁, (((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) t₂ ∂μ
⊢ (μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) (t₁ ×ˢ t₂) =
    ∫⁻ (a : α) in t₁,
      HMul.hMul (β := ℝ≥0∞) (μ.rnDeriv ν a)
        ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t₂ : ℝ≥0∞) ∂ν
have rw₁ : ∫⁻ (a : α) in t₁, (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t₂ ∂μ =
  ∫⁻ (x : α) in t₁, (((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) t₂ ∂μ
Tactic: rw [setLIntegral_rnDeriv_mul hμν (κ.measurable_coe ht₂).aemeasurable ht₁,
      Measure.compProd_apply_prod ht₁ ht₂]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.RadonNikodym (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ν ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : α × β) in s, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in s, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
have h_key : ∀ (t₁ : Set α) (t₂ : Set β),
  MeasurableSet t₁ →
    MeasurableSet t₂ →
      ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
        ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
Tactic: have h_key t₁ t₂ : MeasurableSet t₁ → MeasurableSet t₂ →
      ∫⁻ x in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
        ∫⁻ x in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ := by
    intro ht₁ ht₂
    rw [Measure.setLIntegral_rnDeriv (hμν.compProd_left _),
      Measure.setLIntegral_compProd (by fun_prop) ht₁ ht₂]
    simp only [MeasureTheory.lintegral_const, MeasurableSet.univ, Measure.restrict_apply,
      univ_inter]
    rw [setLIntegral_rnDeriv_mul hμν (κ.measurable_coe ht₂).aemeasurable ht₁,
      Measure.compProd_apply_prod ht₁ ht₂]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.RadonNikodym (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ν ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_key :
  ∀ (t₁ : Set α) (t₂ : Set β),
    MeasurableSet t₁ →
      MeasurableSet t₂ →
        ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
          ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
⊢ ∫⁻ (x : α × β) in s, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in s, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
have refine_1 : ∫⁻ (x : α × β) in ∅, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in ∅, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
Tactic: refine MeasurableSpace.induction_on_inter generateFrom_prod.symm isPiSystem_prod ?_ ?_ ?_ ?_ s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.RadonNikodym (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ν ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_key :
  ∀ (t₁ : Set α) (t₂ : Set β),
    MeasurableSet t₁ →
      MeasurableSet t₂ →
        ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
          ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
refine_1 : ∫⁻ (x : α × β) in ∅, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in ∅, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
⊢ ∫⁻ (x : α × β) in s, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in s, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
have refine_2 : ∀ (t : Set (α × β))
  (ht :
    Membership.mem (γ := Set (Set (α × β)))
      (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) {s : Set α | MeasurableSet s} {t : Set β | MeasurableSet t})
      t),
  ∫⁻ (x : α × β) in t, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in t, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
Tactic: refine MeasurableSpace.induction_on_inter generateFrom_prod.symm isPiSystem_prod ?_ ?_ ?_ ?_ s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.RadonNikodym (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ν ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_key :
  ∀ (t₁ : Set α) (t₂ : Set β),
    MeasurableSet t₁ →
      MeasurableSet t₂ →
        ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
          ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
refine_1 : ∫⁻ (x : α × β) in ∅, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in ∅, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
refine_2 :
  ∀ (t : Set (α × β))
    (ht :
      Membership.mem (γ := Set (Set (α × β)))
        (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) {s : Set α | MeasurableSet s} {t : Set β | MeasurableSet t})
        t),
    ∫⁻ (x : α × β) in t, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in t, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
⊢ ∫⁻ (x : α × β) in s, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in s, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
have refine_3 : ∀ (t : Set (α × β)) (htm : MeasurableSet t),
  ∫⁻ (x : α × β) in t, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in t, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ →
    ∫⁻ (x : α × β) in tᶜ, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in tᶜ, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
Tactic: refine MeasurableSpace.induction_on_inter generateFrom_prod.symm isPiSystem_prod ?_ ?_ ?_ ?_ s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.RadonNikodym (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ν ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_key :
  ∀ (t₁ : Set α) (t₂ : Set β),
    MeasurableSet t₁ →
      MeasurableSet t₂ →
        ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
          ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
refine_1 : ∫⁻ (x : α × β) in ∅, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in ∅, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
refine_2 :
  ∀ (t : Set (α × β))
    (ht :
      Membership.mem (γ := Set (Set (α × β)))
        (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) {s : Set α | MeasurableSet s} {t : Set β | MeasurableSet t})
        t),
    ∫⁻ (x : α × β) in t, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in t, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
refine_3 :
  ∀ (t : Set (α × β)) (htm : MeasurableSet t),
    ∫⁻ (x : α × β) in t, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in t, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ →
      ∫⁻ (x : α × β) in tᶜ, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in tᶜ, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
⊢ ∫⁻ (x : α × β) in s, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in s, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
have refine_4 : ∀ (f : ℕ → Set (α × β)),
  Pairwise (Function.onFun Disjoint f) →
    ∀ (hfm : ∀ (i : ℕ), MeasurableSet (f i)),
      (∀ (i : ℕ),
          ∫⁻ (x : α × β) in f i, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in f i, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ) →
        ∫⁻ (x : α × β) in ⋃ (i : ℕ), f i, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
          ∫⁻ (x : α × β) in ⋃ (i : ℕ), f i, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
Tactic: refine MeasurableSpace.induction_on_inter generateFrom_prod.symm isPiSystem_prod ?_ ?_ ?_ ?_ s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.RadonNikodym (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ν ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_key :
  ∀ (t₁ : Set α) (t₂ : Set β),
    MeasurableSet t₁ →
      MeasurableSet t₂ →
        ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
          ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
t : Set (α × β)
ht : MeasurableSet t
ht_eq : ∫⁻ (x : α × β) in t, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in t, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
⊢ ∫⁻ (x : α × β) in tᶜ, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in tᶜ, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
have refine_3 : ∫⁻ (x : α × β), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ - ∫⁻ (x : α × β) in t, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ =
  ∫⁻ (x : α × β), μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ - ∫⁻ (x : α × β) in t, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
Tactic: rw [setLIntegral_compl ht, ht_eq, setLIntegral_compl ht]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.RadonNikodym (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ν ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_key :
  ∀ (t₁ : Set α) (t₂ : Set β),
    MeasurableSet t₁ →
      MeasurableSet t₂ →
        ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
          ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
t : Set (α × β)
ht : MeasurableSet t
ht_eq : ∫⁻ (x : α × β) in t, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in t, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
refine_3 :
  ∫⁻ (x : α × β), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ - ∫⁻ (x : α × β) in t, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ =
    ∫⁻ (x : α × β), μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ - ∫⁻ (x : α × β) in t, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
⊢ ∫⁻ (x : α × β) in tᶜ, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in tᶜ, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
have refine_3₁ : ∫⁻ (x : α × β) in t, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ ≠ ∞
Tactic: rw [setLIntegral_compl ht, ht_eq, setLIntegral_compl ht]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.RadonNikodym (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ν ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_key :
  ∀ (t₁ : Set α) (t₂ : Set β),
    MeasurableSet t₁ →
      MeasurableSet t₂ →
        ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
          ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
t : Set (α × β)
ht : MeasurableSet t
ht_eq : ∫⁻ (x : α × β) in t, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in t, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
refine_3 :
  ∫⁻ (x : α × β), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ - ∫⁻ (x : α × β) in t, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ =
    ∫⁻ (x : α × β), μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ - ∫⁻ (x : α × β) in t, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
refine_3₁ : ∫⁻ (x : α × β) in t, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ ≠ ∞
⊢ ∫⁻ (x : α × β) in tᶜ, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in tᶜ, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
have refine_3₂ : ∫⁻ (x : α × β) in t, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ ≠ ∞
Tactic: rw [setLIntegral_compl ht, ht_eq, setLIntegral_compl ht]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.RadonNikodym (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ν ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_key :
  ∀ (t₁ : Set α) (t₂ : Set β),
    MeasurableSet t₁ →
      MeasurableSet t₂ →
        ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
          ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
t : Set (α × β)
ht : MeasurableSet t
ht_eq : ∫⁻ (x : α × β) in t, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in t, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
⊢ ∫⁻ (x : α × β), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ - ∫⁻ (x : α × β) in t, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ =
    ∫⁻ (x : α × β), μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ - ∫⁻ (x : α × β) in t, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
have refine_3 : ∫⁻ (x : α × β), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β), μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.RadonNikodym (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ν ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_key :
  ∀ (t₁ : Set α) (t₂ : Set β),
    MeasurableSet t₁ →
      MeasurableSet t₂ →
        ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
          ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
t : Set (α × β)
ht : MeasurableSet t
ht_eq : ∫⁻ (x : α × β) in t, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in t, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
⊢ ∫⁻ (x : α × β), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β), μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
have h_key₁ : ∫⁻ (x : α × β) in SProd.sprod (α := Set α) (β := Set β) univ univ, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
  ∫⁻ (x : α × β) in SProd.sprod (α := Set α) (β := Set β) univ univ, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
Tactic: specialize h_key .univ .univ .univ .univ
Cleared hypotheses: h_key
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.RadonNikodym (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ν ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_key :
  ∀ (t₁ : Set α) (t₂ : Set β),
    MeasurableSet t₁ →
      MeasurableSet t₂ →
        ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
          ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
t : Set (α × β)
ht : MeasurableSet t
ht_eq : ∫⁻ (x : α × β) in t, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in t, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
⊢ ∫⁻ (x : α × β) in t, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ ≠ ∞
have refine_3 : ∫⁻ (x : α × β) in t, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ ≠ ∞
Tactic: rw [← ht_eq]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.RadonNikodym (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ν ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_key :
  ∀ (t₁ : Set α) (t₂ : Set β),
    MeasurableSet t₁ →
      MeasurableSet t₂ →
        ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
          ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
f' : ℕ → Set (α × β)
hf_disj : Pairwise (Function.onFun Disjoint f')
hf_meas : ∀ (i : ℕ), MeasurableSet (f' i)
hf_eq :
  ∀ (i : ℕ),
    ∫⁻ (x : α × β) in f' i, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in f' i, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
⊢ ∫⁻ (x : α × β) in ⋃ (i : ℕ), f' i, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
    ∫⁻ (x : α × β) in ⋃ (i : ℕ), f' i, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
have refine_4 : Eq (α := ℝ≥0∞) (∑' (i : ℕ), ∫⁻ (a : α × β) in f' i, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) a ∂ν ⊗ₘ κ)
  (∑' (i : ℕ), ∫⁻ (a : α × β) in f' i, μ.rnDeriv ν a.1 ∂ν ⊗ₘ κ)
Tactic: rw [lintegral_iUnion hf_meas hf_disj, lintegral_iUnion hf_meas hf_disj]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.RadonNikodym (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
| (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)
have rw : ((μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)
Tactic: rw [Measure.haveLebesgueDecomposition_add μ ν]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.RadonNikodym (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
⊢ (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᶠ[ae (ν ⊗ₘ η)] (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)
have conv_rhs : (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᶠ[ae (ν ⊗ₘ η)]
  ((μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)
Tactic: conv_rhs => rw [Measure.haveLebesgueDecomposition_add μ ν]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.RadonNikodym (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
⊢ (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᶠ[ae (ν ⊗ₘ η)]
    ((μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)
have rw : (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᶠ[ae (ν ⊗ₘ η)]
  (μ.singularPart ν ⊗ₘ κ + ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)
Tactic: rw [Measure.compProd_add_left]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.RadonNikodym (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
⊢ (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᶠ[ae (ν ⊗ₘ η)]
    (μ.singularPart ν ⊗ₘ κ + ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)
have h : (μ.singularPart ν ⊗ₘ κ + ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᶠ[ae (ν ⊗ₘ η)]
  (μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) + (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)
Tactic: have h := Measure.rnDeriv_add' (μ.singularPart ν ⊗ₘ κ) (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ)
    (ν ⊗ₘ η)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.RadonNikodym (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
h :
  (μ.singularPart ν ⊗ₘ κ + ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᶠ[ae (ν ⊗ₘ η)]
    (μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) + (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)
⊢ (μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᶠ[ae (ν ⊗ₘ η)] 0
have refine_1 : μ.singularPart ν ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
Tactic: refine Measure.rnDeriv_eq_zero_of_mutuallySingular ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.RadonNikodym (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
h :
  (μ.singularPart ν ⊗ₘ κ + ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᶠ[ae (ν ⊗ₘ η)]
    (μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) + (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)
refine_1 : μ.singularPart ν ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
⊢ (μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᶠ[ae (ν ⊗ₘ η)] 0
have refine_2 : ν ⊗ₘ η ≪ ν ⊗ₘ η
Tactic: refine Measure.rnDeriv_eq_zero_of_mutuallySingular ?_ ?_