LeanMachineLearning exposition

ProbabilityTheory.HasCondDistrib.hasCondDistrib_sectR🔗

Minimal Lean file

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