Integral

📁 Source: Mathlib/Probability/Kernel/Integral.lean

Statistics

Metric	Count
Definitions	0
Theorems integrable, integrable, integral_congr_ae₂, integral_const, integral_deterministic, integral_deterministic', integral_indicator₂, integral_piecewise, integral_restrict, setIntegral_const, setIntegral_deterministic, setIntegral_deterministic', setIntegral_piecewise, setIntegral_restrict	14
Total	14

ProbabilityTheory.Kernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integral_congr_ae₂ 📖	mathematical	Filter.Eventually Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ProbabilityTheory.Kernel instFunLike	MeasureTheory.integral	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.integral_congr_ae Filter.mp_mem Filter.univ_mem'
integral_const 📖	mathematical	—	MeasureTheory.integral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike const	—	const_apply
integral_deterministic 📖	mathematical	Measurable	MeasureTheory.integral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike deterministic	—	deterministic_apply MeasureTheory.integral_dirac
integral_deterministic' 📖	mathematical	Measurable MeasureTheory.StronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	MeasureTheory.integral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike deterministic	—	deterministic_apply MeasureTheory.integral_dirac'
integral_indicator₂ 📖	mathematical	—	MeasureTheory.integral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike Set.indicator NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	Set.indicator_of_mem Set.indicator_of_notMem MeasureTheory.integral_zero
integral_piecewise 📖	mathematical	MeasurableSet	MeasureTheory.integral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike piecewise Set Set.instMembership	—	—
integral_restrict 📖	mathematical	MeasurableSet	MeasureTheory.integral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike restrict MeasureTheory.Measure.restrict	—	restrict_apply
setIntegral_const 📖	mathematical	—	MeasureTheory.integral MeasureTheory.Measure.restrict DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike const	—	const_apply
setIntegral_deterministic 📖	mathematical	Measurable	MeasureTheory.integral MeasureTheory.Measure.restrict DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike deterministic Set Set.instMembership NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	deterministic_apply MeasureTheory.setIntegral_dirac
setIntegral_deterministic' 📖	mathematical	Measurable MeasureTheory.StronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasurableSet	MeasureTheory.integral MeasureTheory.Measure.restrict DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike deterministic Set Set.instMembership NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	deterministic_apply MeasureTheory.setIntegral_dirac'
setIntegral_piecewise 📖	mathematical	MeasurableSet	MeasureTheory.integral MeasureTheory.Measure.restrict DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike piecewise Set Set.instMembership	—	—
setIntegral_restrict 📖	mathematical	MeasurableSet	MeasureTheory.integral MeasureTheory.Measure.restrict DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike restrict Set Set.instInter	—	restrict_apply MeasureTheory.Measure.restrict_restrict'

ProbabilityTheory.Kernel.IsFiniteKernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integrable 📖	mathematical	MeasurableSet	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing MeasureTheory.Measure.real DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike	—	MeasureTheory.Integrable.mono' MeasureTheory.integrable_const Measurable.aestronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace instSecondCountableTopologyReal BorelSpace.opensMeasurable Real.borelSpace Measurable.ennreal_toReal ProbabilityTheory.Kernel.measurable_coe MeasureTheory.ae_of_all MeasureTheory.Measure.instOuterMeasureClass Real.norm_eq_abs abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid MeasureTheory.measureReal_nonneg ENNReal.toReal_mono ProbabilityTheory.Kernel.bound_ne_top ProbabilityTheory.Kernel.measure_le_bound

ProbabilityTheory.Kernel.IsMarkovKernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integrable 📖	mathematical	MeasurableSet	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing MeasureTheory.Measure.real DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike	—	ProbabilityTheory.Kernel.IsFiniteKernel.integrable ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel

---

← Back to Index