Beta

📁 Source: Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean

Statistics

Metric	Count
Definitions GammaSeq, betaIntegral, GammaSeq	3
Theorems GammaSeq_add_one_left, GammaSeq_eq_approx_Gamma_integral, GammaSeq_eq_betaIntegral_of_re_pos, GammaSeq_mul, GammaSeq_tendsto_Gamma, Gamma_eq_zero_iff, Gamma_mul_Gamma_add_half, Gamma_mul_Gamma_eq_betaIntegral, Gamma_mul_Gamma_one_sub, Gamma_ne_zero, Gamma_ne_zero_of_re_pos, approx_Gamma_integral_tendsto_Gamma_integral, betaIntegral_convergent, betaIntegral_convergent_left, betaIntegral_eq_Gamma_mul_div, betaIntegral_eval_nat_add_one_right, betaIntegral_eval_one_right, betaIntegral_recurrence, betaIntegral_scaled, betaIntegral_symm, differentiable_one_div_Gamma, one_div_Gamma_eq_self_mul_one_div_Gamma_add_one, GammaSeq_tendsto_Gamma, Gamma_mul_Gamma_add_half, Gamma_mul_Gamma_one_sub	25
Total	28

Complex

Definitions

Name	Category	Theorems
GammaSeq 📖	CompOp	5 math math: GammaSeq_tendsto_Gamma, GammaSeq_add_one_left, GammaSeq_eq_betaIntegral_of_re_pos, GammaSeq_eq_approx_Gamma_integral, GammaSeq_mul
betaIntegral 📖	CompOp	9 math math: betaIntegral_scaled, betaIntegral_eval_one_right, betaIntegral_recurrence, ProbabilityTheory.beta_eq_betaIntegralReal, Gamma_mul_Gamma_eq_betaIntegral, GammaSeq_eq_betaIntegral_of_re_pos, betaIntegral_eval_nat_add_one_right, betaIntegral_eq_Gamma_mul_div, betaIntegral_symm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
GammaSeq_add_one_left 📖	mathematical	—	Complex DivInvMonoid.toDiv instDivInvMonoid GammaSeq instAdd instOne instMul instNatCast	—	GammaSeq.eq_1 Finset.prod_range_succ div_div Finset.prod_range_succ' Nat.cast_zero add_zero div_mul_div_comm mul_assoc mul_comm cpow_add Nat.cast_ne_zero instCharZero cpow_one Finset.prod_congr Nat.cast_add Nat.cast_one Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.const_add_termg
GammaSeq_eq_approx_Gamma_integral 📖	mathematical	Real Real.instLT Real.instZero re	GammaSeq intervalIntegral Complex instNormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex instMul ofReal Monoid.toNatPow Real.instMonoid Real.instSub Real.instOne DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNatCast instPow instSub instOne MeasureTheory.MeasureSpace.volume Real.measureSpace	—	div_mul_cancel₀ Nat.cast_ne_zero RCLike.charZero_rclike GammaSeq_eq_betaIntegral_of_re_pos intervalIntegral.integral_comp_div betaIntegral.eq_1 real_smul zero_div div_self add_sub_cancel_right intervalIntegral.integral_const_mul intervalIntegral.integral_of_le zero_le_one Real.instZeroLEOneClass MeasureTheory.setIntegral_congr_fun measurableSet_Ioc BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid ofReal_pow ofReal_sub ofReal_mul instCharZero Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr 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.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add cpow_add cpow_one ofReal_natCast mul_cpow_ofReal_nonneg LT.lt.le Nat.cast_pos Real.instIsOrderedRing Real.instNontrivial cpow_natCast Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_atom Mathlib.Tactic.Ring.pow_zero
GammaSeq_eq_betaIntegral_of_re_pos 📖	mathematical	Real Real.instLT Real.instZero re	GammaSeq Complex instMul instPow instNatCast betaIntegral instAdd instOne	—	GammaSeq.eq_1 betaIntegral_eval_nat_add_one_right mul_div_assoc
GammaSeq_mul 📖	mathematical	—	Complex instMul GammaSeq instSub instOne DivInvMonoid.toDiv instDivInvMonoid instNatCast instAdd Finset.prod CommRing.toCommMonoid commRing Finset.range Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring	—	Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul GammaSeq.eq_1 div_mul_div_comm pow_two cpow_add Nat.cast_ne_zero instCharZero add_sub_cancel cpow_one Finset.prod_range_succ' Finset.prod_range_succ Finset.prod_mul_distrib Nat.cast_zero add_zero add_comm add_sub_assoc Nat.cast_add Nat.cast_one Nat.cast_pow Nat.cast_succ 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.subst_add Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst 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.NF.one_eq_eval Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.pow_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg Mathlib.Tactic.FieldSimp.zpow'_ofNat Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_congr 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.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_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.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Finset.prod_congr Nat.cast_prod Finset.prod_pow Finset.prod_range_add_one_eq_factorial div_div mul_div_cancel_right₀ EuclideanDomain.toMulDivCancelClass pow_ne_zero isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass ne_of_gt Nat.factorial_pos mul_comm mul_one_div
GammaSeq_tendsto_Gamma 📖	mathematical	—	Filter.Tendsto Complex GammaSeq Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField Gamma	—	Gamma_eq_GammaAux Nat.cast_zero neg_lt_zero IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid neg_zero Filter.Tendsto.congr' Filter.Eventually.mp Filter.eventually_ne_atTop instNoTopOrderOfNoMaxOrder Nat.instNoMaxOrder Filter.Eventually.of_forall GammaSeq_eq_approx_Gamma_integral approx_Gamma_integral_tendsto_Gamma_integral GammaAux.eq_2 GammaSeq_add_one_left Filter.Tendsto.div_const IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing add_re one_re sub_lt_iff_lt_add IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add sub_eq_add_neg neg_add Nat.cast_succ Filter.tendsto_mul_iff_of_ne_zero IsTopologicalDivisionRing.toContinuousInv₀ T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace add_assoc tendsto_natCast_div_add_atTop instCharZero NNRat.instContinuousSMulOfIsScalarTowerOfRat IsScalarTower.nnrat Rat.instCharZero IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul one_ne_zero' NeZero.charZero_one mul_one mul_comm Real.instIsStrictOrderedRing Gamma_def neg_lt lt_or_ge LT.lt.trans_le neg_neg_of_pos Nat.cast_nonneg Real.instIsOrderedRing Nat.lt_floor_add_one sub_eq_neg_add Nat.floor_add_one neg_nonneg Nat.cast_add_one le_refl
Gamma_eq_zero_iff 📖	mathematical	—	Gamma Complex instZero instNeg instNatCast	—	Mathlib.Tactic.Contrapose.contrapose₁ Gamma_ne_zero Gamma_neg_nat_eq_zero
Gamma_mul_Gamma_add_half 📖	mathematical	—	Complex instMul Gamma instAdd DivInvMonoid.toDiv instDivInvMonoid instOne instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instPow instSub ofReal Real.sqrt Real.pi	—	Nat.instAtLeastTwoHAddOfNat DifferentiableOn.analyticOnNhd instCompleteSpace Differentiable.differentiableOn Differentiable.mul differentiable_one_div_Gamma Differentiable.comp Differentiable.add differentiable_id differentiable_const isOpen_univ Differentiable.const_mul DifferentiableAt.const_cpow DifferentiableAt.sub_const DifferentiableAt.const_mul differentiableAt_id two_ne_zero CharZero.NeZero.two instCharZero tendsto_nhdsWithin_iff tendsto_nhdsWithin_of_tendsto_nhds Continuous.continuousAt continuous_ofReal eventually_nhdsWithin_iff Filter.Eventually.of_forall ofReal_ne_one AnalyticOnNhd.eq_of_frequently_eq PathConnectedSpace.connectedSpace Convex.instPathConnectedSpace instIsRCLikeNormedField Filter.Tendsto.frequently Filter.Eventually.frequently PerfectSpace.not_isolated instPerfectSpace Filter.Eventually.filter_mono nhdsWithin_le_nhds Filter.Eventually.mp eventually_gt_nhds instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike mul_inv Gamma_ofReal one_div ofReal_add ofReal_inv ofReal_mul Real.Gamma_mul_Gamma_add_half_of_pos ofReal_cpow zero_le_two IsOrderedAddMonoid.toAddLeftMono cpow_neg ofReal_sub ofReal_one neg_sub div_eq_mul_inv inv_inv
Gamma_mul_Gamma_eq_betaIntegral 📖	mathematical	Real Real.instLT Real.instZero re	Complex instMul Gamma instAdd betaIntegral	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul IsScalarTower.right Algebra.to_smulCommClass MeasureTheory.integral_posConvolution instCompleteSpace MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume FiniteDimensional.rclike_to_real Real.borelSpace SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace instIsTopologicalAddGroupReal TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal MeasureTheory.IsAddLeftInvariant.isAddRightInvariant MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant Real.noAtoms_volume GammaIntegral_convergent add_re add_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Gamma_eq_integral GammaIntegral.eq_1 MeasureTheory.integral_mul_const MeasureTheory.setIntegral_congr_fun measurableSet_Ioi BorelSpace.opensMeasurable instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal mul_assoc betaIntegral_scaled intervalIntegral.integral_const_mul ofReal_exp ofReal_neg ofReal_sub exp_add Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Abel.const_add_termg Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Abel.zero_termg Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul
Gamma_mul_Gamma_one_sub 📖	mathematical	—	Complex instMul Gamma instSub instOne DivInvMonoid.toDiv instDivInvMonoid ofReal Real.pi sin	—	ofReal_ne_zero Real.pi_ne_zero div_zero mul_comm sin_eq_zero_iff mul_neg sin_neg neg_eq_zero neg_eq_iff_eq_neg LT.lt.ne' Real.pi_pos mul_eq_mul_right_iff IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero instIsDomain Int.cast_natCast Gamma_neg_nat_eq_zero MulZeroClass.zero_mul Int.cast_negSucc neg_neg Nat.cast_add Nat.cast_one add_comm sub_add_cancel_left MulZeroClass.mul_zero tendsto_nhds_unique instT2Space Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Filter.Tendsto.mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing GammaSeq_tendsto_Gamma one_mul Filter.Tendsto.congr' Filter.Eventually.mp Filter.eventually_ne_atTop instNoTopOrderOfNoMaxOrder Nat.instNoMaxOrder Filter.Eventually.of_forall GammaSeq_mul add_sub_assoc tendsto_natCast_div_add_atTop instCharZero NNRat.instContinuousSMulOfIsScalarTowerOfRat IsScalarTower.nnrat Rat.instCharZero IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul IsTopologicalDivisionRing.toContinuousInv₀ one_div inv_div Filter.Tendsto.div tendsto_const_nhds Filter.tendsto_mul_iff_of_ne_zero T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace div_mul_cancel₀ mul_assoc tendsto_euler_sin_prod div_ne_zero
Gamma_ne_zero 📖	—	—	—	—	re_add_im ofReal_zero MulZeroClass.zero_mul add_zero Gamma_ofReal ofReal_ne_zero Real.Gamma_ne_zero Mathlib.Tactic.Contrapose.contrapose₄ ofReal_natCast ofReal_neg sin_ne_zero_iff im_ofReal_mul ofReal_intCast ofReal_mul ofReal_im mul_ne_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass LT.lt.ne' Real.pi_pos div_ne_zero mul_ne_zero_iff Gamma_mul_Gamma_one_sub
Gamma_ne_zero_of_re_pos 📖	—	Real Real.instLT Real.instZero re	—	—	Gamma_ne_zero Mathlib.Tactic.Contrapose.contrapose₃ IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Nat.cast_nonneg Real.instIsOrderedRing
approx_Gamma_integral_tendsto_Gamma_integral 📖	mathematical	Real Real.instLT Real.instZero re	Filter.Tendsto Complex intervalIntegral instNormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex instMul ofReal Monoid.toNatPow Real.instMonoid Real.instSub Real.instOne DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNatCast instPow instSub instOne MeasureTheory.MeasureSpace.volume Real.measureSpace Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField Gamma	—	Gamma_eq_integral MeasureTheory.integrable_indicator_iff measurableSet_Ioc BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid MeasureTheory.IntegrableOn.eq_1 MeasureTheory.Measure.restrict_restrict_of_subset Set.Ioc_subset_Ioi_self intervalIntegrable_iff_integrableOn_Ioc_of_le PseudoEMetricSpace.pseudoMetrizableSpace Nat.cast_nonneg' IsOrderedAddMonoid.toAddLeftMono Real.instZeroLEOneClass IntervalIntegrable.continuousOn_mul intervalIntegral.intervalIntegrable_cpow' sub_re one_re zero_sub sub_lt_sub_iff_right IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add Continuous.continuousOn ofReal_pow ofReal_sub ofReal_div Continuous.pow IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Continuous.comp' continuous_sub_left IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup Continuous.div_const continuous_ofReal Filter.Tendsto.congr' Filter.mp_mem Real.instIsStrictOrderedRing Filter.eventually_ge_atTop Filter.univ_mem' Set.indicator_of_mem Nat.ceil_le mul_comm Filter.Tendsto.const_mul Filter.Tendsto.comp Continuous.tendsto neg_div sub_eq_add_neg Real.tendsto_one_add_div_pow_exp MeasureTheory.integral_indicator intervalIntegral.integral_of_le MeasureTheory.tendsto_integral_of_dominated_convergence Real.GammaIntegral_convergent MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_restrict_iff' measurableSet_Ioi lt_or_ge Set.indicator_of_notMem Set.notMem_Ioc_of_gt norm_zero mul_nonneg_iff_right_nonneg_of_pos IsStrictOrderedRing.toPosMulStrictMono Real.exp_pos Real.rpow_nonneg le_of_lt Set.mem_Ioc Set.mem_Ioi norm_mul NormedDivisionRing.toNormMulClass norm_of_nonneg pow_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing sub_nonneg div_le_one_of_le₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono norm_cpow_eq_rpow_re_of_pos mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Real.one_sub_div_pow_le_exp_neg Real.rpow_pos_of_pos MeasureTheory.ae_of_all
betaIntegral_convergent 📖	mathematical	Real Real.instLT Real.instZero re	IntervalIntegrable Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField NormedAddGroup.toENormedAddMonoid NormedAddCommGroup.toNormedAddGroup instNormedAddCommGroup instMul instPow ofReal instSub instOne MeasureTheory.MeasureSpace.volume Real.measureSpace Real.instOne	—	IntervalIntegrable.trans PseudoEMetricSpace.pseudoMetrizableSpace Nat.instAtLeastTwoHAddOfNat betaIntegral_convergent_left IntervalIntegrable.iff_comp_neg enorm_ne_top mul_comm ofReal_neg ofReal_add Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.atom_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.sub_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.isRat_eq_true Mathlib.Meta.NormNum.isRat_neg Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.isRat_sub zero_sub IntervalIntegrable.symm IntervalIntegrable.comp_add_right
betaIntegral_convergent_left 📖	mathematical	Real Real.instLT Real.instZero re	IntervalIntegrable Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField NormedAddGroup.toENormedAddMonoid NormedAddCommGroup.toNormedAddGroup instNormedAddCommGroup instMul instPow ofReal instSub instOne MeasureTheory.MeasureSpace.volume Real.measureSpace DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	IntervalIntegrable.mul_continuousOn Nat.instAtLeastTwoHAddOfNat intervalIntegral.intervalIntegrable_cpow' sub_re one_re zero_sub sub_lt_sub_iff_right IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid continuousOn_of_forall_continuousAt ContinuousAt.cpow ContinuousAt.sub IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup continuousAt_const Continuous.continuousAt continuous_ofReal Nat.cast_one ofReal_mem_slitPlane lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat 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.mul_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf 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_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.mul_nonpos Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Meta.NormNum.isNat_lt_true RCLike.charZero_rclike CancelDenoms.derive_trans Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_inv_pos CancelDenoms.sub_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNat_mul Set.uIcc_of_le le_of_lt div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial
betaIntegral_eq_Gamma_mul_div 📖	mathematical	Real Real.instLT Real.instZero re	betaIntegral Complex DivInvMonoid.toDiv instDivInvMonoid instMul Gamma instAdd	—	Gamma_mul_Gamma_eq_betaIntegral mul_div_cancel_left₀ EuclideanDomain.toMulDivCancelClass Gamma_ne_zero_of_re_pos add_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
betaIntegral_eval_nat_add_one_right 📖	mathematical	Real Real.instLT Real.instZero re	betaIntegral Complex instAdd instNatCast instOne DivInvMonoid.toDiv instDivInvMonoid Nat.factorial Finset.prod CommRing.toCommMonoid commRing Finset.range	—	Nat.cast_zero zero_add betaIntegral_eval_one_right Nat.factorial_zero Nat.cast_one one_div Finset.prod_congr Finset.prod_singleton CharP.cast_eq_zero CharP.ofCharZero instCharZero add_zero betaIntegral_recurrence ofReal_natCast ofReal_re Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike eq_div_iff Mathlib.Tactic.Contrapose.contrapose₃ zero_re le_refl mul_comm Finset.prod_range_succ' Nat.cast_succ add_re one_re add_pos' Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.factorial_succ Nat.cast_mul Nat.cast_add mul_div_assoc div_div Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.term_add_constg Mathlib.Tactic.Abel.const_add_termg
betaIntegral_eval_one_right 📖	mathematical	Real Real.instLT Real.instZero re	betaIntegral Complex instOne DivInvMonoid.toDiv instDivInvMonoid	—	sub_self cpow_zero mul_one integral_cpow sub_re one_re sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid sub_neg_eq_add sub_add_cancel ofReal_zero ofReal_one one_cpow zero_cpow Mathlib.Tactic.Contrapose.contrapose₃ zero_re le_refl sub_zero
betaIntegral_recurrence 📖	mathematical	Real Real.instLT Real.instZero re	Complex instMul betaIntegral instAdd instOne	—	add_re one_re add_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one ContinuousOn.mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing continuousOn_of_forall_continuousAt ContinuousAt.comp continuousAt_cpow_const_of_re_pos ofReal_re Continuous.continuousAt continuous_ofReal sub_re sub_nonneg covariant_swap_add_of_covariant_add ContinuousAt.sub IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup continuousAt_const IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology ContinuousMul.to_continuousSMul HasDerivAt.cpow_const hasDerivAt_id HasDerivAt.congr_simp mul_one sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd HasDerivAt.const_sub Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.atom_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_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.cast_pos HasDerivAt.comp Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_congr HasDerivAt.comp_ofReal HasDerivAt.mul IntervalIntegrable.sub IntervalIntegrable.const_mul betaIntegral_convergent intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le instCompleteSpace zero_le_one Real.instZeroLEOneClass add_sub_cancel_right sub_zero one_cpow NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass NeZero.charZero_one instCharZero Mathlib.Tactic.Contrapose.contrapose₃ zero_re le_refl sub_self betaIntegral.eq_1 sub_eq_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add intervalIntegral.integral_const_mul intervalIntegral.integral_sub
betaIntegral_scaled 📖	mathematical	Real Real.instLT Real.instZero	intervalIntegral Complex instNormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex instMul instPow ofReal instSub instOne MeasureTheory.MeasureSpace.volume Real.measureSpace instAdd betaIntegral	—	ofReal_ne_zero LT.lt.ne' betaIntegral.eq_1 Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.const_add_termg Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isInt_neg Mathlib.Tactic.Abel.zero_termg cpow_add cpow_one mul_assoc intervalIntegral.integral_const_mul real_smul zero_div div_self intervalIntegral.integral_comp_div intervalIntegral.integral_of_le LT.lt.le MeasureTheory.setIntegral_congr_fun measurableSet_Ioc BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid mul_mul_mul_comm mul_cpow_ofReal_nonneg div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing ofReal_div mul_div_cancel₀ Nat.cast_one sub_nonneg covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono div_le_one ofReal_sub mul_sub mul_one
betaIntegral_symm 📖	mathematical	—	betaIntegral	—	sub_eq_add_neg add_comm mul_comm mul_neg mul_one ofReal_add ofReal_neg neg_add_rev neg_neg add_neg_cancel_comm_assoc inv_neg inv_one neg_zero zero_add add_neg_cancel neg_smul one_smul intervalIntegral.integral_comp_mul_add LT.lt.ne neg_one_lt_zero Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
differentiable_one_div_Gamma 📖	mathematical	—	Differentiable Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField instInv Gamma	—	exists_nat_gt Real.instIsStrictOrderedRing Real.instArchimedean LT.lt.not_ge IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instIsOrderedRing neg_lt_zero IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Nat.cast_zero DifferentiableAt.inv differentiableAt_Gamma Gamma_ne_zero one_div_Gamma_eq_self_mul_one_div_Gamma_add_one DifferentiableAt.mul differentiableAt_id DifferentiableAt.comp add_re one_re neg_add' sub_lt_iff_lt_add IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add Nat.cast_succ DifferentiableAt.add_const
one_div_Gamma_eq_self_mul_one_div_Gamma_add_one 📖	mathematical	—	Complex instInv Gamma instMul instAdd instOne	—	ne_or_eq Gamma_add_one mul_inv mul_inv_cancel_left₀ zero_add Gamma_zero inv_zero MulZeroClass.zero_mul

Real

Definitions

Name	Category	Theorems
GammaSeq 📖	CompOp	1 math math: GammaSeq_tendsto_Gamma

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
GammaSeq_tendsto_Gamma 📖	mathematical	—	Filter.Tendsto Real GammaSeq Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace Gamma	—	Complex.ofReal_div Complex.ofReal_mul Complex.ofReal_prod Finset.prod_congr Complex.ofReal_add Complex.ofReal_cpow Nat.cast_nonneg instIsOrderedRing Complex.ofReal_natCast Complex.GammaSeq_tendsto_Gamma Filter.Tendsto.comp Continuous.tendsto Complex.continuous_re
Gamma_mul_Gamma_add_half 📖	mathematical	—	Real instMul Gamma instAdd DivInvMonoid.toDiv instDivInvMonoid instOne instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instPow instSub sqrt pi	—	Nat.instAtLeastTwoHAddOfNat Complex.ofReal_mul Complex.ofReal_add Complex.ofReal_div Complex.ofReal_cpow zero_le_two instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid Complex.ofReal_sub Complex.Gamma_mul_Gamma_add_half
Gamma_mul_Gamma_one_sub 📖	mathematical	—	Real instMul Gamma instSub instOne DivInvMonoid.toDiv instDivInvMonoid pi sin	—	Complex.ofReal_div Complex.ofReal_sin Complex.ofReal_mul Complex.ofReal_sub Complex.Gamma_mul_Gamma_one_sub

---

← Back to Index