LeanMachineLearning exposition

ProbabilityTheory.condDistrib_prod_self_left🔗

Minimal Lean file

condDistrib_prod_self_left🔗

LemmaProbabilityTheory.condDistrib_prod_self_left
Details

No docstring.

🔗theorem
ProbabilityTheory.condDistrib_prod_self_left.{u_1, u_2, u_3}
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {X : α → β} {T : α → γ}
  [MeasureTheory.IsFiniteMeasure μ] [StandardBorelSpace β] [Nonempty β]
  [StandardBorelSpace γ] [Nonempty γ] (hX : AEMeasurable X μ)
  (hT : AEMeasurable T μ) :
  ⇑𝓛[fun ω => (X ω, T ω) | T; μ] =ᵐ[MeasureTheory.Measure.map T μ]
    ⇑(Kernel.prod 𝓛[X | T; μ] Kernel.id)
ProbabilityTheory.condDistrib_prod_self_left.{u_1,
    u_2, u_3}
  {α : Type u_1} {β : Type u_2}
  {γ : Type u_3} {mα : MeasurableSpace α}
  {μ : MeasureTheory.Measure α}
  {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {X : α → β}
  {T : α → γ}
  [MeasureTheory.IsFiniteMeasure μ]
  [StandardBorelSpace β] [Nonempty β]
  [StandardBorelSpace γ] [Nonempty γ]
  (hX : AEMeasurable X μ)
  (hT : AEMeasurable T μ) :
  ⇑𝓛[fun ω => (X ω, T ω) | T;
        μ] =ᵐ[MeasureTheory.Measure.map T
      μ]
    ⇑(Kernel.prod 𝓛[X | T; μ] Kernel.id)

Code

lemma condDistrib_prod_self_left [StandardBorelSpace β] [Nonempty β] [StandardBorelSpace γ]
    [Nonempty γ]
    (hX : AEMeasurable X μ) (hT : AEMeasurable T μ) :
    condDistrib (fun ω ↦ (X ω, T ω)) T μ =ᵐ[μ.map T] condDistrib X T μ ×ₖ Kernel.id
Body uses (2)
Used by (1)

Actions: Source · Open Issue

Proof
by
  have h_prod := condDistrib_prod_left hX hT hT (μ := μ)
  have h_fst := condDistrib_comp_self (μ := μ) (fun ω ↦ (T ω, X ω)) (f := Prod.fst) (by fun_prop)
  rw [(compProd_map_condDistrib hX).symm] at h_fst
  have h_fst' := (Measure.ae_compProd_iff (Kernel.measurableSet_eq _ _)).mp h_fst
  filter_upwards [h_prod, h_fst'] with z hz1 hz2
  rw [hz1]
  simp only [Kernel.deterministic_apply] at hz2
  change ∀ᵐ y ∂(condDistrib X T μ z), condDistrib T (fun ω ↦ (T ω, X ω)) μ (z, y) = Measure.dirac z
    at hz2
  ext t ht
  rw [Kernel.compProd_apply ht]
  calc ∫⁻ y, condDistrib T (fun ω ↦ (T ω, X ω)) μ (z, y) (Prod.mk y ⁻¹' t) ∂condDistrib X T μ z
  _ = ∫⁻ y, (Measure.dirac z) (Prod.mk y ⁻¹' t) ∂condDistrib X T μ z :=
    lintegral_congr_ae (hz2.mono fun y hy ↦ by simp only [hy])
  _ = ∫⁻ y, (Prod.mk y ⁻¹' t).indicator 1 z ∂condDistrib X T μ z :=
    lintegral_congr fun y ↦ Measure.dirac_apply' _ (ht.preimage (by fun_prop))
  _ = (condDistrib X T μ z) ((fun y ↦ (y, z)) ⁻¹' t) := by
    rw [← lintegral_indicator_one (ht.preimage (by fun_prop : Measurable fun y ↦ (y, z)))]
    exact lintegral_congr fun _ ↦ rfl
  _ = ((condDistrib X T μ ×ₖ Kernel.id) z) t := by
    rw [Kernel.prod_apply, Kernel.id_apply, Measure.prod_apply_symm ht, lintegral_dirac]