awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
inst_4 : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac :
  ∀ᵐ (ω : Ω) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := 𝓧) (_m0 := m𝓧) ((κ : (a : Ω) → Measure 𝓧) ω)
      ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
h1 :
  ∀ {s : Set Ω} {t : Set 𝓧} (hs : MeasurableSet s) (ht : MeasurableSet t),
    ∫⁻ (x : Ω × 𝓧) in s ×ˢ t, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) =
      (μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) (s ×ˢ t)
h2 :
  ∀ {s : Set Ω} {t : Set 𝓧} (hs : MeasurableSet s) (ht : MeasurableSet t),
    ∫⁻ (x : Ω × 𝓧) in s ×ˢ t,
        κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) x.1 x.2 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) =
      (μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) (s ×ˢ t)
rw :
  ∫⁻ (x : Ω × 𝓧) in Set.univ, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) =
    (μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) Set.univ
⊢ ∫⁻ (x : Ω × 𝓧), (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) =
    (μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) Set.univ
have rw₁ : ∫⁻ (x : Ω × 𝓧) in SProd.sprod (α := Set Ω) (β := Set 𝓧) Set.univ Set.univ,
    (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) =
  (μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) (SProd.sprod (α := Set Ω) (β := Set 𝓧) Set.univ Set.univ)
Tactic: rw [← setLIntegral_univ, ← Set.univ_prod_univ, h1 .univ .univ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
inst_4 : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac :
  ∀ᵐ (ω : Ω) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := 𝓧) (_m0 := m𝓧) ((κ : (a : Ω) → Measure 𝓧) ω)
      ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
h1 :
  ∀ {s : Set Ω} {t : Set 𝓧} (hs : MeasurableSet s) (ht : MeasurableSet t),
    ∫⁻ (x : Ω × 𝓧) in s ×ˢ t, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) =
      (μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) (s ×ˢ t)
h2 :
  ∀ {s : Set Ω} {t : Set 𝓧} (hs : MeasurableSet s) (ht : MeasurableSet t),
    ∫⁻ (x : Ω × 𝓧) in s ×ˢ t,
        κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) x.1 x.2 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) =
      (μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) (s ×ˢ t)
rw :
  ∫⁻ (x : Ω × 𝓧) in Set.univ, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) =
    (μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) Set.univ
rw₁ :
  ∫⁻ (x : Ω × 𝓧) in SProd.sprod (α := Set Ω) (β := Set 𝓧) Set.univ Set.univ,
      (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) =
    (μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) (SProd.sprod (α := Set Ω) (β := Set 𝓧) Set.univ Set.univ)
⊢ ∫⁻ (x : Ω × 𝓧), (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) =
    (μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) Set.univ
have rw₂ : Eq (α := ℝ≥0∞) ((μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) (SProd.sprod (α := Set Ω) (β := Set 𝓧) Set.univ Set.univ) : ℝ≥0∞)
  ((μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) (SProd.sprod (α := Set Ω) (β := Set 𝓧) Set.univ Set.univ) : ℝ≥0∞)
Tactic: rw [← setLIntegral_univ, ← Set.univ_prod_univ, h1 .univ .univ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
inst_4 : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac :
  ∀ᵐ (ω : Ω) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := 𝓧) (_m0 := m𝓧) ((κ : (a : Ω) → Measure 𝓧) ω)
      ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
h1 :
  ∀ {s : Set Ω} {t : Set 𝓧} (hs : MeasurableSet s) (ht : MeasurableSet t),
    ∫⁻ (x : Ω × 𝓧) in s ×ˢ t, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) =
      (μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) (s ×ˢ t)
h2 :
  ∀ {s : Set Ω} {t : Set 𝓧} (hs : MeasurableSet s) (ht : MeasurableSet t),
    ∫⁻ (x : Ω × 𝓧) in s ×ˢ t,
        κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) x.1 x.2 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) =
      (μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) (s ×ˢ t)
⊢ ∫⁻ (x : Ω × 𝓧), (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) < ∞
have calc : ∫⁻ (x : Ω × 𝓧), (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) =
  (μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) Set.univ
Tactic: calc ∫⁻ x, (κ†μ).rnDeriv (Kernel.const _ μ) x.2 x.1 ∂μ.prod (κ ∘ₘ μ)
    _ = (μ ⊗ₘ κ) Set.univ := by rw [← setLIntegral_univ, ← Set.univ_prod_univ, h1 .univ .univ]
    _ < ⊤ := measure_lt_top _ _
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
inst_4 : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac :
  ∀ᵐ (ω : Ω) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := 𝓧) (_m0 := m𝓧) ((κ : (a : Ω) → Measure 𝓧) ω)
      ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
h1 :
  ∀ {s : Set Ω} {t : Set 𝓧} (hs : MeasurableSet s) (ht : MeasurableSet t),
    ∫⁻ (x : Ω × 𝓧) in s ×ˢ t, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) =
      (μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) (s ×ˢ t)
h2 :
  ∀ {s : Set Ω} {t : Set 𝓧} (hs : MeasurableSet s) (ht : MeasurableSet t),
    ∫⁻ (x : Ω × 𝓧) in s ×ˢ t,
        κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) x.1 x.2 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) =
      (μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) (s ×ˢ t)
s : Set Ω
hs : MeasurableSet s
t : Set 𝓧
ht : MeasurableSet t
⊢ ∫⁻ (x : Ω × 𝓧) in s ×ˢ t, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) =
    ∫⁻ (x : Ω × 𝓧) in s ×ˢ t,
      κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) x.1 x.2 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
have refine_2 : (μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) (s ×ˢ t) =
  ∫⁻ (x : Ω × 𝓧) in s ×ˢ t,
    κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) x.1 x.2 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
Tactic: rw [h1 hs ht, h2 hs ht]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
inst_4 : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac :
  ∀ᵐ (ω : Ω) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := 𝓧) (_m0 := m𝓧) ((κ : (a : Ω) → Measure 𝓧) ω)
      ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
h1 :
  ∀ {s : Set Ω} {t : Set 𝓧} (hs : MeasurableSet s) (ht : MeasurableSet t),
    ∫⁻ (x : Ω × 𝓧) in s ×ˢ t, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) =
      (μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) (s ×ˢ t)
h2 :
  ∀ {s : Set Ω} {t : Set 𝓧} (hs : MeasurableSet s) (ht : MeasurableSet t),
    ∫⁻ (x : Ω × 𝓧) in s ×ˢ t,
        κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) x.1 x.2 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) =
      (μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) (s ×ˢ t)
s : Set Ω
hs : MeasurableSet s
t : Set 𝓧
ht : MeasurableSet t
refine_2 :
  (μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) (s ×ˢ t) =
    ∫⁻ (x : Ω × 𝓧) in s ×ˢ t,
      κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) x.1 x.2 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
⊢ ∫⁻ (x : Ω × 𝓧) in s ×ˢ t, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) =
    ∫⁻ (x : Ω × 𝓧) in s ×ˢ t,
      κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) x.1 x.2 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
have refine_2₁ : Eq (α := ℝ≥0∞) ((μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
  ((μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
Tactic: rw [h1 hs ht, h2 hs ht]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
inst_4 : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac :
  ∀ᵐ (ω : Ω) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := 𝓧) (_m0 := m𝓧) ((κ : (a : Ω) → Measure 𝓧) ω)
      ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
⊢ ∀ᵐ (x : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ,
    ∀ᵐ (ω : Ω) ∂μ,
      (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x
have rw : ∀ᵐ (y : Ω) ∂μ,
  ∀ᵐ (x : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ,
    (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x y = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) y x
Tactic: rw [Measure.ae_ae_comm]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
inst_4 : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac :
  ∀ᵐ (ω : Ω) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := 𝓧) (_m0 := m𝓧) ((κ : (a : Ω) → Measure 𝓧) ω)
      ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
rw :
  ∀ᵐ (y : Ω) ∂μ,
    ∀ᵐ (x : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ,
      (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x y = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) y x
⊢ ∀ᵐ (x : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ,
    ∀ᵐ (ω : Ω) ∂μ,
      (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x
have rw₁ : MeasurableSet (α := 𝓧 × Ω)
  {x : 𝓧 × Ω |
    (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.1 x.2 = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) x.2 x.1}
Tactic: rw [Measure.ae_ae_comm]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
inst_4 : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac :
  ∀ᵐ (ω : Ω) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := 𝓧) (_m0 := m𝓧) ((κ : (a : Ω) → Measure 𝓧) ω)
      ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
⊢ ∀ᵐ (x : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ,
    (κ†μ : (a : 𝓧) → Measure Ω) x =
      μ.withDensity fun (ω : Ω) ↦ κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x
have h : ∀ (x : 𝓧)
  (h :
    ∀ᵐ (ω : Ω) ∂μ,
      (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x)
  (h_ac' : (κ†μ : (a : 𝓧) → Measure Ω) x ≪ μ),
  (κ†μ : (a : 𝓧) → Measure Ω) x =
    μ.withDensity fun (ω : Ω) ↦ κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x
Tactic: filter_upwards [rnDeriv_posterior_symm h_ac, absolutelyContinuous_posterior h_ac] with x h h_ac'
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
inst_4 : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac :
  ∀ᵐ (ω : Ω) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := 𝓧) (_m0 := m𝓧) ((κ : (a : Ω) → Measure 𝓧) ω)
      ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
x : 𝓧
h :
  ∀ᵐ (ω : Ω) ∂μ, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x
h_ac' : (κ†μ : (a : 𝓧) → Measure Ω) x ≪ μ
⊢ (κ†μ : (a : 𝓧) → Measure Ω) x =
    μ.withDensity fun (ω : Ω) ↦ κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x
have h₁ : ∀ (s : Set Ω) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((((κ†μ : (a : 𝓧) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ.withDensity fun (ω : Ω) ↦ κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x : (a : Set Ω) → ℝ≥0∞)
        s :
      ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
inst_4 : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac :
  ∀ᵐ (ω : Ω) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := 𝓧) (_m0 := m𝓧) ((κ : (a : Ω) → Measure 𝓧) ω)
      ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
x : 𝓧
h :
  ∀ᵐ (ω : Ω) ∂μ, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x
h_ac' : (κ†μ : (a : 𝓧) → Measure Ω) x ≪ μ
s : Set Ω
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((κ†μ : (a : 𝓧) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ.withDensity fun (ω : Ω) ↦ κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x : (a : Set Ω) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have h₁ : ∫⁻ (x_1 : Ω) in s, (∂(κ†μ : (a : 𝓧) → Measure Ω) x/∂μ) x_1 ∂μ =
  ∫⁻ (a : Ω) in s, κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) a x ∂μ
Tactic: rw [← Measure.setLIntegral_rnDeriv h_ac', withDensity_apply _ hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
inst_4 : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac :
  ∀ᵐ (ω : Ω) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := 𝓧) (_m0 := m𝓧) ((κ : (a : Ω) → Measure 𝓧) ω)
      ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
x : 𝓧
h :
  ∀ᵐ (ω : Ω) ∂μ, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x
h_ac' : (κ†μ : (a : 𝓧) → Measure Ω) x ≪ μ
s : Set Ω
hs : MeasurableSet s
⊢ ∫⁻ (x_1 : Ω) in s, (∂(κ†μ : (a : 𝓧) → Measure Ω) x/∂μ) x_1 ∂μ =
    ∫⁻ (a : Ω) in s, κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) a x ∂μ
have h₁ : ∀ᵐ (x_1 : Ω) ∂μ,
  x_1 ∈ s → (∂(κ†μ : (a : 𝓧) → Measure Ω) x/∂μ) x_1 = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) x_1 x
Tactic: refine setLIntegral_congr_fun_ae hs ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
inst_4 : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac :
  ∀ᵐ (ω : Ω) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := 𝓧) (_m0 := m𝓧) ((κ : (a : Ω) → Measure 𝓧) ω)
      ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
x : 𝓧
h :
  ∀ᵐ (ω : Ω) ∂μ, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x
h_ac' : (κ†μ : (a : 𝓧) → Measure Ω) x ≪ μ
s : Set Ω
hs : MeasurableSet s
⊢ ∀ᵐ (x_1 : Ω) ∂μ,
    x_1 ∈ s →
      (∂(κ†μ : (a : 𝓧) → Measure Ω) x/∂μ) x_1 = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) x_1 x
have h₁ : ∀ (ω : Ω) (h : (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x)
  (h_eq :
    (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω =
      Measure.rnDeriv (m := mΩ) ((κ†μ : (a : 𝓧) → Measure Ω) x)
        (((Kernel.const 𝓧 μ : Kernel 𝓧 Ω) : (a : 𝓧) → Measure Ω) x) ω)
  (hωs : ω ∈ s),
  (∂(κ†μ : (a : 𝓧) → Measure Ω) x/∂μ) ω = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x
Tactic: filter_upwards [h, Kernel.rnDeriv_eq_rnDeriv_measure (κ := κ†μ) (η := Kernel.const 𝓧 μ) (a := x)]
    with ω h h_eq hωs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
inst_4 : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac :
  ∀ᵐ (ω : Ω) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := 𝓧) (_m0 := m𝓧) ((κ : (a : Ω) → Measure 𝓧) ω)
      ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
x : 𝓧
h_1 :
  ∀ᵐ (ω : Ω) ∂μ, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x
h_ac' : (κ†μ : (a : 𝓧) → Measure Ω) x ≪ μ
s : Set Ω
hs : MeasurableSet s
ω : Ω
h : (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x
h_eq :
  (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω =
    Measure.rnDeriv (m := mΩ) ((κ†μ : (a : 𝓧) → Measure Ω) x)
      (((Kernel.const 𝓧 μ : Kernel 𝓧 Ω) : (a : 𝓧) → Measure Ω) x) ω
hωs : ω ∈ s
⊢ (∂(κ†μ : (a : 𝓧) → Measure Ω) x/∂μ) ω = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x
have h₁ : (∂(κ†μ : (a : 𝓧) → Measure Ω) x/∂μ) ω = (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω
Tactic: rw [← h, h_eq, Kernel.const_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
inst_4 : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac :
  ∀ᵐ (ω : Ω) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := 𝓧) (_m0 := m𝓧) ((κ : (a : Ω) → Measure 𝓧) ω)
      ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
x : 𝓧
h_1 :
  ∀ᵐ (ω : Ω) ∂μ, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x
h_ac' : (κ†μ : (a : 𝓧) → Measure Ω) x ≪ μ
s : Set Ω
hs : MeasurableSet s
ω : Ω
h : (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x
h_eq :
  (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω =
    Measure.rnDeriv (m := mΩ) ((κ†μ : (a : 𝓧) → Measure Ω) x)
      (((Kernel.const 𝓧 μ : Kernel 𝓧 Ω) : (a : 𝓧) → Measure Ω) x) ω
hωs : ω ∈ s
h₁ : (∂(κ†μ : (a : 𝓧) → Measure Ω) x/∂μ) ω = (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω
⊢ (∂(κ†μ : (a : 𝓧) → Measure Ω) x/∂μ) ω = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x
have h₂ : (∂(κ†μ : (a : 𝓧) → Measure Ω) x/∂μ) ω =
  Measure.rnDeriv (m := mΩ) ((κ†μ : (a : 𝓧) → Measure Ω) x) (((Kernel.const 𝓧 μ : Kernel 𝓧 Ω) : (a : 𝓧) → Measure Ω) x)
    ω
Tactic: rw [← h, h_eq, Kernel.const_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
inst_4 : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac :
  ∀ᵐ (ω : Ω) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := 𝓧) (_m0 := m𝓧) ((κ : (a : Ω) → Measure 𝓧) ω)
      ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
x : 𝓧
h_1 :
  ∀ᵐ (ω : Ω) ∂μ, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x
h_ac' : (κ†μ : (a : 𝓧) → Measure Ω) x ≪ μ
s : Set Ω
hs : MeasurableSet s
ω : Ω
h : (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x
h_eq :
  (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω =
    Measure.rnDeriv (m := mΩ) ((κ†μ : (a : 𝓧) → Measure Ω) x)
      (((Kernel.const 𝓧 μ : Kernel 𝓧 Ω) : (a : 𝓧) → Measure Ω) x) ω
hωs : ω ∈ s
h₁ : (∂(κ†μ : (a : 𝓧) → Measure Ω) x/∂μ) ω = (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω
h₂ :
  (∂(κ†μ : (a : 𝓧) → Measure Ω) x/∂μ) ω =
    Measure.rnDeriv (m := mΩ) ((κ†μ : (a : 𝓧) → Measure Ω) x)
      (((Kernel.const 𝓧 μ : Kernel 𝓧 Ω) : (a : 𝓧) → Measure Ω) x) ω
⊢ (∂(κ†μ : (a : 𝓧) → Measure Ω) x/∂μ) ω = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x
have h₃ : (∂(κ†μ : (a : 𝓧) → Measure Ω) x/∂μ) ω = (∂(κ†μ : (a : 𝓧) → Measure Ω) x/∂μ) ω
Tactic: rw [← h, h_eq, Kernel.const_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (hypothesis)
Goal:
𝓧 : Type u_2
m𝓧 : MeasurableSpace 𝓧
Ω : Type u_5
inst : Countable Ω
inst_1 : MeasurableSpace Ω
inst_2 : Nonempty Ω
inst_3 : StandardBorelSpace Ω
κ : Kernel Ω 𝓧
inst_4 : IsFiniteKernel κ
μ : Measure Ω
inst_5 : IsFiniteMeasure μ
⊢ ∀ᵐ (x : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ,
    (κ†μ : (a : 𝓧) → Measure Ω) x =
      μ.withDensity fun (ω : Ω) ↦
        Measure.rnDeriv (m := m𝓧) ((κ : (a : Ω) → Measure 𝓧) ω) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) x
have h_rnDeriv : ∀ (ω : Ω),
  κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ))
      ω =ᶠ[ae (F := Measure 𝓧) ((Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) : (a : Ω) → Measure 𝓧) ω : Measure 𝓧)]
    Measure.rnDeriv (m := m𝓧) ((κ : (a : Ω) → Measure 𝓧) ω)
      ((Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) : (a : Ω) → Measure 𝓧) ω)
Tactic: have h_rnDeriv ω := Kernel.rnDeriv_eq_rnDeriv_measure (κ := κ) (η := Kernel.const Ω (κ ∘ₘ μ))
    (a := ω)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (hypothesis)
Goal:
𝓧 : Type u_2
m𝓧 : MeasurableSpace 𝓧
Ω : Type u_5
inst : Countable Ω
inst_1 : MeasurableSpace Ω
inst_2 : Nonempty Ω
inst_3 : StandardBorelSpace Ω
κ : Kernel Ω 𝓧
inst_4 : IsFiniteKernel κ
μ : Measure Ω
inst_5 : IsFiniteMeasure μ
h_rnDeriv :
  ∀ (ω : Ω),
    ∀ᵐ (x : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ,
      κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x =
        Measure.rnDeriv (m := m𝓧) ((κ : (a : Ω) → Measure 𝓧) ω) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) x
⊢ ∀ᵐ (x : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ,
    (κ†μ : (a : 𝓧) → Measure Ω) x =
      μ.withDensity fun (ω : Ω) ↦
        Measure.rnDeriv (m := m𝓧) ((κ : (a : Ω) → Measure 𝓧) ω) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) x
have h_rnDeriv₁ : ∀ᵐ (a : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ,
  ∀ (i : Ω),
    κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) i a =
      Measure.rnDeriv (m := m𝓧) ((κ : (a : Ω) → Measure 𝓧) i) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) a
Tactic: rw [← ae_all_iff] at h_rnDeriv
Cleared hypotheses: h_rnDeriv
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
𝓧 : Type u_2
m𝓧 : MeasurableSpace 𝓧
Ω : Type u_5
inst : Countable Ω
inst_1 : MeasurableSpace Ω
inst_2 : Nonempty Ω
inst_3 : StandardBorelSpace Ω
κ : Kernel Ω 𝓧
inst_4 : IsFiniteKernel κ
μ : Measure Ω
inst_5 : IsFiniteMeasure μ
h_rnDeriv :
  ∀ᵐ (a : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ,
    ∀ (i : Ω),
      κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) i a =
        Measure.rnDeriv (m := m𝓧) ((κ : (a : Ω) → Measure 𝓧) i) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) a
⊢ ∀ᵐ (x : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ,
    (κ†μ : (a : 𝓧) → Measure Ω) x =
      μ.withDensity fun (ω : Ω) ↦
        Measure.rnDeriv (m := m𝓧) ((κ : (a : Ω) → Measure 𝓧) ω) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) x
have h : ∀ (x : 𝓧)
  (hx :
    (κ†μ : (a : 𝓧) → Measure Ω) x =
      μ.withDensity fun (ω : Ω) ↦ κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x)
  (hx_all :
    ∀ (i : Ω),
      κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) i x =
        Measure.rnDeriv (m := m𝓧) ((κ : (a : Ω) → Measure 𝓧) i) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) x),
  (κ†μ : (a : 𝓧) → Measure Ω) x =
    μ.withDensity fun (ω : Ω) ↦
      Measure.rnDeriv (m := m𝓧) ((κ : (a : Ω) → Measure 𝓧) ω) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) x
Tactic: filter_upwards [posterior_eq_withDensity Measure.absolutelyContinuous_comp_of_countable,
    h_rnDeriv] with x hx hx_all