Commit 2023-06-14 02:21 635f0d1f

View on Github →

feat: port Probability.Kernel.WithDensity (#5027)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Probability/Kernel/WithDensity.lean

added theorem ProbabilityTheory.kernel.integral_withDensity

added theorem ProbabilityTheory.kernel.isFiniteKernel_withDensity_of_bounded

added theorem ProbabilityTheory.kernel.isSFiniteKernel_withDensity_of_isFiniteKernel

added theorem ProbabilityTheory.kernel.lintegral_withDensity

added theorem ProbabilityTheory.kernel.withDensity_add_left

added theorem ProbabilityTheory.kernel.withDensity_apply'

added theorem ProbabilityTheory.kernel.withDensity_kernel_sum

added theorem ProbabilityTheory.kernel.withDensity_of_not_measurable

added theorem ProbabilityTheory.kernel.withDensity_tsum