awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.CompProdEqIff (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : MeasurableSpace.CountableOrCountablyGenerated α β
inst_1 : IsFiniteMeasure μ
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
h : μ ⊗ₘ κ = μ ⊗ₘ η
h_ac :
  ∀ᵐ (a : α) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
hκ_eq :
  ∀ᵐ (a : α) ∂μ,
    Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
      ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure β) a : Measure β)
s : Set (α × β)
hs : MeasurableSet s
h_1 : LT.lt (α := ℝ≥0∞) ((μ ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : α × β) in s, κ.rnDeriv η x.1 x.2 ∂μ ⊗ₘ η = ∫⁻ (x : α × β) in s, 1 ∂μ ⊗ₘ η
have simp : ∫⁻ (x : α × β) in s, κ.rnDeriv η x.1 x.2 ∂μ ⊗ₘ η = (μ ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) s
Tactic: simp only [MeasureTheory.lintegral_const, MeasurableSet.univ, Measure.restrict_apply,
    Set.univ_inter, one_mul]
-- Lean 4 proof step from Mathlib.Probability.Kernel.CompProdEqIff (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : MeasurableSpace.CountableOrCountablyGenerated α β
inst_1 : IsFiniteMeasure μ
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
h : μ ⊗ₘ κ = μ ⊗ₘ η
h_ac :
  ∀ᵐ (a : α) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
hκ_eq :
  ∀ᵐ (a : α) ∂μ,
    Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
      ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure β) a : Measure β)
s : Set (α × β)
hs : MeasurableSet s
h_1 : LT.lt (α := ℝ≥0∞) ((μ ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : α × β) in s, κ.rnDeriv η x.1 x.2 ∂μ ⊗ₘ η = (μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s
have rw : Measurable (Function.uncurry (κ.rnDeriv η))
Tactic: rw [Measure.compProd_congr hκ_eq, Measure.compProd_withDensity, withDensity_apply _ hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.CompProdEqIff (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : MeasurableSpace.CountableOrCountablyGenerated α β
inst_1 : IsFiniteMeasure μ
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
h : μ ⊗ₘ κ = μ ⊗ₘ η
h_ac :
  ∀ᵐ (a : α) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
hκ_eq :
  ∀ᵐ (a : α) ∂μ,
    Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
      ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure β) a : Measure β)
s : Set (α × β)
hs : MeasurableSet s
h_1 : LT.lt (α := ℝ≥0∞) ((μ ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) ((μ ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) ((μ ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Probability.Kernel.CompProdEqIff (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : MeasurableSpace.CountableOrCountablyGenerated α β
inst_1 : IsFiniteMeasure μ
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
h : μ ⊗ₘ κ = μ ⊗ₘ η
h_ac :
  ∀ᵐ (a : α) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
hκ_eq :
  ∀ᵐ (a : α) ∂μ,
    Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
      ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure β) a : Measure β)
s : Set (α × β)
hs : MeasurableSet s
h_1 : LT.lt (α := ℝ≥0∞) ((μ ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : α × β) in s, κ.rnDeriv η x.1 x.2 ∂μ ⊗ₘ η = (μ ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) s
have calc : ∫⁻ (x : α × β) in s, κ.rnDeriv η x.1 x.2 ∂μ ⊗ₘ η = (μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s
Tactic: calc ∫⁻ x in s, κ.rnDeriv η x.1 x.2 ∂μ ⊗ₘ η
  _ = (μ ⊗ₘ κ) s := by
    rw [Measure.compProd_congr hκ_eq, Measure.compProd_withDensity, withDensity_apply _ hs]
    fun_prop
  _ = (μ ⊗ₘ η) s := by rw [h]
-- Lean 4 proof step from Mathlib.Probability.Kernel.CompProdEqIff (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : MeasurableSpace.CountableOrCountablyGenerated α β
inst_1 : IsFiniteMeasure μ
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
h : μ ⊗ₘ κ = μ ⊗ₘ η
h_ac :
  ∀ᵐ (a : α) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
hκ_eq :
  ∀ᵐ (a : α) ∂μ,
    Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
      ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure β) a : Measure β)
s : Set (α × β)
hs : MeasurableSet s
h_1 : LT.lt (α := ℝ≥0∞) ((μ ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
calc : ∫⁻ (x : α × β) in s, κ.rnDeriv η x.1 x.2 ∂μ ⊗ₘ η = (μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s
⊢ ∫⁻ (x : α × β) in s, κ.rnDeriv η x.1 x.2 ∂μ ⊗ₘ η = (μ ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) s
have calc₁ : Eq (α := ℝ≥0∞) ((μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) ((μ ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: calc ∫⁻ x in s, κ.rnDeriv η x.1 x.2 ∂μ ⊗ₘ η
  _ = (μ ⊗ₘ κ) s := by
    rw [Measure.compProd_congr hκ_eq, Measure.compProd_withDensity, withDensity_apply _ hs]
    fun_prop
  _ = (μ ⊗ₘ η) s := by rw [h]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
inst_2 : MeasurableSpace.CountableOrCountablyGenerated α β
μ ν : Measure α
hκη : ∀ᵐ (a : α) ∂μ, @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
have pos : ∀ (hμ : SFinite μ), μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
Tactic: by_cases hμ : SFinite μ
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
inst_2 : MeasurableSpace.CountableOrCountablyGenerated α β
μ ν : Measure α
hκη : ∀ᵐ (a : α) ∂μ, @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
pos : ∀ (hμ : SFinite μ), μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
have neg : ∀ (hμ : ¬SFinite μ), μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
Tactic: by_cases hμ : SFinite μ
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
inst_2 : MeasurableSpace.CountableOrCountablyGenerated α β
μ ν : Measure α
hκη : ∀ᵐ (a : α) ∂μ, @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
hμ : ¬SFinite μ
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
have neg : 0 ⟂ₘ ν ⊗ₘ η
Tactic: rw [compProd_of_not_sfinite _ _ hμ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
inst_2 : MeasurableSpace.CountableOrCountablyGenerated α β
μ ν : Measure α
hκη : ∀ᵐ (a : α) ∂μ, @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
hμ : SFinite μ
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
have pos : ∀ (hν : SFinite ν), μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
Tactic: by_cases hν : SFinite ν
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
inst_2 : MeasurableSpace.CountableOrCountablyGenerated α β
μ ν : Measure α
hκη : ∀ᵐ (a : α) ∂μ, @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
hμ : SFinite μ
pos : ∀ (hν : SFinite ν), μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
have neg : ∀ (hν : ¬SFinite ν), μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
Tactic: by_cases hν : SFinite ν
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
inst_2 : MeasurableSpace.CountableOrCountablyGenerated α β
μ ν : Measure α
hκη : ∀ᵐ (a : α) ∂μ, @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
hμ : SFinite μ
hν : ¬SFinite ν
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
have neg : μ ⊗ₘ κ ⟂ₘ 0
Tactic: rw [compProd_of_not_sfinite _ _ hν]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
inst_2 : MeasurableSpace.CountableOrCountablyGenerated α β
μ ν : Measure α
hκη : ∀ᵐ (a : α) ∂μ, @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
hμ : SFinite μ
hν : SFinite ν
s : Set (α × β) := κ.mutuallySingularSet η
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
have hs : MeasurableSet s
Tactic: have hs : MeasurableSet s := Kernel.measurableSet_mutuallySingularSet κ η
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
inst_2 : MeasurableSpace.CountableOrCountablyGenerated α β
μ ν : Measure α
hκη : ∀ᵐ (a : α) ∂μ, @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
hμ : SFinite μ
hν : SFinite ν
s : Set (α × β) := κ.mutuallySingularSet η
hs : MeasurableSet s
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
have pos : ν ⊗ₘ η ⟂ₘ μ ⊗ₘ κ
Tactic: symm
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
inst_2 : MeasurableSpace.CountableOrCountablyGenerated α β
μ ν : Measure α
hκη : ∀ᵐ (a : α) ∂μ, @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
hμ : SFinite μ
hν : SFinite ν
s : Set (α × β) := κ.mutuallySingularSet η
hs : MeasurableSet s
⊢ ν ⊗ₘ η ⟂ₘ μ ⊗ₘ κ
have pos : Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
  Eq (α := ℝ≥0∞) ((μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine ⟨s, hs, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
inst_2 : MeasurableSpace.CountableOrCountablyGenerated α β
μ ν : Measure α
hκη : ∀ᵐ (a : α) ∂μ, @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
hμ : SFinite μ
hν : SFinite ν
s : Set (α × β) := κ.mutuallySingularSet η
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
have pos : ∫⁻ (a : α), (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) ∂ν = 0 ∧
  ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' sᶜ) ∂μ = 0
Tactic: rw [compProd_apply hs, compProd_apply hs.compl]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
inst_2 : MeasurableSpace.CountableOrCountablyGenerated α β
μ ν : Measure α
hκη : ∀ᵐ (a : α) ∂μ, @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
hμ : SFinite μ
hν : SFinite ν
s : Set (α × β) := κ.mutuallySingularSet η
hs : MeasurableSet s
⊢ ∫⁻ (a : α), (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) ∂ν = 0 ∧
    ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' sᶜ) ∂μ = 0
have h_eq : ∀ (a : α), Prod.mk a ⁻¹' s = κ.mutuallySingularSetSlice η a
Tactic: have h_eq a : Prod.mk a ⁻¹' s = Kernel.mutuallySingularSetSlice κ η a := rfl
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
inst_2 : MeasurableSpace.CountableOrCountablyGenerated α β
μ ν : Measure α
hκη : ∀ᵐ (a : α) ∂μ, @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
hμ : SFinite μ
hν : SFinite ν
s : Set (α × β) := κ.mutuallySingularSet η
hs : MeasurableSet s
h_eq : ∀ (a : α), Prod.mk a ⁻¹' s = κ.mutuallySingularSetSlice η a
a : α
⊢ Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞)
  ((((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [h_eq, Kernel.measure_mutuallySingularSetSlice]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
inst_2 : MeasurableSpace.CountableOrCountablyGenerated α β
μ ν : Measure α
hκη : ∀ᵐ (a : α) ∂μ, @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
hμ : SFinite μ
hν : SFinite ν
s : Set (α × β) := κ.mutuallySingularSet η
hs : MeasurableSet s
h_eq : ∀ (a : α), Prod.mk a ⁻¹' s = κ.mutuallySingularSetSlice η a
a : α
rw :
  Eq (α := ℝ≥0∞)
    ((((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [h_eq, Kernel.measure_mutuallySingularSetSlice]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
inst_2 : MeasurableSpace.CountableOrCountablyGenerated α β
μ ν : Measure α
hκη : ∀ᵐ (a : α) ∂μ, @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
hμ : SFinite μ
hν : SFinite ν
s : Set (α × β) := κ.mutuallySingularSet η
hs : MeasurableSet s
h_eq : ∀ (a : α), Prod.mk a ⁻¹' s = κ.mutuallySingularSetSlice η a
⊢ ∫⁻ (a : α), (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) ∂ν = 0 ∧
    ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' sᶜ) ∂μ = 0
have h1 : ∀ (a : α),
  Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have h1 a : η a (Prod.mk a ⁻¹' s) = 0 := by rw [h_eq, Kernel.measure_mutuallySingularSetSlice]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
inst_2 : MeasurableSpace.CountableOrCountablyGenerated α β
μ ν : Measure α
hκη : ∀ᵐ (a : α) ∂μ, @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
hμ : SFinite μ
hν : SFinite ν
s : Set (α × β) := κ.mutuallySingularSet η
hs : MeasurableSet s
h_eq : ∀ (a : α), Prod.mk a ⁻¹' s = κ.mutuallySingularSetSlice η a
h1 :
  ∀ (a : α),
    Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) : ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ ∀ᵐ (a : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s)ᶜ : ℝ≥0∞)
      (0 : ℝ≥0∞)
have h : ∀ (a : α) (ha : @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)),
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: filter_upwards [hκη] with a ha
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
inst_2 : MeasurableSpace.CountableOrCountablyGenerated α β
μ ν : Measure α
hκη : ∀ᵐ (a : α) ∂μ, @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
hμ : SFinite μ
hν : SFinite ν
s : Set (α × β) := κ.mutuallySingularSet η
hs : MeasurableSet s
h_eq : ∀ (a : α), Prod.mk a ⁻¹' s = κ.mutuallySingularSetSlice η a
h1 :
  ∀ (a : α),
    Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) : ℝ≥0∞)
      (0 : ℝ≥0∞)
a : α
ha : @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞)
  ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rwa [h_eq, ← Kernel.withDensity_rnDeriv_eq_zero_iff_measure_eq_zero κ η a,
      Kernel.withDensity_rnDeriv_eq_zero_iff_mutuallySingular]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
inst_2 : MeasurableSpace.CountableOrCountablyGenerated α β
μ ν : Measure α
hκη : ∀ᵐ (a : α) ∂μ, @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
hμ : SFinite μ
hν : SFinite ν
s : Set (α × β) := κ.mutuallySingularSet η
hs : MeasurableSet s
h_eq : ∀ (a : α), Prod.mk a ⁻¹' s = κ.mutuallySingularSetSlice η a
h1 :
  ∀ (a : α),
    Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) : ℝ≥0∞)
      (0 : ℝ≥0∞)
a : α
ha : @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
h :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a)ᶜ : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
have h₁ : Eq.{u_2 + 1} (α := Measure β) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure β) a : Measure β) (0 : Measure β)
Tactic: rwa [h_eq, ← Kernel.withDensity_rnDeriv_eq_zero_iff_measure_eq_zero κ η a,
      Kernel.withDensity_rnDeriv_eq_zero_iff_mutuallySingular]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
inst_2 : MeasurableSpace.CountableOrCountablyGenerated α β
μ ν : Measure α
hκη : ∀ᵐ (a : α) ∂μ, @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
hμ : SFinite μ
hν : SFinite ν
s : Set (α × β) := κ.mutuallySingularSet η
hs : MeasurableSet s
h_eq : ∀ (a : α), Prod.mk a ⁻¹' s = κ.mutuallySingularSetSlice η a
h1 :
  ∀ (a : α),
    Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) : ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ ∫⁻ (a : α), (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) ∂ν = 0 ∧
    ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' sᶜ) ∂μ = 0
have h2 : ∀ᵐ (a : α) ∂μ,
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have h2 : ∀ᵐ a ∂μ, κ a (Prod.mk a ⁻¹' s)ᶜ = 0 := by
    filter_upwards [hκη] with a ha
    rwa [h_eq, ← Kernel.withDensity_rnDeriv_eq_zero_iff_measure_eq_zero κ η a,
      Kernel.withDensity_rnDeriv_eq_zero_iff_mutuallySingular]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
inst_2 : MeasurableSpace.CountableOrCountablyGenerated α β
μ ν : Measure α
hκη : ∀ᵐ (a : α) ∂ν, @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
have refine : ∀ᵐ (a : α) ∂ν, @MutuallySingular.{u_2} β mβ ((η : (a : α) → Measure β) a) ((κ : (a : α) → Measure β) a)
Tactic: refine (MutuallySingular.compProd_of_right _ _ ?_).symm
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
inst_2 : MeasurableSpace.CountableOrCountablyGenerated α β
inst_3 : SFinite μ
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
this :
  ∀ᵐ (a : α) ∂μ, Eq.{u_2 + 1} (α := Measure β) ((κ.singularPart η : (a : α) → Measure β) a : Measure β) (0 : Measure β)
⊢ ∀ᵐ (a : α) ∂μ,
    AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
have h₁ : ∀ (a : α) (ha : Eq.{u_2 + 1} (α := Measure β) ((κ.singularPart η : (a : α) → Measure β) a : Measure β) (0 : Measure β)),
  AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
Tactic: filter_upwards [this] with a ha
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
inst_2 : MeasurableSpace.CountableOrCountablyGenerated α β
inst_3 : SFinite μ
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
this :
  ∀ᵐ (a : α) ∂μ, Eq.{u_2 + 1} (α := Measure β) ((κ.singularPart η : (a : α) → Measure β) a : Measure β) (0 : Measure β)
a : α
ha : Eq.{u_2 + 1} (α := Measure β) ((κ.singularPart η : (a : α) → Measure β) a : Measure β) (0 : Measure β)
⊢ AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
have h₁ : ∀ (ha : AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)),
  AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
Tactic: rwa [Kernel.singularPart_eq_zero_iff_absolutelyContinuous] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
inst_2 : MeasurableSpace.CountableOrCountablyGenerated α β
inst_3 : SFinite μ
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
⊢ ∀ᵐ (a : α) ∂μ,
    AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
have suffices : ∀ᵐ (a : α) ∂μ, Eq.{u_2 + 1} (α := Measure β) ((κ.singularPart η : (a : α) → Measure β) a : Measure β) (0 : Measure β)
Tactic: suffices ∀ᵐ a ∂μ, κ.singularPart η a = 0 by
    filter_upwards [this] with a ha
    rwa [Kernel.singularPart_eq_zero_iff_absolutelyContinuous] at ha