LeanMachineLearning exposition

ProbabilityTheory.indepFun_iff_condDistrib_eq_const🔗

Minimal Lean file

indepFun_iff_condDistrib_eq_const🔗

LemmaProbabilityTheory.indepFun_iff_condDistrib_eq_const
Details

No docstring.

🔗theorem
ProbabilityTheory.indepFun_iff_condDistrib_eq_const.{u_1, u_2, u_5}
  {α : Type u_1} {β : Type u_2} {Ω : Type u_5} {mα : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {mβ : MeasurableSpace β}
  [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {X : α → β}
  {Y : α → Ω} [MeasureTheory.IsFiniteMeasure μ] (hX : AEMeasurable X μ)
  (hY : AEMeasurable Y μ) :
  IndepFun X Y μ ↔
    ⇑𝓛[Y | X; μ] =ᵐ[MeasureTheory.Measure.map X μ]
      ⇑(Kernel.const β (MeasureTheory.Measure.map Y μ))
ProbabilityTheory.indepFun_iff_condDistrib_eq_const.{u_1,
    u_2, u_5}
  {α : Type u_1} {β : Type u_2}
  {Ω : Type u_5} {mα : MeasurableSpace α}
  {μ : MeasureTheory.Measure α}
  {mβ : MeasurableSpace β}
  [MeasurableSpace Ω]
  [StandardBorelSpace Ω] [Nonempty Ω]
  {X : α → β} {Y : α → Ω}
  [MeasureTheory.IsFiniteMeasure μ]
  (hX : AEMeasurable X μ)
  (hY : AEMeasurable Y μ) :
  IndepFun X Y μ ↔
    ⇑𝓛[Y | X;
          μ] =ᵐ[MeasureTheory.Measure.map
        X μ]
      ⇑(Kernel.const β
          (MeasureTheory.Measure.map Y μ))

Code

lemma indepFun_iff_condDistrib_eq_const (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) :
    IndepFun X Y μ ↔ condDistrib Y X μ =ᵐ[μ.map X] Kernel.const β (μ.map Y)
Body uses (1)

Actions: Source · Open Issue

Proof
by
  refine ⟨fun h ↦ condDistrib_of_indepFun h hX hY, fun h ↦ ?_⟩
  rw [indepFun_iff_map_prod_eq_prod_map_map hX hY, ← compProd_map_condDistrib hY,
    Measure.compProd_congr h]
  simp