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

ProbabilityTheory.IndepFun.map_add_eq_sum

PFR.Kullback · PFR/Kullback.lean:201 to 232

Source documentation

The distribution of X + Z is the convolution of the distributions of Z and X when these random variables are independent. Probably already available somewhere in some form, but I couldn't locate it.

Exact Lean statement

lemma ProbabilityTheory.IndepFun.map_add_eq_sum
    [Fintype G] [AddCommGroup G] [DiscreteMeasurableSpace G]
    {X Z : Ω → G} (h_indep : IndepFun X Z μ)
    (hX : Measurable X) (hZ : Measurable Z) (S : Set G) :
    μ.map (X + Z) S = ∑ s, μ.map Z {s} * μ.map X ({-s} + S)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma ProbabilityTheory.IndepFun.map_add_eq_sum    [Fintype G] [AddCommGroup G] [DiscreteMeasurableSpace G]    {X Z : Ω → G} (h_indep : IndepFun X Z μ)    (hX : Measurable X) (hZ : Measurable Z) (S : Set G) :    μ.map (X + Z) S = ∑ s, μ.map Z {s} * μ.map X ({-s} + S) := by  rw [Measure.map_apply (by fun_prop) (DiscreteMeasurableSpace.forall_measurableSet S)]  have : (X + Z) ⁻¹' S = ⋃ s, X ⁻¹' ({-s} + S) ∩ Z ⁻¹' {s} := by    apply Subset.antisymm    · intro y hy      simp only [mem_iUnion, mem_inter_iff, mem_preimage, mem_singleton_iff]      exact ⟨Z y, by simpa [add_comm] using hy, rfl⟩    · simp only [iUnion_subset_iff]      intro i y hy      simp only [singleton_add, image_add_left, neg_neg, mem_inter_iff, mem_preimage,        mem_singleton_iff] at hy      simp [hy.1, hy.2, add_comm]  rw [this, measure_iUnion, tsum_fintype]; rotate_left  · intro i j hij    simp only [Function.onFun, singleton_add, image_add_left, neg_neg]    apply Disjoint.inter_left'    apply Disjoint.inter_right'    apply disjoint_left.2 (fun a ha hb ↦ ?_)    rw [← ha, ← hb] at hij    exact hij rfl  · intro i    exact (hX (DiscreteMeasurableSpace.forall_measurableSet _)).inter      (hZ (measurableSet_singleton _))  congr with i  rw [h_indep.measure_inter_preimage_eq_mul _ _ (DiscreteMeasurableSpace.forall_measurableSet _)    (measurableSet_singleton _), mul_comm,    Measure.map_apply hZ (measurableSet_singleton _),    Measure.map_apply hX (DiscreteMeasurableSpace.forall_measurableSet _)]