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

cond_c_eq_integral

PFR.Endgame · PFR/Endgame.lean:319 to 329

Mathematical statement

Exact Lean statement

lemma cond_c_eq_integral [IsProbabilityMeasure (ℙ : Measure Ω')]
    {Y Z : Ω' → G} (hY : Measurable Y) (hZ : Measurable Z) : c[Y | Z # Y | Z] =
    (Measure.map Z ℙ)[fun z => c[Y ; ℙ[|Z ← z] # Y ; ℙ[|Z ← z]]]

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma cond_c_eq_integral [IsProbabilityMeasure (ℙ : Measure Ω')]    {Y Z : Ω' → G} (hY : Measurable Y) (hZ : Measurable Z) : c[Y | Z # Y | Z] =    (Measure.map Z ℙ)[fun z => c[Y ; ℙ[|Z ← z] # Y ; ℙ[|Z ← z]]] := by  cases nonempty_fintype G  simp only [integral_fintype .of_finite, smul_sub, smul_add, smul_sub, Finset.sum_sub_distrib,    Finset.sum_add_distrib]  simp_rw [← integral_fintype .of_finite]  rw [← condRuzsaDist'_eq_integral _ hY hZ, ← condRuzsaDist'_eq_integral _ hY hZ, integral_const,    integral_const]  have : IsProbabilityMeasure (Measure.map Z ℙ) := Measure.isProbabilityMeasure_map hZ.aemeasurable  simp