Theorem ConcaveOn.condExp_map_le_of_finiteDimensional

Modification history

2026-03-18 19:14
Mathlib/MeasureTheory/Function/ConditionalExpectation/CondJensen.lean
feat(ProbabilityTheory): Conditional Jensen's Inequality (#27953) …
Added ConcaveOn.condExp_map_le_of_finiteDimensionalView on Github →