LeanMachineLearning exposition

ProbabilityTheory.Kernel.prodMkLeft_ae_eq_iff🔗

Minimal Lean file

prodMkLeft_ae_eq_iff🔗

LemmaProbabilityTheory.Kernel.prodMkLeft_ae_eq_iff
Details

No docstring.

🔗theorem
ProbabilityTheory.Kernel.prodMkLeft_ae_eq_iff.{u_1, u_2, u_3}
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
  [MeasurableSpace.CountableOrCountablyGenerated α β] {κ η : Kernel α β}
  [IsFiniteKernel κ] [IsFiniteKernel η]
  {μ : MeasureTheory.Measure (γ × α)} :
  ⇑(prodMkLeft γ κ) =ᵐ[μ] ⇑(prodMkLeft γ η) ↔
    ⇑κ =ᵐ[MeasureTheory.Measure.snd μ] ⇑η
ProbabilityTheory.Kernel.prodMkLeft_ae_eq_iff.{u_1,
    u_2, u_3}
  {α : Type u_1} {β : Type u_2}
  {γ : Type u_3} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ}
  [MeasurableSpace.CountableOrCountablyGenerated
      α β]
  {κ η : Kernel α β} [IsFiniteKernel κ]
  [IsFiniteKernel η]
  {μ : MeasureTheory.Measure (γ × α)} :
  ⇑(prodMkLeft γ κ) =ᵐ[μ]
      ⇑(prodMkLeft γ η) ↔
    ⇑κ =ᵐ[MeasureTheory.Measure.snd μ] ⇑η

Code

lemma Kernel.prodMkLeft_ae_eq_iff [MeasurableSpace.CountableOrCountablyGenerated α β]
    {κ η : Kernel α β} [IsFiniteKernel κ] [IsFiniteKernel η]
    {μ : Measure (γ × α)} :
    κ.prodMkLeft γ =ᵐ[μ] η.prodMkLeft γ ↔ κ =ᵐ[μ.snd] η
Body uses (1)

Actions: Source · Open Issue

Proof
by
  rw [Measure.snd, Filter.EventuallyEq, Filter.EventuallyEq, ae_map_iff (by fun_prop)]
  · simp
  · classical
    exact Kernel.measurableSet_eq κ η