LeanMachineLearning exposition

ProbabilityTheory.condDistrib_condDistrib_ae_eq_sectR_condDistrib🔗

Minimal Lean file

condDistrib_condDistrib_ae_eq_sectR_condDistrib🔗

LemmaProbabilityTheory.condDistrib_condDistrib_ae_eq_sectR_condDistrib
Details

No docstring.

🔗theorem
ProbabilityTheory.condDistrib_condDistrib_ae_eq_sectR_condDistrib.{u_1,
    u_2, u_3, u_5, u_6}
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {Ω : Type u_5}
  {Ω' : Type u_6} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace Ω]
  [StandardBorelSpace Ω] [Nonempty Ω] [mΩ' : MeasurableSpace Ω']
  [StandardBorelSpace Ω'] [Nonempty Ω'] {Z : α → Ω'} {T : α → γ}
  [MeasureTheory.IsFiniteMeasure μ] [StandardBorelSpace β] [Nonempty β]
  {f : Ω' → β} {g : Ω' → Ω} (hf : Measurable f) (hg : Measurable g)
  (hZ : AEMeasurable Z μ) (hT : AEMeasurable T μ) :
  ∀ᵐ (t : γ) ∂MeasureTheory.Measure.map T μ,
    ⇑𝓛[g | f;
          𝓛[Z | T; μ] t] =ᵐ[MeasureTheory.Measure.map f (𝓛[Z | T; μ] t)]
      ⇑(Kernel.sectR 𝓛[g ∘ Z | fun a => (T a, (f ∘ Z) a); μ] t)
ProbabilityTheory.condDistrib_condDistrib_ae_eq_sectR_condDistrib.{u_1,
    u_2, u_3, u_5, u_6}
  {α : Type u_1} {β : Type u_2}
  {γ : Type u_3} {Ω : Type u_5}
  {Ω' : Type u_6} {mα : MeasurableSpace α}
  {μ : MeasureTheory.Measure α}
  {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ}
  [MeasurableSpace Ω]
  [StandardBorelSpace Ω] [Nonempty Ω]
  [mΩ' : MeasurableSpace Ω']
  [StandardBorelSpace Ω'] [Nonempty Ω']
  {Z : α → Ω'} {T : α → γ}
  [MeasureTheory.IsFiniteMeasure μ]
  [StandardBorelSpace β] [Nonempty β]
  {f : Ω' → β} {g : Ω' → Ω}
  (hf : Measurable f) (hg : Measurable g)
  (hZ : AEMeasurable Z μ)
  (hT : AEMeasurable T μ) :
  ∀ᵐ (t :
    γ) ∂MeasureTheory.Measure.map T μ,
    ⇑𝓛[g | f;
          𝓛[Z | T; μ]
            t] =ᵐ[MeasureTheory.Measure.map
        f (𝓛[Z | T; μ] t)]
      ⇑(Kernel.sectR
          𝓛[g ∘ Z | fun a =>
            (T a, (f ∘ Z) a); μ]
          t)

Code

lemma condDistrib_condDistrib_ae_eq_sectR_condDistrib [StandardBorelSpace β] [Nonempty β]
    {f : Ω' → β} {g : Ω' → Ω} (hf : Measurable f) (hg : Measurable g) (hZ : AEMeasurable Z μ)
    (hT : AEMeasurable T μ) :
    ∀ᵐ t ∂(μ.map T),
      condDistrib g f (condDistrib Z T μ t) =ᵐ[(condDistrib Z T μ t).map f]
        (condDistrib (g ∘ Z) (fun a ↦ (T a, (f ∘ Z) a)) μ).sectR t
Body uses (1)
Used by (1)

Actions: Source · Open Issue

Proof
by
  filter_upwards [
    condDistrib_prod_left (hf.comp_aemeasurable hZ) (hg.comp_aemeasurable hZ) hT,
    condDistrib_comp T hZ (hf.prodMk hg), condDistrib_comp T hZ hf] with t h_prod h_pair h_fst
  rw [condDistrib_ae_eq_iff_measure_eq_compProd f hg.aemeasurable]
  calc (condDistrib Z T μ t).map (fun ω' ↦ (f ω', g ω'))
  _ = condDistrib (fun a ↦ ((f ∘ Z) a, (g ∘ Z) a)) T μ t := by
      rw [← Kernel.map_apply _ (hf.prodMk hg)]
      exact h_pair.symm
  _ = (condDistrib Z T μ t).map f
        ⊗ₘ (condDistrib (g ∘ Z) (fun a ↦ (T a, (f ∘ Z) a)) μ).sectR t := by
      rw [h_prod, Kernel.compProd_apply_eq_compProd_sectR, h_fst, Kernel.map_apply _ hf]