Commit 2025-01-30 15:46 dc2c5875

View on Github →

feat: conditional variance (#21051) From my PhD (LeanCamCombi)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean

Modified Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean

Created Mathlib/Probability/CondVar.lean

added theorem ProbabilityTheory.condVar_ae_eq_condExp_sq_sub_sq_condExp

added theorem ProbabilityTheory.condVar_ae_le_condExp_sq

added theorem ProbabilityTheory.condVar_bot'

added theorem ProbabilityTheory.condVar_bot

added theorem ProbabilityTheory.condVar_bot_ae_eq

added theorem ProbabilityTheory.condVar_congr_ae

added theorem ProbabilityTheory.condVar_const

added theorem ProbabilityTheory.condVar_neg

added theorem ProbabilityTheory.condVar_of_aestronglyMeasurable

added theorem ProbabilityTheory.condVar_of_not_integrable

added theorem ProbabilityTheory.condVar_of_not_le

added theorem ProbabilityTheory.condVar_of_not_sigmaFinite

added theorem ProbabilityTheory.condVar_of_sigmaFinite

added theorem ProbabilityTheory.condVar_of_stronglyMeasurable

added theorem ProbabilityTheory.condVar_smul

added theorem ProbabilityTheory.condVar_zero

added theorem ProbabilityTheory.integrable_condVar

added theorem ProbabilityTheory.integral_condVar_add_variance_condExp

added theorem ProbabilityTheory.setIntegral_condVar

added theorem ProbabilityTheory.stronglyMeasurable_condVar