Integrals

📁 Source: Mathlib/Probability/ProbabilityMassFunction/Integrals.lean

Statistics

Metric	Count
Definitions	0
Theorems bernoulli_expectation, integral_eq_sum, integral_eq_tsum	3
Total	3

PMF

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bernoulli_expectation 📖	mathematical	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal instOneNNReal	MeasureTheory.integral Real Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField Bool.instMeasurableSpace toMeasure bernoulli Real.instOne Real.instZero NNReal.toReal	—	integral_eq_sum Bool.instMeasurableSingletonClass Real.instCompleteSpace Finset.sum_congr bernoulli_apply Finset.sum_insert mul_one Finset.sum_singleton MulZeroClass.mul_zero add_zero
integral_eq_sum 📖	mathematical	—	MeasureTheory.integral toMeasure Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Finset.univ Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toModule Real.normedField ENNReal.toReal DFunLike.coe PMF ENNReal instFunLike	—	MeasureTheory.integral_fintype MeasureTheory.Integrable.of_finite Finite.of_fintype MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure toMeasure.isProbabilityMeasure MeasureTheory.measureReal_def toMeasure_apply_singleton MeasurableSet.singleton
integral_eq_tsum 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup toMeasure	MeasureTheory.integral tsum ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toModule Real.normedField ENNReal.toReal DFunLike.coe PMF ENNReal instFunLike SummationFilter.unconditional	—	restrict_toMeasure_support MeasureTheory.integral_countable support_countable MeasureTheory.IntegrableOn.eq_1 toMeasure_apply_singleton MeasurableSet.singleton tsum_subtype_eq_of_support_subset Function.support_smul_subset_left

---

← Back to Index