Defs

📁 Source: Mathlib/Probability/Combinatorics/BinomialRandomGraph/Defs.lean

Statistics

Metric	Count
Definitions binomialRandom, «termG(_,_)»»)	2
Theorems binomialRandom_apply, binomialRandom_apply', binomialRandom_eq_map, binomialRandom_one, binomialRandom_singleton, binomialRandom_zero, instIsProbabilityMeasureBinomialRandom	7
Total	9

SimpleGraph

Definitions

Name	Category	Theorems
binomialRandom 📖	CompOp	7 math math: binomialRandom_apply', binomialRandom_apply, binomialRandom_eq_map, binomialRandom_zero, binomialRandom_singleton, instIsProbabilityMeasureBinomialRandom, binomialRandom_one
«termG(_,_)» 📖» "API Documentation")	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
binomialRandom_apply 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure SimpleGraph instMeasurableSpace Set ENNReal MeasureTheory.Measure.instFunLike binomialRandom MeasurableSpace.pi Sym2 Prop.instMeasurableSpace MeasureTheory.Measure.infinitePi MeasureTheory.Measure.instAdd NNReal MeasureTheory.Measure.instSMul Algebra.toSMul NNReal.instCommSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id IsScalarTower.right unitInterval.toNNReal MeasureTheory.Measure.dirac Sym2.IsDiag unitInterval.symm Set.image Set.instMembership edgeSet	—	IsScalarTower.right binomialRandom_apply' ProbabilityTheory.setBernoulli_apply Set.image_congr
binomialRandom_apply' 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure SimpleGraph instMeasurableSpace Set ENNReal MeasureTheory.Measure.instFunLike binomialRandom Sym2 Set.instMeasurableSpace ProbabilityTheory.setBernoulli Compl.compl Set.instCompl Sym2.diagSet Set.image edgeSet	—	binomialRandom.eq_1 MeasurableEmbedding.comap_apply measurableEmbedding_edgeSet
binomialRandom_eq_map 📖	mathematical	—	binomialRandom MeasureTheory.Measure.map Set Sym2 SimpleGraph Set.instMeasurableSpace instMeasurableSpace fromEdgeSet ProbabilityTheory.setBernoulli Compl.compl Set.instCompl Sym2.diagSet	—	MeasureTheory.Measure.map_eq_comap measurable_fromEdgeSet measurableEmbedding_edgeSet Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.setBernoulli_ae_subset Quotient.countable instCountableProd Filter.univ_mem' edgeSet_fromEdgeSet fromEdgeSet_edgeSet
binomialRandom_one 📖	mathematical	—	binomialRandom Set.Elem Real unitInterval Set.Icc.instOne Real.semiring Real.partialOrder Real.instIsOrderedRing MeasureTheory.Measure.dirac SimpleGraph instMeasurableSpace Top.top BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra completeAtomicBooleanAlgebra	—	Real.instIsOrderedRing binomialRandom_eq_map ProbabilityTheory.setBernoulli_one MeasureTheory.Measure.map_dirac' fromEdgeSet_not_isDiag
binomialRandom_singleton 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure SimpleGraph instMeasurableSpace Set ENNReal MeasureTheory.Measure.instFunLike binomialRandom Set.instSingletonSet Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero ENNReal.ofNNReal unitInterval.toNNReal Set.ncard Sym2 edgeSet unitInterval.symm Nat.choose Nat.card	—	nonempty_fintype MeasurableEmbedding.comap_apply measurableEmbedding_edgeSet Finite.to_countable Set.image_singleton ProbabilityTheory.setBernoulli_singleton Quotient.countable instCountableProd Subtype.finite Quot.finite Finite.instProd Set.ncard_diff Set.toFinite Nat.card_eq_fintype_card Sym2.card_diagSet_compl Fintype.card_eq_nat_card Nat.card_coe_set_eq
binomialRandom_zero 📖	mathematical	—	binomialRandom Set.Elem Real unitInterval Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing MeasureTheory.Measure.dirac SimpleGraph instMeasurableSpace Bot.bot BooleanAlgebra.toBot CompleteBooleanAlgebra.toBooleanAlgebra CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra completeAtomicBooleanAlgebra	—	Real.instIsOrderedRing binomialRandom_eq_map ProbabilityTheory.setBernoulli_zero MeasureTheory.Measure.map_dirac' fromEdgeSet_empty
instIsProbabilityMeasureBinomialRandom 📖	mathematical	—	MeasureTheory.IsProbabilityMeasure SimpleGraph instMeasurableSpace binomialRandom	—	MeasurableEmbedding.isProbabilityMeasure_comap ProbabilityTheory.instIsProbabilityMeasureSetSetBernoulli measurableEmbedding_edgeSet Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.setBernoulli_ae_subset Quotient.countable instCountableProd Filter.univ_mem' edgeSet_fromEdgeSet compl_compl

---

← Back to Index