LeanMachineLearning exposition

1.7. ForMathlib.Probability.HasCondDistrib🔗

A predicate for having a specified conditional distribution

Module LeanMachineLearning.ForMathlib.Probability.HasCondDistrib contains 11 exposed declarations.

hasCondDistrib_fst_prod🔗

LemmaProbabilityTheory.hasCondDistrib_fst_prod
Details

No docstring.

🔗theorem
ProbabilityTheory.hasCondDistrib_fst_prod.{u_1, u_2, u_3, u_4}
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {Ω : Type u_4}
  {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {mΩ : MeasurableSpace Ω} {Y : α → Ω}
  {X : α → β} {κ : Kernel β Ω} {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure γ} [MeasureTheory.IsProbabilityMeasure ν]
  (h : HasCondDistrib Y X κ μ) :
  HasCondDistrib (fun ω => Y (Prod.fst ω)) (fun ω => X (Prod.fst ω)) κ
    (MeasureTheory.Measure.prod μ ν)
ProbabilityTheory.hasCondDistrib_fst_prod.{u_1,
    u_2, u_3, u_4}
  {α : Type u_1} {β : Type u_2}
  {γ : Type u_3} {Ω : Type u_4}
  {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ}
  {mΩ : MeasurableSpace Ω} {Y : α → Ω}
  {X : α → β} {κ : Kernel β Ω}
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure γ}
  [MeasureTheory.IsProbabilityMeasure ν]
  (h : HasCondDistrib Y X κ μ) :
  HasCondDistrib (fun ω => Y (Prod.fst ω))
    (fun ω => X (Prod.fst ω)) κ
    (MeasureTheory.Measure.prod μ ν)

Code

lemma hasCondDistrib_fst_prod {Y : α → Ω} {X : α → β} {κ : Kernel β Ω}
    {μ : Measure α} {ν : Measure γ} [IsProbabilityMeasure ν]
    (h : HasCondDistrib Y X κ μ) :
    HasCondDistrib (fun ω ↦ Y ω.1) (fun ω ↦ X ω.1) κ (μ.prod ν) where
  aemeasurable

Actions: Source · Open Issue

Proof
by fun_prop
  map_eq := by
    have h_rhs : Measure.map (fun ω ↦ X ω.1) (μ.prod ν) ⊗ₘ κ = (μ.map X) ⊗ₘ κ := by
      conv_rhs => rw [← Measure.fst_prod (μ := μ) (ν := ν), Measure.fst]
      rw [AEMeasurable.map_map_of_aemeasurable _ (by fun_prop)]
      · rfl
      · have := h.aemeasurable_fst
        simpa
    rw [h_rhs, ← h.map_eq]
    conv_rhs => rw [← Measure.fst_prod (μ := μ) (ν := ν), Measure.fst]
    rw [AEMeasurable.map_map_of_aemeasurable _ (by fun_prop)]
    · rfl
    · have := h.aemeasurable
      simpa

prod_right🔗

LemmaProbabilityTheory.HasCondDistrib.prod_right
Details

No docstring.

🔗theorem
ProbabilityTheory.HasCondDistrib.prod_right.{u_1, u_2, u_3, u_4}
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {Ω : Type u_4}
  {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {mΩ : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure α} {X : α → β} {Y : α → Ω} {κ : Kernel β Ω}
  [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ]
  (h : HasCondDistrib Y X κ μ) {f : β → γ} (hf : Measurable f) :
  HasCondDistrib Y (fun a => (X a, f (X a))) (Kernel.prodMkRight γ κ) μ
ProbabilityTheory.HasCondDistrib.prod_right.{u_1,
    u_2, u_3, u_4}
  {α : Type u_1} {β : Type u_2}
  {γ : Type u_3} {Ω : Type u_4}
  {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ}
  {mΩ : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure α}
  {X : α → β} {Y : α → Ω} {κ : Kernel β Ω}
  [MeasureTheory.IsFiniteMeasure μ]
  [IsFiniteKernel κ]
  (h : HasCondDistrib Y X κ μ) {f : β → γ}
  (hf : Measurable f) :
  HasCondDistrib Y
    (fun a => (X a, f (X a)))
    (Kernel.prodMkRight γ κ) μ

Code

lemma HasCondDistrib.prod_right [IsFiniteMeasure μ] [IsFiniteKernel κ] (h : HasCondDistrib Y X κ μ)
    {f : β → γ} (hf : Measurable f) :
    HasCondDistrib Y (fun a ↦ (X a, f (X a))) (κ.prodMkRight _) μ
Used by (1)

Actions: Source · Open Issue

Proof
by
  refine ⟨by fun_prop, ?_⟩
  have h_eq := h.map_eq
  calc μ.map (fun x ↦ ((X x, f (X x)), Y x))
  _ = (μ.map (fun ω ↦ (X ω, Y ω))).map (fun p ↦ ((p.1, f p.1), p.2)) := by
    rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
    congr
  _ = (μ.map X ⊗ₘ κ).map (fun p ↦ ((p.1, f p.1), p.2)) := by rw [h_eq]
  _ = (μ.map X).map (fun a ↦ (a, f a)) ⊗ₘ κ.prodMkRight γ := by
    rw [Measure.compProd_eq_comp_prod, Measure.compProd_eq_comp_prod,
      ← Measure.deterministic_comp_eq_map (f := fun a ↦ (a, f a)),
      ← Measure.deterministic_comp_eq_map, Measure.comp_assoc, Measure.comp_assoc]
    swap; · fun_prop
    swap; · fun_prop
    congr 1
    ext b : 1
    rw [Kernel.comp_apply, Kernel.comp_apply, Kernel.prod_apply, Kernel.deterministic_apply,
      Kernel.id_apply, Measure.dirac_bind (Kernel.measurable _), Kernel.prod_apply,
      Measure.deterministic_comp_eq_map, Kernel.prodMkRight_apply, Kernel.id_apply]
    change Measure.map (Prod.map (fun x ↦ (x, f x)) id) ((Measure.dirac b).prod (κ b)) =
      (Measure.dirac (b, f b)).prod (κ b)
    rw [← Measure.map_prod_map _ _ (by fun_prop) (by fun_prop), Measure.map_id,
      Measure.map_dirac' (by fun_prop)]
  _ = μ.map (fun a ↦ (X a, f (X a))) ⊗ₘ κ.prodMkRight γ := by
    rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
    congr

hasCondDistrib_prod_right_iff🔗

LemmaProbabilityTheory.hasCondDistrib_prod_right_iff
Details

No docstring.

🔗theorem
ProbabilityTheory.hasCondDistrib_prod_right_iff.{u_1, u_2, u_3, u_4}
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {Ω : Type u_4}
  {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {mΩ : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure α} {κ : Kernel β Ω}
  [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ] (X : α → β)
  (Y : α → Ω) {f : β → γ} (hf : Measurable f) :
  HasCondDistrib Y (fun a => (X a, f (X a))) (Kernel.prodMkRight γ κ)
      μ ↔
    HasCondDistrib Y X κ μ
ProbabilityTheory.hasCondDistrib_prod_right_iff.{u_1,
    u_2, u_3, u_4}
  {α : Type u_1} {β : Type u_2}
  {γ : Type u_3} {Ω : Type u_4}
  {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ}
  {mΩ : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure α}
  {κ : Kernel β Ω}
  [MeasureTheory.IsFiniteMeasure μ]
  [IsFiniteKernel κ] (X : α → β)
  (Y : α → Ω) {f : β → γ}
  (hf : Measurable f) :
  HasCondDistrib Y
      (fun a => (X a, f (X a)))
      (Kernel.prodMkRight γ κ) μ ↔
    HasCondDistrib Y X κ μ

Code

lemma hasCondDistrib_prod_right_iff [IsFiniteMeasure μ] [IsFiniteKernel κ] (X : α → β) (Y : α → Ω)
    {f : β → γ} (hf : Measurable f) :
    HasCondDistrib Y (fun a ↦ (X a, f (X a))) (κ.prodMkRight _) μ ↔ HasCondDistrib Y X κ μ
Body uses (1)
Used by (1)

Actions: Source · Open Issue

Proof
by
  refine ⟨fun h ↦ ?_, fun h ↦ h.prod_right hf⟩
  have hX : AEMeasurable X μ := by
    have := h.aemeasurable_snd
    have h_eq : X = (fun p ↦ p.1) ∘ (fun a ↦ (X a, f (X a))) := by ext; simp
    rw [h_eq]
    exact Measurable.comp_aemeasurable (by fun_prop) (by fun_prop)
  refine ⟨by fun_prop, ?_⟩
  have h_eq := h.map_eq
  calc μ.map (fun x ↦ (X x, Y x))
  _ = (μ.map (fun ω ↦ ((X ω, f (X ω)), Y ω))).map (fun p ↦ (p.1.1, p.2)) := by
    rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
    congr
  _ = (μ.map (fun a ↦ (X a, f (X a))) ⊗ₘ κ.prodMkRight γ).map (fun p ↦ (p.1.1, p.2)) := by rw [h_eq]
  _ = ((μ.map X).map (fun a ↦ (a, f a)) ⊗ₘ κ.prodMkRight γ).map (fun p ↦ (p.1.1, p.2)) := by
    rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
    congr
  _ = μ.map X ⊗ₘ κ := by
    simp_rw [Measure.compProd_eq_comp_prod,
      ← Measure.deterministic_comp_eq_map (f := fun a ↦ (a, f a)) (by fun_prop),
      ← Measure.deterministic_comp_eq_map (f := fun p : (β × γ) × Ω ↦ (p.1.1, p.2)) (by fun_prop),
      Measure.comp_assoc]
    congr 1
    ext b : 1
    rw [Kernel.comp_apply, Kernel.comp_apply, Kernel.prod_apply, Kernel.id_apply,
      Kernel.deterministic_apply, Measure.dirac_bind (Kernel.measurable _),
      Kernel.prod_apply, Measure.deterministic_comp_eq_map, Kernel.prodMkRight_apply,
      Kernel.id_apply]
    change Measure.map (Prod.map (fun x ↦ x.1) id) ((Measure.dirac (b, f b)).prod (κ b)) = _
    rw [← Measure.map_prod_map _ _ (by fun_prop) (by fun_prop), Measure.map_id,
      Measure.map_dirac' (by fun_prop)]

indepFun_of_const🔗

LemmaProbabilityTheory.HasCondDistrib.indepFun_of_const
Details

No docstring.

🔗theorem
ProbabilityTheory.HasCondDistrib.indepFun_of_const.{u_1, u_2, u_4}
  {α : Type u_1} {β : Type u_2} {Ω : Type u_4} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β} {mΩ : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure α} {X : α → β} {Y : α → Ω}
  [MeasureTheory.IsProbabilityMeasure μ] {Q : MeasureTheory.Measure Ω}
  [MeasureTheory.SFinite Q]
  (h : HasCondDistrib Y X (Kernel.const β Q) μ) : IndepFun X Y μ
ProbabilityTheory.HasCondDistrib.indepFun_of_const.{u_1,
    u_2, u_4}
  {α : Type u_1} {β : Type u_2}
  {Ω : Type u_4} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  {mΩ : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure α}
  {X : α → β} {Y : α → Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {Q : MeasureTheory.Measure Ω}
  [MeasureTheory.SFinite Q]
  (h :
    HasCondDistrib Y X (Kernel.const β Q)
      μ) :
  IndepFun X Y μ

Code

lemma HasCondDistrib.indepFun_of_const [IsProbabilityMeasure μ] {Q : Measure Ω} [SFinite Q]
    (h : HasCondDistrib Y X (Kernel.const β Q) μ) :
    IndepFun X Y μ

Actions: Source · Open Issue

Proof
by
  rw [indepFun_iff_map_prod_eq_prod_map_map h.aemeasurable_fst h.aemeasurable_snd, h.map_eq,
    h.hasLaw_of_const.map_eq, Measure.compProd_const]

const_map_of_const🔗

LemmaProbabilityTheory.HasCondDistrib.const_map_of_const
Details

No docstring.

🔗theorem
ProbabilityTheory.HasCondDistrib.const_map_of_const.{u_1, u_2, u_4}
  {α : Type u_1} {β : Type u_2} {Ω : Type u_4} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β} {mΩ : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure α} {X : α → β} {Y : α → Ω}
  [MeasureTheory.IsProbabilityMeasure μ] {Q : MeasureTheory.Measure Ω}
  [MeasureTheory.SFinite Q]
  (h : HasCondDistrib Y X (Kernel.const β Q) μ) :
  HasCondDistrib X Y (Kernel.const Ω (MeasureTheory.Measure.map X μ)) μ
ProbabilityTheory.HasCondDistrib.const_map_of_const.{u_1,
    u_2, u_4}
  {α : Type u_1} {β : Type u_2}
  {Ω : Type u_4} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  {mΩ : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure α}
  {X : α → β} {Y : α → Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {Q : MeasureTheory.Measure Ω}
  [MeasureTheory.SFinite Q]
  (h :
    HasCondDistrib Y X (Kernel.const β Q)
      μ) :
  HasCondDistrib X Y
    (Kernel.const Ω
      (MeasureTheory.Measure.map X μ))
    μ

Code

lemma HasCondDistrib.const_map_of_const [IsProbabilityMeasure μ] {Q : Measure Ω} [SFinite Q]
    (h : HasCondDistrib Y X (Kernel.const β Q) μ) :
    HasCondDistrib X Y (Kernel.const Ω (μ.map X)) μ where
  aemeasurable
Used by (1)

Actions: Source · Open Issue

Proof
by fun_prop
  map_eq := by
    calc μ.map (fun ω ↦ (Y ω, X ω))
    _ = (μ.map (fun ω ↦ (X ω, Y ω))).map Prod.swap := by
      rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
      rfl
    _ = (μ.map X ⊗ₘ Kernel.const β Q).map Prod.swap := by rw [h.map_eq]
    _ = μ.map Y ⊗ₘ Kernel.const Ω (μ.map X) := by simp [h.hasLaw_of_const.map_eq, Measure.prod_swap]

prod_of_hasCondDistrib🔗

LemmaProbabilityTheory.HasLaw.prod_of_hasCondDistrib
Details

No docstring.

🔗theorem
ProbabilityTheory.HasLaw.prod_of_hasCondDistrib.{u_1, u_2, u_4}
  {α : Type u_1} {β : Type u_2} {Ω : Type u_4} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β} {mΩ : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure α} {X : α → β} {Y : α → Ω} {κ : Kernel β Ω}
  {P : MeasureTheory.Measure β} (h1 : HasLaw X P μ)
  (h2 : HasCondDistrib Y X κ μ) :
  HasLaw (fun ω => (X ω, Y ω)) (MeasureTheory.Measure.compProd P κ) μ
ProbabilityTheory.HasLaw.prod_of_hasCondDistrib.{u_1,
    u_2, u_4}
  {α : Type u_1} {β : Type u_2}
  {Ω : Type u_4} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  {mΩ : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure α}
  {X : α → β} {Y : α → Ω} {κ : Kernel β Ω}
  {P : MeasureTheory.Measure β}
  (h1 : HasLaw X P μ)
  (h2 : HasCondDistrib Y X κ μ) :
  HasLaw (fun ω => (X ω, Y ω))
    (MeasureTheory.Measure.compProd P κ) μ

Code

lemma HasLaw.prod_of_hasCondDistrib {P : Measure β}
    (h1 : HasLaw X P μ) (h2 : HasCondDistrib Y X κ μ) :
    HasLaw (fun ω ↦ (X ω, Y ω)) (P ⊗ₘ κ) μ
Used by (3)

Actions: Source · Open Issue

Proof
⟨by fun_prop, by rw [h2.map_eq, h1.map_eq]⟩

prod🔗

LemmaProbabilityTheory.HasCondDistrib.prod
Details

No docstring.

🔗theorem
ProbabilityTheory.HasCondDistrib.prod.{u_1, u_2, u_4, u_5}
  {α : Type u_1} {β : Type u_2} {Ω : Type u_4} {Ω' : Type u_5}
  {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'}
  {μ : MeasureTheory.Measure α} {X : α → β} {Y : α → Ω} {κ : Kernel β Ω}
  {Z : α → Ω'} {η : Kernel (β × Ω) Ω'} (h1 : HasCondDistrib Y X κ μ)
  (h2 : HasCondDistrib Z (fun ω => (X ω, Y ω)) η μ) :
  HasCondDistrib (fun ω => (Y ω, Z ω)) X (Kernel.compProd κ η) μ
ProbabilityTheory.HasCondDistrib.prod.{u_1,
    u_2, u_4, u_5}
  {α : Type u_1} {β : Type u_2}
  {Ω : Type u_4} {Ω' : Type u_5}
  {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  {mΩ : MeasurableSpace Ω}
  {mΩ' : MeasurableSpace Ω'}
  {μ : MeasureTheory.Measure α}
  {X : α → β} {Y : α → Ω} {κ : Kernel β Ω}
  {Z : α → Ω'} {η : Kernel (β × Ω) Ω'}
  (h1 : HasCondDistrib Y X κ μ)
  (h2 :
    HasCondDistrib Z (fun ω => (X ω, Y ω))
      η μ) :
  HasCondDistrib (fun ω => (Y ω, Z ω)) X
    (Kernel.compProd κ η) μ

Code

lemma HasCondDistrib.prod {Z : α → Ω'} {η : Kernel (β × Ω) Ω'}
    (h1 : HasCondDistrib Y X κ μ) (h2 : HasCondDistrib Z (fun ω ↦ (X ω, Y ω)) η μ) :
    HasCondDistrib (fun ω ↦ (Y ω, Z ω)) X (κ ⊗ₖ η) μ
Used by (2)

Actions: Source · Open Issue

Proof
by
  refine ⟨by fun_prop, ?_⟩
  rw [← Measure.compProd_assoc', ← h1.map_eq, ← h2.map_eq,
    AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
  rfl

ae_eq_of_hasCondDistrib_deterministic🔗

LemmaProbabilityTheory.ae_eq_of_hasCondDistrib_deterministic
Details

No docstring.

🔗theorem
ProbabilityTheory.ae_eq_of_hasCondDistrib_deterministic.{u_1, u_2, u_4}
  {α : Type u_1} {β : Type u_2} {Ω : Type u_4} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β} {mΩ : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure α} {X : α → β} {Y : α → Ω} [MeasurableEq Ω]
  [MeasureTheory.SFinite μ] {f : β → Ω} (hf : Measurable f)
  (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ)
  (h : HasCondDistrib Y X (Kernel.deterministic f hf) μ) : Y =ᵐ[μ] f ∘ X
ProbabilityTheory.ae_eq_of_hasCondDistrib_deterministic.{u_1,
    u_2, u_4}
  {α : Type u_1} {β : Type u_2}
  {Ω : Type u_4} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  {mΩ : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure α}
  {X : α → β} {Y : α → Ω} [MeasurableEq Ω]
  [MeasureTheory.SFinite μ] {f : β → Ω}
  (hf : Measurable f)
  (hX : AEMeasurable X μ)
  (hY : AEMeasurable Y μ)
  (h :
    HasCondDistrib Y X
      (Kernel.deterministic f hf) μ) :
  Y =ᵐ[μ] f ∘ X

Code

lemma ae_eq_of_hasCondDistrib_deterministic [MeasurableEq Ω] [SFinite μ] {f : β → Ω}
    (hf : Measurable f) (hX : AEMeasurable X μ)
    (hY : AEMeasurable Y μ) (h : HasCondDistrib Y X (Kernel.deterministic f hf) μ) :
    Y =ᵐ[μ] f ∘ X
Body uses (1)
Used by (1)

Actions: Source · Open Issue

Proof
by
  refine ae_eq_of_map_prodMk_eq hf hX hY ?_
  rw [h.map_eq, Measure.compProd_deterministic,
    AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
  rfl

condDistrib_eq🔗

LemmaProbabilityTheory.HasCondDistrib.condDistrib_eq
Details

No docstring.

🔗theorem
ProbabilityTheory.HasCondDistrib.condDistrib_eq.{u_1, u_2, u_4}
  {α : Type u_1} {β : Type u_2} {Ω : Type u_4} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β} {mΩ : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure α} {X : α → β} {Y : α → Ω} {κ : Kernel β Ω}
  [StandardBorelSpace Ω] [Nonempty Ω] [MeasureTheory.IsFiniteMeasure μ]
  [IsFiniteKernel κ] (h : HasCondDistrib Y X κ μ) :
  ⇑𝓛[Y | X; μ] =ᵐ[MeasureTheory.Measure.map X μ] ⇑κ
ProbabilityTheory.HasCondDistrib.condDistrib_eq.{u_1,
    u_2, u_4}
  {α : Type u_1} {β : Type u_2}
  {Ω : Type u_4} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  {mΩ : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure α}
  {X : α → β} {Y : α → Ω} {κ : Kernel β Ω}
  [StandardBorelSpace Ω] [Nonempty Ω]
  [MeasureTheory.IsFiniteMeasure μ]
  [IsFiniteKernel κ]
  (h : HasCondDistrib Y X κ μ) :
  ⇑𝓛[Y | X;
        μ] =ᵐ[MeasureTheory.Measure.map X
      μ]
    ⇑κ

Code

lemma HasCondDistrib.condDistrib_eq [IsFiniteMeasure μ] [IsFiniteKernel κ]
    (h : HasCondDistrib Y X κ μ) :
    condDistrib Y X μ =ᵐ[μ.map X] κ
Used by (13)

Actions: Source · Open Issue

Proof
by
  rw [condDistrib_ae_eq_iff_measure_eq_compProd _ (by fun_prop), h.map_eq]

hasCondDistrib_of_condDistrib_eq🔗

LemmaProbabilityTheory.hasCondDistrib_of_condDistrib_eq
Details

No docstring.

🔗theorem
ProbabilityTheory.hasCondDistrib_of_condDistrib_eq.{u_1, u_2, u_4}
  {α : Type u_1} {β : Type u_2} {Ω : Type u_4} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β} {mΩ : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure α} {X : α → β} {Y : α → Ω} {κ : Kernel β Ω}
  [StandardBorelSpace Ω] [Nonempty Ω] [MeasureTheory.IsFiniteMeasure μ]
  [IsFiniteKernel κ] (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ)
  (h : ⇑𝓛[Y | X; μ] =ᵐ[MeasureTheory.Measure.map X μ] ⇑κ) :
  HasCondDistrib Y X κ μ
ProbabilityTheory.hasCondDistrib_of_condDistrib_eq.{u_1,
    u_2, u_4}
  {α : Type u_1} {β : Type u_2}
  {Ω : Type u_4} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  {mΩ : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure α}
  {X : α → β} {Y : α → Ω} {κ : Kernel β Ω}
  [StandardBorelSpace Ω] [Nonempty Ω]
  [MeasureTheory.IsFiniteMeasure μ]
  [IsFiniteKernel κ]
  (hX : AEMeasurable X μ)
  (hY : AEMeasurable Y μ)
  (h :
    ⇑𝓛[Y | X;
          μ] =ᵐ[MeasureTheory.Measure.map
        X μ]
      ⇑κ) :
  HasCondDistrib Y X κ μ

Code

lemma hasCondDistrib_of_condDistrib_eq [IsFiniteMeasure μ] [IsFiniteKernel κ]
    (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ)
    (h : condDistrib Y X μ =ᵐ[μ.map X] κ) :
    HasCondDistrib Y X κ μ where
  aemeasurable
Used by (5)

Actions: Source · Open Issue

Proof
by fun_prop
  map_eq := by rw [← compProd_map_condDistrib hY, Measure.compProd_congr h]

hasCondDistrib_sectR🔗

LemmaProbabilityTheory.HasCondDistrib.hasCondDistrib_sectR
Details

No docstring.

🔗theorem
ProbabilityTheory.HasCondDistrib.hasCondDistrib_sectR.{u_1, u_2, u_3,
    u_4, u_5}
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {Ω : Type u_4}
  {Ω' : Type u_5} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {mΩ : MeasurableSpace Ω}
  {mΩ' : MeasurableSpace Ω'} {μ : MeasureTheory.Measure α}
  [StandardBorelSpace Ω] [Nonempty Ω] [StandardBorelSpace Ω']
  [Nonempty Ω'] [MeasureTheory.IsFiniteMeasure μ] [StandardBorelSpace β]
  [Nonempty β] {W : α → Ω'} {Z : α → γ} {f : Ω' → β} {g : Ω' → Ω}
  {η : Kernel (γ × β) Ω} [IsFiniteKernel η] (hf : Measurable f)
  (hg : Measurable g) (hW : AEMeasurable W μ)
  (hcd : HasCondDistrib (g ∘ W) (fun a => (Z a, (f ∘ W) a)) η μ) :
  ∀ᵐ (z : γ) ∂MeasureTheory.Measure.map Z μ,
    HasCondDistrib g f (Kernel.sectR η z) (𝓛[W | Z; μ] z)
ProbabilityTheory.HasCondDistrib.hasCondDistrib_sectR.{u_1,
    u_2, u_3, u_4, u_5}
  {α : Type u_1} {β : Type u_2}
  {γ : Type u_3} {Ω : Type u_4}
  {Ω' : Type u_5} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ}
  {mΩ : MeasurableSpace Ω}
  {mΩ' : MeasurableSpace Ω'}
  {μ : MeasureTheory.Measure α}
  [StandardBorelSpace Ω] [Nonempty Ω]
  [StandardBorelSpace Ω'] [Nonempty Ω']
  [MeasureTheory.IsFiniteMeasure μ]
  [StandardBorelSpace β] [Nonempty β]
  {W : α → Ω'} {Z : α → γ} {f : Ω' → β}
  {g : Ω' → Ω} {η : Kernel (γ × β) Ω}
  [IsFiniteKernel η] (hf : Measurable f)
  (hg : Measurable g)
  (hW : AEMeasurable W μ)
  (hcd :
    HasCondDistrib (g ∘ W)
      (fun a => (Z a, (f ∘ W) a)) η μ) :
  ∀ᵐ (z :
    γ) ∂MeasureTheory.Measure.map Z μ,
    HasCondDistrib g f (Kernel.sectR η z)
      (𝓛[W | Z; μ] z)

Code

lemma HasCondDistrib.hasCondDistrib_sectR [IsFiniteMeasure μ] [StandardBorelSpace β] [Nonempty β]
    {W : α → Ω'} {Z : α → γ} {f : Ω' → β} {g : Ω' → Ω}
    {η : Kernel (γ × β) Ω} [IsFiniteKernel η] (hf : Measurable f)
    (hg : Measurable g) (hW : AEMeasurable W μ)
    (hcd : HasCondDistrib (g ∘ W) (fun a ↦ (Z a, (f ∘ W) a)) η μ) :
    ∀ᵐ z ∂(μ.map Z), HasCondDistrib g f (η.sectR z) (condDistrib W Z μ z)
Body uses (3)
Used by (3)

Actions: Source · Open Issue

Proof
by
  suffices ∀ᵐ z ∂μ.map Z, condDistrib g f (condDistrib W Z μ z) =ᵐ[(condDistrib W Z μ z).map f]
      (η.sectR z) by
    filter_upwards [this] with z hz
    exact hasCondDistrib_of_condDistrib_eq (by fun_prop) (by fun_prop) hz
  have h_eq : condDistrib (g ∘ W) (fun a ↦ (Z a, (f ∘ W) a)) μ
      =ᵐ[μ.map Z ⊗ₘ (condDistrib W Z μ).map f] η := by
    rw [← Measure.compProd_congr (condDistrib_comp Z hW hf),
        compProd_map_condDistrib (hf.comp_aemeasurable hW)]
    exact hcd.condDistrib_eq
  filter_upwards [
    condDistrib_condDistrib_ae_eq_sectR_condDistrib hf hg hW hcd.aemeasurable_fst.fst,
    Measure.ae_ae_of_ae_compProd h_eq] with z hc ha
  rw [Kernel.map_apply _ hf] at ha
  filter_upwards [hc, ha] with b hcb hab using hcb.trans hab
  1. ProbabilityTheory.hasCondDistrib_fst_prod
  2. ProbabilityTheory.HasCondDistrib.prod_right
  3. ProbabilityTheory.hasCondDistrib_prod_right_iff
  4. ProbabilityTheory.HasCondDistrib.indepFun_of_const
  5. ProbabilityTheory.HasCondDistrib.const_map_of_const
  6. ProbabilityTheory.HasLaw.prod_of_hasCondDistrib
  7. ProbabilityTheory.HasCondDistrib.prod
  8. ProbabilityTheory.ae_eq_of_hasCondDistrib_deterministic
  9. ProbabilityTheory.HasCondDistrib.condDistrib_eq
  10. ProbabilityTheory.hasCondDistrib_of_condDistrib_eq
  11. ProbabilityTheory.HasCondDistrib.hasCondDistrib_sectR