Theorem ProbabilityTheory.iIndepFun.indepFun_prod_range_succ₀

Modification history

2025-03-23 16:04
Mathlib/Probability/Independence/Basic.lean
feat: remove measurable assumptions in Azuma-Hoeffding inequality (#23070)
Added ProbabilityTheory.iIndepFun.indepFun_prod_range_succ₀View on Github →