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

absolutelyContinuous_add_of_indep

PFR.Kullback · PFR/Kullback.lean:270 to 284

Mathematical statement

Exact Lean statement

lemma absolutelyContinuous_add_of_indep [Finite G] [AddCommGroup G] [DiscreteMeasurableSpace G]
    {X Y Z : Ω → G} (h_indep : IndepFun (⟨X, Y⟩) Z μ) (hX : Measurable X) (hY : Measurable Y)
    (hZ : Measurable Z)
    (habs : ∀ x, μ.map Y {x} = 0 → μ.map X {x} = 0) :
    ∀ x, μ.map (Y + Z) {x} = 0 → μ.map (X + Z) {x} = 0

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma absolutelyContinuous_add_of_indep [Finite G] [AddCommGroup G] [DiscreteMeasurableSpace G]    {X Y Z : Ω → G} (h_indep : IndepFun (⟨X, Y⟩) Z μ) (hX : Measurable X) (hY : Measurable Y)    (hZ : Measurable Z)    (habs : ∀ x, μ.map Y {x} = 0 → μ.map X {x} = 0) :    ∀ x, μ.map (Y + Z) {x} = 0 → μ.map (X + Z) {x} = 0 := by  cases nonempty_fintype G  intro x hx  have IX : IndepFun X Z μ := h_indep.comp (φ := Prod.fst) (ψ := id) measurable_fst measurable_id  have IY : IndepFun Y Z μ := h_indep.comp (φ := Prod.snd) (ψ := id) measurable_snd measurable_id  rw [IY.map_add_singleton_eq_sum hY hZ, Finset.sum_eq_zero_iff] at hx  rw [IX.map_add_singleton_eq_sum hX hZ, Finset.sum_eq_zero_iff]  intro i hi  rcases mul_eq_zero.1 (hx i hi) with h'i | h'i  · simp [h'i]  · simp [habs _ h'i]