Source indexedlemma · leanprover/lean4:v4.33.0-rc1

condMultiDist_eq'

PFR.MoreRuzsaDist · PFR/MoreRuzsaDist.lean:1756 to 1773

Source documentation

If (X_i, Y_i), 1 ≤ i ≤ m are independent, then D[X_[m] | Y_[m]] = ∑_{(y_i)_{1 ≤ i ≤ m}} P(Y_i=y_i ∀ i) D[(X_i | Y_i=y_i ∀ i)_{i=1}^m].

Exact Lean statement

lemma condMultiDist_eq' {m : ℕ} {Ω : Type*} [hΩ : MeasureSpace Ω]
    {S : Type*} [Fintype S] [hS : MeasurableSpace S] [MeasurableSingletonClass S]
    {X : Fin m → Ω → G} (hX : ∀ i, Measurable (X i)) {Y : Fin m → Ω → S}
    (hY : ∀ i, Measurable (Y i))
    (h_indep : iIndepFun (fun i ↦ ⟨X i, Y i⟩)) :
    D[X | Y ; fun _ ↦ hΩ] =
      ∑ y : Fin m → S, (ℙ (⋂ i, (Y i) ⁻¹' {y i})).toReal
        * D[X; fun _ ↦ ⟨cond ℙ (⋂ i, Y i ⁻¹' {y i})⟩]

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma condMultiDist_eq' {m : ℕ} {Ω : Type*} [hΩ : MeasureSpace Ω]    {S : Type*} [Fintype S] [hS : MeasurableSpace S] [MeasurableSingletonClass S]    {X : Fin m → Ω → G} (hX : ∀ i, Measurable (X i)) {Y : Fin m → Ω → S}    (hY : ∀ i, Measurable (Y i))    (h_indep : iIndepFun (fun i ↦ ⟨X i, Y i⟩)) :    D[X | Y ; fun _ ↦ hΩ] =      ∑ y : Fin m → S, (ℙ (⋂ i, (Y i) ⁻¹' {y i})).toReal        * D[X; fun _ ↦ ⟨cond ℙ (⋂ i, Y i ⁻¹' {y i})⟩] := by  rw [condMultiDist]  congr with y  rw [iIndepFun.meas_iInter h_indep fun _ ↦ mes_of_comap <| .singleton _, ENNReal.toReal_prod]  by_cases hf : ∏ i : Fin m, (ℙ (Y i ⁻¹' {y i})).toReal = 0  · simp [Measure.real, hf]  congr 1  apply multiDist_copy  intro _  apply ident_of_cond_of_indep hX hY h_indep  exact prob_nonzero_of_prod_prob_nonzero hf