Commit 2023-08-14 12:56 886c740a

View on Github →

feat(Probability/Kernel/Condexp): some properties of condexpKernel (#6109) condexpKernel is a Markov kernel, is strongly measurable and is a.e. equal to the conditional expectation.

Estimated changes

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

added theorem MeasureTheory.AEStronglyMeasurable'.mono

Modified Mathlib/MeasureTheory/MeasurableSpace.lean

added theorem measurable_id''

Modified Mathlib/MeasureTheory/Measure/AEMeasurable.lean

added theorem aemeasurable_id''

Modified Mathlib/Probability/Kernel/Condexp.lean

modified theorem MeasureTheory.Integrable.condexpKernel_ae

modified theorem MeasureTheory.Integrable.integral_norm_condexpKernel

deleted theorem ProbabilityTheory.aemeasurable_id''

added theorem ProbabilityTheory.condexpKernel_ae_eq_condexp'

added theorem ProbabilityTheory.condexpKernel_ae_eq_condexp

added theorem ProbabilityTheory.condexpKernel_ae_eq_trim_condexp

added theorem ProbabilityTheory.condexpKernel_apply_eq_condDistrib

added theorem ProbabilityTheory.condexp_ae_eq_integral_condexpKernel'

modified theorem ProbabilityTheory.condexp_ae_eq_integral_condexpKernel

modified theorem ProbabilityTheory.integrable_toReal_condexpKernel

deleted theorem ProbabilityTheory.measurable_id''

added theorem ProbabilityTheory.stronglyMeasurable_condexpKernel