Commit 2026-07-16 07:28 4a15420c

View on Github →

feat(MeasureTheory): use IsApply for Kernel (#41179)

Estimated changes

Modified Mathlib/Probability/Kernel/Composition/Comp.lean

modified theorem ProbabilityTheory.Kernel.zero_comp

Modified Mathlib/Probability/Kernel/Composition/CompProd.lean

Modified Mathlib/Probability/Kernel/Composition/Lemmas.lean

Modified Mathlib/Probability/Kernel/Composition/MeasureComp.lean

modified theorem MeasureTheory.Measure.add_comp'

Modified Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean

Modified Mathlib/Probability/Kernel/Defs.lean

deleted theorem ProbabilityTheory.Kernel.add_apply

deleted theorem ProbabilityTheory.Kernel.coeAddHom_apply

deleted theorem ProbabilityTheory.Kernel.coe_add

deleted theorem ProbabilityTheory.Kernel.coe_finsetSum

deleted theorem ProbabilityTheory.Kernel.coe_nsmul

deleted theorem ProbabilityTheory.Kernel.coe_zero

deleted theorem ProbabilityTheory.Kernel.finsetSum_apply

deleted theorem ProbabilityTheory.Kernel.nsmul_apply

deleted theorem ProbabilityTheory.Kernel.zero_apply

Modified Mathlib/Probability/Kernel/RadonNikodym.lean

Modified Mathlib/Probability/Kernel/WithDensity.lean

Modified Mathlib/Probability/Moments/SubGaussian.lean