Commit 2026-03-06 11:44 c328044d

View on Github →

feat: lemmas about characteristic function (#36251) Characteristic function of a random variable multiplied by a constant. Characteristic function of a sum over a finite set.

Estimated changes

Modified Mathlib/MeasureTheory/Measure/CharacteristicFunction/Basic.lean

added theorem MeasureTheory.charFun_map_mul_comp

added theorem MeasureTheory.charFun_map_smul_comp

Modified Mathlib/Probability/Independence/Basic.lean

Modified Mathlib/Probability/Independence/CharacteristicFunction.lean

modified theorem ProbabilityTheory.charFunDual_map_sum_pi_eq_prod

modified theorem ProbabilityTheory.charFun_map_sum_pi_eq_prod

added theorem ProbabilityTheory.iIndepFun.charFunDual_map_finset_sum_eq_prod

added theorem ProbabilityTheory.iIndepFun.charFunDual_map_fun_finset_sum_eq_prod

modified theorem ProbabilityTheory.iIndepFun.charFunDual_map_fun_sum_eq_prod

modified theorem ProbabilityTheory.iIndepFun.charFunDual_map_sum_eq_prod

added theorem ProbabilityTheory.iIndepFun.charFun_map_finset_sum_eq_prod

added theorem ProbabilityTheory.iIndepFun.charFun_map_fun_finset_sum_eq_prod

modified theorem ProbabilityTheory.iIndepFun.charFun_map_fun_sum_eq_prod

modified theorem ProbabilityTheory.iIndepFun.charFun_map_sum_eq_prod