Theorem ProbabilityTheory.Kernel.IndepFun.comp₀

Modification history

2025-03-23 16:04

Mathlib/Probability/Independence/Kernel.lean

feat: remove measurable assumptions in Azuma-Hoeffding inequality (#23070)

Added ProbabilityTheory.Kernel.IndepFun.comp₀ View on Github →