Beta

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

Statistics

Metric	Count
Definitions beta, betaMeasure, betaPDF, betaPDFReal	4
Theorems betaPDFReal_pos, betaPDF_eq, betaPDF_eq_zero_of_nonpos, betaPDF_eq_zero_of_one_le, betaPDF_of_pos_lt_one, beta_eq_betaIntegralReal, beta_pos, isProbabilityMeasureBeta, lintegral_betaPDF, lintegral_betaPDF_eq_one, measurable_betaPDFReal, stronglyMeasurable_betaPDFReal	12
Total	16

ProbabilityTheory

Definitions

Name	Category	Theorems
beta 📖	CompOp	5 math math: betaPDF_eq, betaPDF_of_pos_lt_one, beta_eq_betaIntegralReal, lintegral_betaPDF, beta_pos
betaMeasure 📖	CompOp	1 math math: isProbabilityMeasureBeta
betaPDF 📖	CompOp	6 math math: betaPDF_eq, betaPDF_eq_zero_of_nonpos, betaPDF_of_pos_lt_one, lintegral_betaPDF_eq_one, lintegral_betaPDF, betaPDF_eq_zero_of_one_le
betaPDFReal 📖	CompOp	3 math math: betaPDFReal_pos, stronglyMeasurable_betaPDFReal, measurable_betaPDFReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
betaPDFReal_pos 📖	mathematical	Real Real.instLT Real.instZero Real.instOne	betaPDFReal	—	betaPDFReal.eq_1 mul_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing one_div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE beta_pos Real.rpow_pos_of_pos lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le
betaPDF_eq 📖	mathematical	—	betaPDF ENNReal.ofReal Real Real.instLT Real.instZero Real.instOne Real.decidableLT Real.instMul DivInvMonoid.toDiv Real.instDivInvMonoid beta Real.instPow Real.instSub	—	—
betaPDF_eq_zero_of_nonpos 📖	mathematical	Real Real.instLE Real.instZero	betaPDF ENNReal instZeroENNReal	—	LE.le.not_gt ENNReal.ofReal_zero
betaPDF_eq_zero_of_one_le 📖	mathematical	Real Real.instLE Real.instOne	betaPDF ENNReal instZeroENNReal	—	LE.le.not_gt ENNReal.ofReal_zero
betaPDF_of_pos_lt_one 📖	mathematical	Real Real.instLT Real.instZero Real.instOne	betaPDF ENNReal.ofReal Real.instMul DivInvMonoid.toDiv Real.instDivInvMonoid beta Real.instPow Real.instSub	—	betaPDF_eq
beta_eq_betaIntegralReal 📖	mathematical	Real Real.instLT Real.instZero	beta Complex.re Complex.betaIntegral Complex.ofReal	—	Complex.betaIntegral_eq_Gamma_mul_div Complex.ofReal_add Complex.Gamma_ofReal
beta_pos 📖	mathematical	Real Real.instLT Real.instZero	beta	—	div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing mul_pos Real.Gamma_pos_of_pos add_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
isProbabilityMeasureBeta 📖	mathematical	Real Real.instLT Real.instZero	MeasureTheory.IsProbabilityMeasure Real.measurableSpace betaMeasure	—	MeasureTheory.withDensity_apply MeasureTheory.Measure.restrict_univ lintegral_betaPDF_eq_one
lintegral_betaPDF 📖	mathematical	—	MeasureTheory.lintegral Real MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.MeasureSpace.volume betaPDF MeasureTheory.Measure.restrict Set.Ioo Real.instPreorder Real.instZero Real.instOne ENNReal.ofReal Real.instMul DivInvMonoid.toDiv Real.instDivInvMonoid beta Real.instPow Real.instSub	—	MeasureTheory.lintegral_add_compl measurableSet_Iic BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid MeasureTheory.setLIntegral_eq_zero betaPDF_eq_zero_of_nonpos zero_add Set.compl_Iic measurableSet_Ici instClosedIciTopology betaPDF_eq_zero_of_one_le Set.compl_Ici MeasureTheory.Measure.restrict_restrict measurableSet_Iio Set.Iio_inter_Ioi MeasureTheory.setLIntegral_congr_fun measurableSet_Ioo betaPDF_of_pos_lt_one
lintegral_betaPDF_eq_one 📖	mathematical	Real Real.instLT Real.instZero	MeasureTheory.lintegral MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.MeasureSpace.volume betaPDF ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	lintegral_betaPDF ENNReal.toReal_eq_one_iff MeasureTheory.integral_eq_lintegral_of_nonneg_ae MeasureTheory.ae_restrict_of_forall_mem measurableSet_Ioo BorelSpace.opensMeasurable Real.borelSpace HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid betaPDFReal.eq_1 LT.lt.le betaPDFReal_pos Measurable.aestronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace instSecondCountableTopologyReal Measurable.mul ContinuousMul.measurableMul₂ IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Measurable.const_mul ContinuousMul.measurableMul Measurable.pow_const Real.hasMeasurablePow measurable_id' Measurable.const_sub ContinuousSub.measurableSub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal mul_assoc MeasureTheory.integral_const_mul Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div' div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst one_ne_zero NeZero.one GroupWithZero.toNontrivial div_eq_one_iff_eq ne_of_gt beta_pos beta_eq_betaIntegralReal Complex.betaIntegral.eq_1 intervalIntegral.integral_of_le Mathlib.Meta.NormNum.isNat_le_true Real.instIsOrderedRing Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Nat.cast_one MeasureTheory.integral_Ioc_eq_integral_Ioo Real.noAtoms_volume RCLike.re_to_complex integral_re intervalIntegrable_iff_integrableOn_Ioc_of_le Real.instZeroLEOneClass MeasureTheory.IntegrableOn.eq_1 Complex.betaIntegral_convergent MeasureTheory.setIntegral_congr_fun measurableSet_Ioc instClosedIicTopology Complex.ofReal_cpow le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.sub_nonpos_of_le Complex.re_mul_ofReal Complex.ofReal_re
measurable_betaPDFReal 📖	mathematical	—	Measurable Real Real.measurableSpace betaPDFReal	—	Measurable.ite measurableSet_Ioo BorelSpace.opensMeasurable Real.borelSpace HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Measurable.mul ContinuousMul.measurableMul₂ instSecondCountableTopologyReal IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Measurable.const_mul ContinuousMul.measurableMul Measurable.pow_const Real.hasMeasurablePow measurable_id' Measurable.const_sub ContinuousSub.measurableSub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal measurable_const
stronglyMeasurable_betaPDFReal 📖	mathematical	—	MeasureTheory.StronglyMeasurable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.measurableSpace betaPDFReal	—	Measurable.stronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace instSecondCountableTopologyReal BorelSpace.opensMeasurable Real.borelSpace measurable_betaPDFReal

---

← Back to Index