awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
ξ : Measure α
inst : SFinite μ
inst_1 : SFinite ν
inst_2 : IsSFiniteKernel κ
inst_3 : IsSFiniteKernel η
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
hμ : ξ ≪ μ
hν : ξ ≪ ν
hs : MeasurableSet h.nullSet
hμ_zero : Eq (α := ℝ≥0∞) ((μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) h.nullSet : ℝ≥0∞) (0 : ℝ≥0∞)
hν_zero : Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) h.nullSetᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∀ᵐ (x : α) ∂ξ, @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) x) ((η : (a : α) → Measure β) x)
have rw : ∀
  (hμ_zero :
    (ae μ).EventuallyEq (β := ℝ≥0∞)
      (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSet)) 0)
  (hν_zero :
    (ae ν).EventuallyEq (β := ℝ≥0∞)
      (fun (a : α) ↦ (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSetᶜ)) 0),
  ∀ᵐ (x : α) ∂ξ, @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) x) ((η : (a : α) → Measure β) x)
Tactic: rw [compProd_apply, lintegral_eq_zero_iff'] at hμ_zero hν_zero
Cleared hypotheses: hμ_zero, hν_zero
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
ξ : Measure α
inst : SFinite μ
inst_1 : SFinite ν
inst_2 : IsSFiniteKernel κ
inst_3 : IsSFiniteKernel η
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
hμ : ξ ≪ μ
hν : ξ ≪ ν
hs : MeasurableSet h.nullSet
hμ_zero : Eq (α := ℝ≥0∞) ((μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) h.nullSet : ℝ≥0∞) (0 : ℝ≥0∞)
hν_zero : Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) h.nullSetᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
rw :
  ∀
    (hμ_zero :
      (ae μ).EventuallyEq (β := ℝ≥0∞)
        (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSet)) 0)
    (hν_zero :
      (ae ν).EventuallyEq (β := ℝ≥0∞)
        (fun (a : α) ↦ (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSetᶜ)) 0),
    ∀ᵐ (x : α) ∂ξ, @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) x) ((η : (a : α) → Measure β) x)
⊢ ∀ᵐ (x : α) ∂ξ, @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) x) ((η : (a : α) → Measure β) x)
have rw₁ : ∀
  (hμ_zero :
    (ae μ).EventuallyEq (β := ℝ≥0∞)
      (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSet)) 0)
  (hν_zero :
    ∫⁻ (a : α), (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSetᶜ) ∂ν = 0),
  AEMeasurable (β := ℝ≥0∞)
    (fun (a : α) ↦ (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSetᶜ)) ν
Tactic: rw [compProd_apply, lintegral_eq_zero_iff'] at hμ_zero hν_zero
Cleared hypotheses: hμ_zero, hν_zero
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
ξ : Measure α
inst : SFinite μ
inst_1 : SFinite ν
inst_2 : IsSFiniteKernel κ
inst_3 : IsSFiniteKernel η
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
hμ : ξ ≪ μ
hν : ξ ≪ ν
hs : MeasurableSet h.nullSet
hμ_zero : Eq (α := ℝ≥0∞) ((μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) h.nullSet : ℝ≥0∞) (0 : ℝ≥0∞)
hν_zero : Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) h.nullSetᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
rw :
  ∀
    (hμ_zero :
      (ae μ).EventuallyEq (β := ℝ≥0∞)
        (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSet)) 0)
    (hν_zero :
      (ae ν).EventuallyEq (β := ℝ≥0∞)
        (fun (a : α) ↦ (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSetᶜ)) 0),
    ∀ᵐ (x : α) ∂ξ, @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) x) ((η : (a : α) → Measure β) x)
rw₁ :
  ∀
    (hμ_zero :
      (ae μ).EventuallyEq (β := ℝ≥0∞)
        (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSet)) 0)
    (hν_zero :
      ∫⁻ (a : α), (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSetᶜ) ∂ν = 0),
    AEMeasurable (β := ℝ≥0∞)
      (fun (a : α) ↦ (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSetᶜ)) ν
⊢ ∀ᵐ (x : α) ∂ξ, @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) x) ((η : (a : α) → Measure β) x)
have rw₂ : ∀
  (hμ_zero :
    ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSet) ∂μ = 0)
  (hν_zero :
    ∫⁻ (a : α), (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSetᶜ) ∂ν = 0),
  AEMeasurable (β := ℝ≥0∞)
    (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSet)) μ
Tactic: rw [compProd_apply, lintegral_eq_zero_iff'] at hμ_zero hν_zero
Cleared hypotheses: hμ_zero, hν_zero
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
ξ : Measure α
inst : SFinite μ
inst_1 : SFinite ν
inst_2 : IsSFiniteKernel κ
inst_3 : IsSFiniteKernel η
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
hμ : ξ ≪ μ
hν : ξ ≪ ν
hs : MeasurableSet h.nullSet
hμ_zero : Eq (α := ℝ≥0∞) ((μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) h.nullSet : ℝ≥0∞) (0 : ℝ≥0∞)
hν_zero : Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) h.nullSetᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
rw :
  ∀
    (hμ_zero :
      (ae μ).EventuallyEq (β := ℝ≥0∞)
        (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSet)) 0)
    (hν_zero :
      (ae ν).EventuallyEq (β := ℝ≥0∞)
        (fun (a : α) ↦ (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSetᶜ)) 0),
    ∀ᵐ (x : α) ∂ξ, @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) x) ((η : (a : α) → Measure β) x)
rw₁ :
  ∀
    (hμ_zero :
      (ae μ).EventuallyEq (β := ℝ≥0∞)
        (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSet)) 0)
    (hν_zero :
      ∫⁻ (a : α), (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSetᶜ) ∂ν = 0),
    AEMeasurable (β := ℝ≥0∞)
      (fun (a : α) ↦ (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSetᶜ)) ν
rw₂ :
  ∀
    (hμ_zero :
      ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSet) ∂μ = 0)
    (hν_zero :
      ∫⁻ (a : α), (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSetᶜ) ∂ν = 0),
    AEMeasurable (β := ℝ≥0∞)
      (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSet)) μ
⊢ ∀ᵐ (x : α) ∂ξ, @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) x) ((η : (a : α) → Measure β) x)
have rw₃ : ∀
  (hμ_zero :
    ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSet) ∂μ = 0)
  (hν_zero : Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) h.nullSetᶜ : ℝ≥0∞) (0 : ℝ≥0∞)),
  MeasurableSet h.nullSetᶜ
Tactic: rw [compProd_apply, lintegral_eq_zero_iff'] at hμ_zero hν_zero
Cleared hypotheses: hμ_zero, hν_zero
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
ξ : Measure α
inst : SFinite μ
inst_1 : SFinite ν
inst_2 : IsSFiniteKernel κ
inst_3 : IsSFiniteKernel η
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
hμ : ξ ≪ μ
hν : ξ ≪ ν
hs : MeasurableSet h.nullSet
hμ_zero :
  (ae μ).EventuallyEq (β := ℝ≥0∞)
    (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSet)) 0
hν_zero :
  (ae ν).EventuallyEq (β := ℝ≥0∞)
    (fun (a : α) ↦ (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' h.nullSetᶜ)) 0
⊢ ∀ᵐ (x : α) ∂ξ, @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) x) ((η : (a : α) → Measure β) x)
have h₁ : ∀ (x : α)
  (hxμ :
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' h.nullSet) : ℝ≥0∞)
      (0 x : ℝ≥0∞))
  (hxν :
    Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' h.nullSetᶜ) : ℝ≥0∞)
      (0 x : ℝ≥0∞)),
  @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) x) ((η : (a : α) → Measure β) x)
Tactic: filter_upwards [hμ hμ_zero, hν hν_zero] with x hxμ hxν
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : SigmaFinite ν
inst_2 : IsSFiniteKernel κ
hκ : ∀ (x : α), NeZero.{u_2} (R := Measure β) ((κ : (a : α) → Measure β) x : Measure β)
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ ↔ μ ⟂ₘ ν
have refine : ∀ (h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ), μ ⟂ₘ ν
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ h.compProd_of_left _ _⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : SigmaFinite ν
inst_2 : IsSFiniteKernel κ
hκ : ∀ (x : α), NeZero.{u_2} (R := Measure β) ((κ : (a : α) → Measure β) x : Measure β)
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ
⊢ μ ⟂ₘ ν
have rw : ν.withDensity (μ.rnDeriv ν) = 0
Tactic: rw [← withDensity_rnDeriv_eq_zero]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : SigmaFinite ν
inst_2 : IsSFiniteKernel κ
hκ : ∀ (x : α), NeZero.{u_2} (R := Measure β) ((κ : (a : α) → Measure β) x : Measure β)
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ
⊢ ν.withDensity (μ.rnDeriv ν) = 0
have refine_3 : ∀
  (hh :
    ∀ᵐ (x : α) ∂ν.withDensity (μ.rnDeriv ν),
      @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) x) ((κ : (a : α) → Measure β) x)),
  ν.withDensity (μ.rnDeriv ν) = 0
Tactic: have hh := mutuallySingular_of_mutuallySingular_compProd h ?_ ?_
    (ξ := ν.withDensity (μ.rnDeriv ν))
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : SigmaFinite ν
inst_2 : IsSFiniteKernel κ
hκ : ∀ (x : α), NeZero.{u_2} (R := Measure β) ((κ : (a : α) → Measure β) x : Measure β)
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ
refine_3 :
  ∀
    (hh :
      ∀ᵐ (x : α) ∂ν.withDensity (μ.rnDeriv ν),
        @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) x) ((κ : (a : α) → Measure β) x)),
    ν.withDensity (μ.rnDeriv ν) = 0
⊢ ν.withDensity (μ.rnDeriv ν) = 0
have refine_1 : ν.withDensity (μ.rnDeriv ν) ≪ μ
Tactic: have hh := mutuallySingular_of_mutuallySingular_compProd h ?_ ?_
    (ξ := ν.withDensity (μ.rnDeriv ν))
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : SigmaFinite ν
inst_2 : IsSFiniteKernel κ
hκ : ∀ (x : α), NeZero.{u_2} (R := Measure β) ((κ : (a : α) → Measure β) x : Measure β)
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ
refine_3 :
  ∀
    (hh :
      ∀ᵐ (x : α) ∂ν.withDensity (μ.rnDeriv ν),
        @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) x) ((κ : (a : α) → Measure β) x)),
    ν.withDensity (μ.rnDeriv ν) = 0
refine_1 : ν.withDensity (μ.rnDeriv ν) ≪ μ
⊢ ν.withDensity (μ.rnDeriv ν) = 0
have refine_2 : ν.withDensity (μ.rnDeriv ν) ≪ ν
Tactic: have hh := mutuallySingular_of_mutuallySingular_compProd h ?_ ?_
    (ξ := ν.withDensity (μ.rnDeriv ν))
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : SigmaFinite ν
inst_2 : IsSFiniteKernel κ
hκ : ∀ (x : α), NeZero.{u_2} (R := Measure β) ((κ : (a : α) → Measure β) x : Measure β)
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ
hh :
  ∀ᵐ (x : α) ∂ν.withDensity (μ.rnDeriv ν),
    @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) x) ((κ : (a : α) → Measure β) x)
⊢ ν.withDensity (μ.rnDeriv ν) = 0
have hh₁ : ∀ᵐ (x : α) ∂ν.withDensity (μ.rnDeriv ν), False
Tactic: simp_rw [MutuallySingular.self_iff, (hκ _).ne] at hh
Cleared hypotheses: hh
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
| μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
have rw : μ ⊗ₘ κ ⟂ₘ (ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)) ⊗ₘ η
Tactic: rw [ν.haveLebesgueDecomposition_add μ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η ↔ μ ⊗ₘ κ ⟂ₘ μ ⊗ₘ η
have conv_lhs : μ ⊗ₘ κ ⟂ₘ (ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)) ⊗ₘ η ↔ μ ⊗ₘ κ ⟂ₘ μ ⊗ₘ η
Tactic: conv_lhs => rw [ν.haveLebesgueDecomposition_add μ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
⊢ μ ⊗ₘ κ ⟂ₘ (ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)) ⊗ₘ η ↔ μ ⊗ₘ κ ⟂ₘ μ ⊗ₘ η
have rw : μ ⊗ₘ κ ⟂ₘ ν.singularPart μ ⊗ₘ η ∧ μ ⊗ₘ κ ⟂ₘ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η ↔ μ ⊗ₘ κ ⟂ₘ μ ⊗ₘ η
Tactic: rw [compProd_add_left, MutuallySingular.add_right_iff]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
⊢ μ ⊗ₘ κ ⟂ₘ ν.singularPart μ ⊗ₘ η ∧ μ ⊗ₘ κ ⟂ₘ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η ↔ μ ⊗ₘ κ ⟂ₘ μ ⊗ₘ η
have simp : μ ⊗ₘ κ ⟂ₘ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η ↔ μ ⊗ₘ κ ⟂ₘ μ ⊗ₘ η
Tactic: simp only [(mutuallySingular_singularPart ν μ).symm.compProd_of_left κ η, true_and]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
⊢ μ ⊗ₘ κ ⟂ₘ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η ↔ μ ⊗ₘ κ ⟂ₘ μ ⊗ₘ η
have refine_1 : ∀ (h : μ ⊗ₘ κ ⟂ₘ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η), μ ⊗ₘ η ≪ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η
Tactic: refine ⟨fun h ↦ h.mono_ac .rfl ?_, fun h ↦ h.mono_ac .rfl ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
refine_1 : ∀ (h : μ ⊗ₘ κ ⟂ₘ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η), μ ⊗ₘ η ≪ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η
⊢ μ ⊗ₘ κ ⟂ₘ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η ↔ μ ⊗ₘ κ ⟂ₘ μ ⊗ₘ η
have refine_2 : ∀ (h : μ ⊗ₘ κ ⟂ₘ μ ⊗ₘ η), μ.withDensity (ν.rnDeriv μ) ⊗ₘ η ≪ μ ⊗ₘ η
Tactic: refine ⟨fun h ↦ h.mono_ac .rfl ?_, fun h ↦ h.mono_ac .rfl ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
| μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
have rw : (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)) ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
Tactic: rw [μ.haveLebesgueDecomposition_add ν]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η ↔ ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η
have conv_lhs : (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)) ⊗ₘ κ ⟂ₘ ν ⊗ₘ η ↔
  ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η
Tactic: conv_lhs => rw [μ.haveLebesgueDecomposition_add ν]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
⊢ (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)) ⊗ₘ κ ⟂ₘ ν ⊗ₘ η ↔
    ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η
have rw : μ.singularPart ν ⊗ₘ κ ⟂ₘ ν ⊗ₘ η ∧ ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ ⟂ₘ ν ⊗ₘ η ↔
  ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η
Tactic: rw [compProd_add_left, MutuallySingular.add_left_iff]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
⊢ μ.singularPart ν ⊗ₘ κ ⟂ₘ ν ⊗ₘ η ∧ ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ ⟂ₘ ν ⊗ₘ η ↔
    ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η
have simp : ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ ⟂ₘ ν ⊗ₘ η ↔ ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η
Tactic: simp only [(mutuallySingular_singularPart μ ν).compProd_of_left κ η, true_and]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
⊢ ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ ⟂ₘ ν ⊗ₘ η ↔ ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η
have rw : ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ ⟂ₘ ν.withDensity (μ.rnDeriv ν) ⊗ₘ η ↔
  ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η
Tactic: rw [(withDensity_absolutelyContinuous ν (μ.rnDeriv ν)).mutuallySingular_compProd_iff]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
⊢ ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ ⟂ₘ ν.withDensity (μ.rnDeriv ν) ⊗ₘ η ↔
    ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η
have refine_1 : ∀ (h : ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ ⟂ₘ ν.withDensity (μ.rnDeriv ν) ⊗ₘ η) (ξ : Measure α) (hξ : SFinite ξ)
  (hξμ : ξ ≪ μ) (hξν : ξ ≪ ν), ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η
Tactic: refine ⟨fun h ξ hξ hξμ hξν ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
refine_1 :
  ∀ (h : ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ ⟂ₘ ν.withDensity (μ.rnDeriv ν) ⊗ₘ η) (ξ : Measure α) (hξ : SFinite ξ)
    (hξμ : ξ ≪ μ) (hξν : ξ ≪ ν), ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η
⊢ ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ ⟂ₘ ν.withDensity (μ.rnDeriv ν) ⊗ₘ η ↔
    ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η
have refine_2 : ∀ (h : ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η),
  ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ ⟂ₘ ν.withDensity (μ.rnDeriv ν) ⊗ₘ η
Tactic: refine ⟨fun h ξ hξ hξμ hξν ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
h : ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η
⊢ ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ ⟂ₘ ν.withDensity (μ.rnDeriv ν) ⊗ₘ η
have refine_2 : SFinite (ν.withDensity (μ.rnDeriv ν))
Tactic: refine h _ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
h : ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η
refine_2 : SFinite (ν.withDensity (μ.rnDeriv ν))
⊢ ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ ⟂ₘ ν.withDensity (μ.rnDeriv ν) ⊗ₘ η
have refine_2₁ : ν.withDensity (μ.rnDeriv ν) ≪ μ
Tactic: refine h _ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
h : ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η
refine_2 : SFinite (ν.withDensity (μ.rnDeriv ν))
refine_2₁ : ν.withDensity (μ.rnDeriv ν) ≪ μ
⊢ ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ ⟂ₘ ν.withDensity (μ.rnDeriv ν) ⊗ₘ η
have refine_2₂ : ν.withDensity (μ.rnDeriv ν) ≪ ν
Tactic: refine h _ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hκη : μ ⊗ₘ κ ≪ ν ⊗ₘ η
⊢ μ ⊗ₘ κ ≪ μ ⊗ₘ η
have hκη₁ : μ ⊗ₘ κ ≪ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η + ν.singularPart μ ⊗ₘ η
Tactic: rw [ν.haveLebesgueDecomposition_add μ, compProd_add_left, add_comm] at hκη
Cleared hypotheses: hκη
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hκη : μ ⊗ₘ κ ≪ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η + ν.singularPart μ ⊗ₘ η
⊢ μ ⊗ₘ κ ≪ μ ⊗ₘ η
have h : μ ⊗ₘ κ ≪ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η
Tactic: have h := absolutelyContinuous_of_add_of_mutuallySingular hκη
    ((mutuallySingular_singularPart _ _).symm.compProd_of_left _ _)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hκη : μ ⊗ₘ κ ≪ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η + ν.singularPart μ ⊗ₘ η
h : μ ⊗ₘ κ ≪ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η
⊢ μ ⊗ₘ κ ≪ μ ⊗ₘ η
have refine : μ.withDensity (ν.rnDeriv μ) ≪ μ
Tactic: refine h.trans (AbsolutelyContinuous.compProd_left ?_ _)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.ParallelComp (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ_1 : Kernel α β
η_1 : Kernel γ δ
x : α × γ
κ : Kernel α β
η : Kernel γ δ
h : IsSFiniteKernel κ ∧ IsSFiniteKernel η
⊢ Measurable (β := Measure (β × δ)) fun (x : α × γ) ↦
    Measure.prod ((κ : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2)
have hκ : IsSFiniteKernel κ
Tactic: have hκ := h.1
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.ParallelComp (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ_1 : Kernel α β
η_1 : Kernel γ δ
x : α × γ
κ : Kernel α β
η : Kernel γ δ
h : IsSFiniteKernel κ ∧ IsSFiniteKernel η
hκ : IsSFiniteKernel κ
⊢ Measurable (β := Measure (β × δ)) fun (x : α × γ) ↦
    Measure.prod ((κ : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2)
have hη : IsSFiniteKernel η
Tactic: have hη := h.2