Commit 2023-06-09 04:10 4b233234

View on Github →

feat: port Probability.Kernel.Basic (#4879)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Probability/Kernel/Basic.lean

added theorem ProbabilityTheory.IsFiniteKernel.bound_lt_top

added theorem ProbabilityTheory.IsFiniteKernel.bound_ne_top

added theorem ProbabilityTheory.kernel.IsMarkovKernel.comapRight

added theorem ProbabilityTheory.kernel.IsSFiniteKernel.finset_sum

added def ProbabilityTheory.kernel.coeAddHom

added theorem ProbabilityTheory.kernel.coeFn_add

added theorem ProbabilityTheory.kernel.coeFn_zero

added theorem ProbabilityTheory.kernel.coe_finset_sum

added theorem ProbabilityTheory.kernel.comapRight_apply'

added theorem ProbabilityTheory.kernel.comapRight_apply

added def ProbabilityTheory.kernel.const

added theorem ProbabilityTheory.kernel.const_apply

added theorem ProbabilityTheory.kernel.deterministic_apply'

added theorem ProbabilityTheory.kernel.deterministic_apply

added theorem ProbabilityTheory.kernel.ext

added theorem ProbabilityTheory.kernel.ext_fun

added theorem ProbabilityTheory.kernel.ext_fun_iff

added theorem ProbabilityTheory.kernel.ext_iff'

added theorem ProbabilityTheory.kernel.ext_iff

added theorem ProbabilityTheory.kernel.finset_sum_apply'

added theorem ProbabilityTheory.kernel.finset_sum_apply

added theorem ProbabilityTheory.kernel.integral_const

added theorem ProbabilityTheory.kernel.integral_deterministic'

added theorem ProbabilityTheory.kernel.integral_deterministic

added theorem ProbabilityTheory.kernel.integral_piecewise

added theorem ProbabilityTheory.kernel.isSFiniteKernel_sum

added theorem ProbabilityTheory.kernel.isSFiniteKernel_sum_of_denumerable

added theorem ProbabilityTheory.kernel.kernel_sum_seq

added theorem ProbabilityTheory.kernel.lintegral_const

added theorem ProbabilityTheory.kernel.lintegral_deterministic'

added theorem ProbabilityTheory.kernel.lintegral_deterministic

added theorem ProbabilityTheory.kernel.lintegral_piecewise

added theorem ProbabilityTheory.kernel.lintegral_restrict

added theorem ProbabilityTheory.kernel.measure_le_bound

added theorem ProbabilityTheory.kernel.measure_sum_seq

added def ProbabilityTheory.kernel.ofFunOfCountable

added def ProbabilityTheory.kernel.piecewise

added theorem ProbabilityTheory.kernel.piecewise_apply'

added theorem ProbabilityTheory.kernel.piecewise_apply

added theorem ProbabilityTheory.kernel.restrict_apply'

added theorem ProbabilityTheory.kernel.restrict_apply

added theorem ProbabilityTheory.kernel.restrict_univ

added theorem ProbabilityTheory.kernel.set_integral_const

added theorem ProbabilityTheory.kernel.set_integral_deterministic'

added theorem ProbabilityTheory.kernel.set_integral_deterministic

added theorem ProbabilityTheory.kernel.set_integral_piecewise

added theorem ProbabilityTheory.kernel.set_integral_restrict

added theorem ProbabilityTheory.kernel.set_lintegral_const

added theorem ProbabilityTheory.kernel.set_lintegral_deterministic'

added theorem ProbabilityTheory.kernel.set_lintegral_deterministic

added theorem ProbabilityTheory.kernel.set_lintegral_piecewise

added theorem ProbabilityTheory.kernel.set_lintegral_restrict

added theorem ProbabilityTheory.kernel.sum_add

added theorem ProbabilityTheory.kernel.sum_apply'

added theorem ProbabilityTheory.kernel.sum_apply

added theorem ProbabilityTheory.kernel.sum_comm

added theorem ProbabilityTheory.kernel.sum_fintype

added theorem ProbabilityTheory.kernel.sum_zero

added theorem ProbabilityTheory.kernel.zero_apply