Binomial

📁 Source: Mathlib/Probability/Distributions/Binomial.lean

Statistics

Metric	Count
Definitions binomial, «termBin(_,_)»»), «termBin(_,_,_)»»)	3
Theorems ae_le_of_hasLaw_binomial, isProbabilityMeasure_binomial	2
Total	5

ProbabilityTheory

Definitions

Name	Category	Theorems
binomial 📖	CompOp	1 math math: isProbabilityMeasure_binomial
«termBin(_,_)» 📖» "API Documentation")	CompOp	—
«termBin(_,_,_)» 📖» "API Documentation")	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_le_of_hasLaw_binomial 📖	mathematical	HasLaw Nat.instMeasurableSpace binomial	Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.Measure.instOuterMeasureClass HasLaw.ae_iff Measurable.fun_comp measurable_le BorelSpace.opensMeasurable Nat.borelSpace OrderTopology.to_orderClosedTopology OrderTopology.of_linearLocallyFinite instDiscreteTopologyNat PolishSpace.toSecondCountableTopology instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.Countable.to_separableSpace instCountableNat TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable DiscreteUniformity.instCompleteSpace DiscreteUniformity.inst EMetric.instIsCountablyGeneratedUniformity T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace Measurable.prodMk measurable_id' measurable_const binomial.eq_1 MeasureTheory.ae_map_iff Measurable.aemeasurable measurable_ncard Set.Finite.measurableSet Nat.instMeasurableSingletonClass Set.finite_Iic Filter.mp_mem setBernoulli_ae_subset Filter.univ_mem' Set.ncard_Iio_nat Set.ncard_le_ncard Set.toFinite Finite.of_fintype
isProbabilityMeasure_binomial 📖	mathematical	—	MeasureTheory.IsProbabilityMeasure Nat.instMeasurableSpace binomial	—	MeasureTheory.Measure.isProbabilityMeasure_map instIsProbabilityMeasureSetSetBernoulli Measurable.aemeasurable measurable_ncard instCountableNat

---

← Back to Index