Commit 2026-03-03 17:42 c08143f5

View on Github →

feat: more versions of the characteristic function of a sum (#36058)

Estimated changes

Modified Mathlib/Probability/Independence/CharacteristicFunction.lean

added theorem ProbabilityTheory.IndepFun.charFunDual_map_fun_add_eq_mul

added theorem ProbabilityTheory.IndepFun.charFun_map_fun_add_eq_mul

added theorem ProbabilityTheory.charFunDual_map_add_prod_eq_mul

added theorem ProbabilityTheory.charFunDual_map_sum_pi_eq_prod

added theorem ProbabilityTheory.charFun_map_add_prod_eq_mul

added theorem ProbabilityTheory.charFun_map_sum_pi_eq_prod

added theorem ProbabilityTheory.iIndepFun.charFunDual_map_fun_sum_eq_prod

added theorem ProbabilityTheory.iIndepFun.charFun_map_fun_sum_eq_prod