Commit 2025-02-15 20:15 1f0feaaf

View on Github →

feat: properties of condExpKernel and condDistrib (#21906)

Estimated changes

Modified Mathlib/MeasureTheory/Measure/Trim.lean

added theorem MeasureTheory.trim_eq_map

Modified Mathlib/Probability/Kernel/CondDistrib.lean

added theorem MeasureTheory.StronglyMeasurable.integral_condDistrib

added theorem ProbabilityTheory.compProd_map_condDistrib

added theorem ProbabilityTheory.stronglyMeasurable_integral_condDistrib

Modified Mathlib/Probability/Kernel/Condexp.lean

added theorem MeasureTheory.StronglyMeasurable.integral_condExpKernel'

added theorem MeasureTheory.StronglyMeasurable.integral_condExpKernel

added theorem ProbabilityTheory.compProd_trim_condExpKernel

added theorem ProbabilityTheory.condExpKernel_comp_trim