Gamma

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

Statistics

Metric	Count
Definitions Gamma, Gamma, gammaCDFReal, gammaMeasure, gammaPDF, gammaPDFReal, Gamma	7
Theorems Gamma, Gamma, Gamma, cdf_gammaMeasure_eq_integral, cdf_gammaMeasure_eq_lintegral, gammaCDFReal_eq_integral, gammaCDFReal_eq_lintegral, gammaPDFReal_nonneg, gammaPDFReal_pos, gammaPDF_eq, gammaPDF_of_neg, gammaPDF_of_nonneg, isProbabilityMeasureGamma, isProbabilityMeasure_gammaMeasure, lintegral_gammaPDF_eq_one, lintegral_gammaPDF_of_nonpos, measurable_gammaPDFReal, stronglyMeasurable_gammaPDFReal, lintegral_Iic_eq_lintegral_Iio_add_Icc	19
Total	26

Complex

Definitions

Name	Category	Theorems
Gamma 📖	CompOp	55 math math: completedZeta_eq_tsum_of_one_lt_re, Gammaℝ_def, Gamma_neg_nat_eq_zero, Gamma_nat_eq_factorial, GammaSeq_tendsto_Gamma, ZMod.LFunction_one_sub, Gamma_add_one, not_differentiableAt_Gamma_neg_nat, Gamma_one, one_div_Gamma_eq_self_mul_one_div_Gamma_add_one, riemannZeta_one_sub, deriv_Gamma_add_one, HurwitzZeta.expZeta_one_sub, hasSum_mellin, Gamma_conj, HurwitzZeta.cosZeta_one_sub, deriv_Gamma_nat, continuousAt_Gamma_one, tendsto_self_mul_Gamma_nhds_zero, not_continuousAt_Gamma_zero, HurwitzZeta.hurwitzZetaEven_one_sub, hasSum_mellin_pi_mul, Gamma_eq_GammaAux, MeromorphicNFOn.Gamma, Gammaℂ_def, digamma_def, Gamma_mul_Gamma_eq_betaIntegral, hasSum_mellin_pi_mul₀, differentiable_one_div_Gamma, not_differentiableAt_Gamma_zero, differentiableAt_Gamma_nat_add_one, HurwitzZeta.hurwitzZeta_one_sub, not_continuousAt_Gamma_neg_nat, differentiableAt_Gamma_one, hasDerivAt_Gamma_one, Gamma_eq_integral, hasDerivAt_Gamma_one_half, Gamma_mul_Gamma_add_half, differentiableAt_Gamma, Gamma_mul_Gamma_one_sub, continuousAt_Gamma, Gamma_def, Gamma_ofNat_eq_factorial, Meromorphic.Gamma, HurwitzZeta.hurwitzZetaOdd_one_sub, Gamma_eq_zero_iff, betaIntegral_eq_Gamma_mul_div, MeromorphicOn.Gamma, integral_cpow_mul_exp_neg_mul_Ioi, HurwitzZeta.sinZeta_one_sub, Gamma_zero, approx_Gamma_integral_tendsto_Gamma_integral, Gamma_ofReal, Gamma_one_half_eq, hasDerivAt_Gamma_nat

CongruenceSubgroup

Definitions

Name	Category	Theorems
Gamma 📖	CompOp	28 math math: Gamma_zero_bot, Gamma_mem', instFiniteIndexGamma, exists_Gamma_le_conj', mem_Gamma_one, Gamma_normal, ModularForm.levelOne_neg_weight_rank_zero, exists_Gamma_le_conj, Gamma_one_top, ModularFormClass.one_mem_strictPeriods_SL2Z, ModularForm.levelOne_weight_zero_rank_one, Gamma_cong_eq_self, EisensteinSeries.q_expansion_riemannZeta, EisensteinSeries.isBoundedAtImInfty_eisensteinSeries_SIF, EisensteinSeries.eisensteinSeries_SIF_apply, ModularGroup_T_pow_mem_Gamma, Gamma_is_cong_sub, strictWidthInfty_Gamma, EisensteinSeries.q_expansion_bernoulli, strictPeriods_Gamma, SlashInvariantForm.vAdd_width_periodic, EisensteinSeries.eisensteinSeriesSIF_apply, EisensteinSeries.eisensteinSeries_tendstoLocallyUniformlyOn, EisensteinSeries.eisensteinSeries_SIF_MDifferentiable, Gamma_mem, EisensteinSeries.eisensteinSeriesSIF_mdifferentiable, SlashInvariantForm.T_zpow_width_invariant, EisensteinSeries.isBoundedAtImInfty_eisensteinSeriesSIF

Meromorphic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Gamma 📖	mathematical	—	Meromorphic Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Complex.Gamma	—	meromorphicOn_univ MeromorphicNFOn.meromorphicOn MeromorphicNFOn.Gamma

MeromorphicNFOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Gamma 📖	mathematical	—	MeromorphicNFOn Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Complex.Gamma Set.univ	—	meromorphicNFOn_inv AnalyticOnNhd.meromorphicNFOn Complex.analyticOnNhd_univ_iff_differentiable Complex.instCompleteSpace Complex.differentiable_one_div_Gamma

MeromorphicOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Gamma 📖	mathematical	—	MeromorphicOn Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Complex.Gamma	—	Meromorphic.meromorphicOn Meromorphic.Gamma

ProbabilityTheory

Definitions

Name	Category	Theorems
gammaCDFReal 📖	CompOp	—
gammaMeasure 📖	CompOp	6 math math: gammaCDFReal_eq_lintegral, gammaCDFReal_eq_integral, isProbabilityMeasure_gammaMeasure, cdf_gammaMeasure_eq_lintegral, isProbabilityMeasureGamma, cdf_gammaMeasure_eq_integral
gammaPDF 📖	CompOp	7 math math: gammaPDF_of_nonneg, gammaCDFReal_eq_lintegral, lintegral_gammaPDF_of_nonpos, cdf_gammaMeasure_eq_lintegral, gammaPDF_of_neg, gammaPDF_eq, lintegral_gammaPDF_eq_one
gammaPDFReal 📖	CompOp	6 math math: gammaPDFReal_nonneg, gammaCDFReal_eq_integral, measurable_gammaPDFReal, gammaPDFReal_pos, stronglyMeasurable_gammaPDFReal, cdf_gammaMeasure_eq_integral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cdf_gammaMeasure_eq_integral 📖	mathematical	Real Real.instLT Real.instZero	StieltjesFunction.toFun Real.linearOrder UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace cdf gammaMeasure MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.Iic Real.instPreorder gammaPDFReal	—	isProbabilityMeasure_gammaMeasure cdf_eq_real gammaMeasure.eq_1 MeasureTheory.measureReal_def MeasureTheory.withDensity_apply measurableSet_Iic BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid MeasureTheory.integral_eq_lintegral_of_nonneg_ae MeasureTheory.ae_of_all MeasureTheory.Measure.instOuterMeasureClass gammaPDFReal_nonneg MeasureTheory.StronglyMeasurable.aestronglyMeasurable stronglyMeasurable_gammaPDFReal
cdf_gammaMeasure_eq_lintegral 📖	mathematical	Real Real.instLT Real.instZero	StieltjesFunction.toFun Real.linearOrder UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace cdf gammaMeasure ENNReal.toReal MeasureTheory.lintegral MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.Iic Real.instPreorder gammaPDF	—	isProbabilityMeasure_gammaMeasure cdf_eq_real MeasureTheory.withDensity_apply BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid
gammaCDFReal_eq_integral 📖	mathematical	Real Real.instLT Real.instZero	StieltjesFunction.toFun Real.linearOrder UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace cdf gammaMeasure MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.Iic Real.instPreorder gammaPDFReal	—	cdf_gammaMeasure_eq_integral
gammaCDFReal_eq_lintegral 📖	mathematical	Real Real.instLT Real.instZero	StieltjesFunction.toFun Real.linearOrder UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace cdf gammaMeasure ENNReal.toReal MeasureTheory.lintegral MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.Iic Real.instPreorder gammaPDF	—	cdf_gammaMeasure_eq_lintegral
gammaPDFReal_nonneg 📖	mathematical	Real Real.instLT Real.instZero	Real.instLE gammaPDFReal	—	mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing le_of_lt div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.rpow_pos_of_pos Real.Gamma_pos_of_pos Real.rpow_nonneg Real.exp_pos Mathlib.Meta.Positivity.nonneg_of_isNat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero
gammaPDFReal_pos 📖	mathematical	Real Real.instLT Real.instZero	gammaPDFReal	—	LT.lt.le mul_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE Real.rpow_pos_of_pos Real.Gamma_pos_of_pos Real.exp_pos
gammaPDF_eq 📖	mathematical	—	gammaPDF ENNReal.ofReal Real Real.instLE Real.instZero Real.decidableLE Real.instMul DivInvMonoid.toDiv Real.instDivInvMonoid Real.instPow Real.Gamma Real.instSub Real.instOne Real.exp Real.instNeg	—	—
gammaPDF_of_neg 📖	mathematical	Real Real.instLT Real.instZero	gammaPDF ENNReal instZeroENNReal	—	not_le ENNReal.ofReal_zero
gammaPDF_of_nonneg 📖	mathematical	Real Real.instLE Real.instZero	gammaPDF ENNReal.ofReal Real.instMul DivInvMonoid.toDiv Real.instDivInvMonoid Real.instPow Real.Gamma Real.instSub Real.instOne Real.exp Real.instNeg	—	—
isProbabilityMeasureGamma 📖	mathematical	Real Real.instLT Real.instZero	MeasureTheory.IsProbabilityMeasure Real.measurableSpace gammaMeasure	—	isProbabilityMeasure_gammaMeasure
isProbabilityMeasure_gammaMeasure 📖	mathematical	Real Real.instLT Real.instZero	MeasureTheory.IsProbabilityMeasure Real.measurableSpace gammaMeasure	—	MeasureTheory.withDensity_apply MeasureTheory.Measure.restrict_univ lintegral_gammaPDF_eq_one
lintegral_gammaPDF_eq_one 📖	mathematical	Real Real.instLT Real.instZero	MeasureTheory.lintegral MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.MeasureSpace.volume gammaPDF ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	MeasureTheory.setLIntegral_congr_fun measurableSet_Iio BorelSpace.opensMeasurable Real.borelSpace instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid gammaPDF_of_neg MeasureTheory.lintegral_zero measurableSet_Ici gammaPDF_of_nonneg ENNReal.toReal_eq_one_iff MeasureTheory.lintegral_add_compl Set.compl_Ici add_zero MeasureTheory.integral_eq_lintegral_of_nonneg_ae MeasureTheory.Measure.instOuterMeasureClass Filter.EventuallyLE.eq_1 MeasureTheory.ae_restrict_iff' MeasureTheory.ae_of_all mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing le_of_lt div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.rpow_pos_of_pos Real.Gamma_pos_of_pos Real.rpow_nonneg Real.exp_pos MeasureTheory.AEStronglyMeasurable.congr Measurable.aestronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace instSecondCountableTopologyReal measurable_gammaPDFReal eq_true_intro MeasureTheory.integral_Ici_eq_integral_Ioi Real.noAtoms_volume mul_assoc MeasureTheory.integral_const_mul Real.integral_rpow_mul_exp_neg_mul_Ioi div_mul_eq_mul_div mul_div_assoc div_self LT.lt.ne' mul_one Real.div_rpow zero_le_one Real.instZeroLEOneClass LT.lt.le Real.one_rpow mul_one_div
lintegral_gammaPDF_of_nonpos 📖	mathematical	Real Real.instLE Real.instZero	MeasureTheory.lintegral MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.Iio Real.instPreorder gammaPDF ENNReal instZeroENNReal	—	MeasureTheory.setLIntegral_congr_fun measurableSet_Iio BorelSpace.opensMeasurable Real.borelSpace instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid 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_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_zero 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.add_pf_add_gt 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.Ring.add_pf_zero_add Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.sub_nonpos_of_le Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt le_refl MeasureTheory.lintegral_zero ENNReal.ofReal_zero
measurable_gammaPDFReal 📖	mathematical	—	Measurable Real Real.measurableSpace gammaPDFReal	—	Measurable.ite measurableSet_Ici BorelSpace.opensMeasurable Real.borelSpace instClosedIciTopology 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.exp Measurable.neg ContinuousNeg.measurableNeg IsTopologicalRing.toContinuousNeg measurable_const
stronglyMeasurable_gammaPDFReal 📖	mathematical	—	MeasureTheory.StronglyMeasurable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.measurableSpace gammaPDFReal	—	Measurable.stronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace instSecondCountableTopologyReal BorelSpace.opensMeasurable Real.borelSpace measurable_gammaPDFReal

Real

Definitions

Name	Category	Theorems
Gamma 📖	CompOp	60 math math: ProbabilityTheory.gammaPDF_of_nonneg, Gamma_pos_of_pos, Gamma_nat_add_half, Gamma_nonneg_of_nonneg, Gamma_strictAntiOn_Ioc, integral_exp_neg_mul_rpow, Complex.integral_rpow_mul_exp_neg_rpow, Complex.volume_sum_rpow_le, integral_rpow_mul_exp_neg_rpow, MeasureTheory.measure_lt_one_eq_integral_div_gamma, Gamma_two, Gamma_mul_Gamma_add_half, doublingGamma_eq_Gamma, Gamma_mul_Gamma_one_sub, Gamma_one, GammaSeq_tendsto_Gamma, Gamma_one_half_eq, Complex.integral_exp_neg_rpow, exists_isMinOn_Gamma_Ioi, MeasureTheory.volume_sum_rpow_lt, deriv_Gamma_nat, Gamma_strictMonoOn_Ici, Gamma_mul_add_mul_le_rpow_Gamma_mul_rpow_Gamma, Gamma_eq_zero_iff, MeasureTheory.volume_sum_rpow_le, integral_rpow_mul_exp_neg_mul_rpow, differentiableAt_Gamma, differentiableOn_Gamma_Ioi, InnerProductSpace.volume_ball, convexOn_log_Gamma, Gamma_add_one, Complex.integral_exp_neg_mul_rpow, convexOn_Gamma, Gamma_nat_add_one_add_half, Complex.volume_sum_rpow_lt, integral_exp_neg_rpow, Gamma_ofNat_eq_factorial, eulerMascheroniConstant_eq_neg_deriv, Gamma_eq_integral, Gamma_zero, hasDerivAt_Gamma_one_half, Gamma_mul_Gamma_add_half_of_pos, EuclideanSpace.volume_ball, hasDerivAt_Gamma_one, ProbabilityTheory.gammaPDF_eq, Complex.integral_rpow_mul_exp_neg_mul_rpow, integral_rpow_mul_exp_neg_mul_Ioi, InnerProductSpace.volume_closedBall, Complex.volume_sum_rpow_lt_one, Gamma_nat_eq_factorial, hasDerivAt_Gamma_nat, MeasureTheory.measure_unitBall_eq_integral_div_gamma, Gamma_neg_nat_eq_zero, Gamma_three_div_two_lt_one, Complex.Gamma_ofReal, EuclideanSpace.volume_closedBall, MeasureTheory.volume_sum_rpow_lt_one, eq_Gamma_of_log_convex, log_doublingGamma_eq, BohrMollerup.tendsto_log_gamma

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lintegral_Iic_eq_lintegral_Iio_add_Icc 📖	mathematical	Real Real.instLE	MeasureTheory.lintegral MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.Iic Real.instPreorder ENNReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Set.Iio Set.Icc	—	Set.Iio_union_Icc_eq_Iic MeasureTheory.lintegral_union measurableSet_Icc BorelSpace.opensMeasurable Real.borelSpace HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid 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.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_add_lt Mathlib.Tactic.Ring.add_pf_zero_add 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.Ring.neg_congr Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Linarith.lt_of_lt_of_eq Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le neg_eq_zero sub_eq_zero_of_eq

---

← Back to Index