Pochhammer

📁 Source: Mathlib/Analysis/SpecialFunctions/Pochhammer.lean

Statistics

Metric	Count
Definitions	0
Theorems continuous_descPochhammer_eval, convexOn_descPochhammer_eval, deriv_descPochhammer_eval_eq_sum_prod_range_erase, descPochhammer_eval_div_factorial_le_sum_choose, descPochhammer_eval_le_sum_descFactorial, differentiable_descPochhammer_eval, monotoneOn_deriv_descPochhammer_eval	7
Total	7

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_descPochhammer_eval 📖	mathematical	—	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Polynomial.eval Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing descPochhammer	—	Differentiable.continuous IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul differentiable_descPochhammer_eval
convexOn_descPochhammer_eval 📖	mathematical	—	ConvexOn Real Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Set.Ici Real.instPreorder Real.instSub Real.instNatCast Real.instOne Polynomial.eval Ring.toSemiring Real.instRing descPochhammer	—	CharP.cast_eq_zero CharP.ofCharZero RCLike.charZero_rclike zero_sub Polynomial.eval_one Real.instIsOrderedAddMonoid IsOrderedModule.toPosSMulMono IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing MonotoneOn.convexOn_of_deriv convex_Ici Continuous.continuousOn continuous_descPochhammer_eval Differentiable.differentiableOn differentiable_descPochhammer_eval interior_Ici instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instNoMinOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial monotoneOn_deriv_descPochhammer_eval
deriv_descPochhammer_eval_eq_sum_prod_range_erase 📖	mathematical	—	deriv NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing Polynomial.eval Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing descPochhammer Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Finset.range Finset.prod CommRing.toCommMonoid Field.toCommRing NormedField.toField Finset.erase SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	descPochhammer_eval_eq_prod_range deriv_fun_finset_prod Finset.sum_congr deriv_fun_sub deriv_id'' deriv_const' sub_zero mul_one
descPochhammer_eval_div_factorial_le_sum_choose 📖	mathematical	Real Real.instLE Real.instZero Finset.sum Real.instAddCommMonoid Real.instOne Real.instSub Real.instNatCast Real.instMul	DivInvMonoid.toDiv Real.instDivInvMonoid Polynomial.eval Ring.toSemiring Real.instRing descPochhammer Nat.factorial Nat.choose	—	Finset.sum_congr Nat.cast_choose_eq_descPochhammer_div RCLike.charZero_rclike mul_div descPochhammer_eval_eq_descFactorial div_le_div_of_nonneg_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing descPochhammer_eval_le_sum_descFactorial Nat.cast_nonneg Real.instIsOrderedRing
descPochhammer_eval_le_sum_descFactorial 📖	mathematical	Real Real.instLE Real.instZero Finset.sum Real.instAddCommMonoid Real.instOne Real.instSub Real.instNatCast Real.instMul	Polynomial.eval Ring.toSemiring Real.instRing descPochhammer Nat.descFactorial	—	ConvexOn.map_sum_le Real.instIsStrictOrderedRing Real.instIsOrderedAddMonoid IsStrictOrderedRing.toIsStrictOrderedModule Finset.sum_congr Set.piecewise_eq_of_mem
differentiable_descPochhammer_eval 📖	mathematical	—	Differentiable NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing Polynomial.eval Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing descPochhammer	—	descPochhammer_eval_eq_prod_range
monotoneOn_deriv_descPochhammer_eval 📖	mathematical	—	MonotoneOn Real Real.instPreorder deriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Polynomial.eval Ring.toSemiring Real.instRing descPochhammer Set.Ioi Real.instSub Real.instNatCast Real.instOne	—	Polynomial.eval_one deriv_const' CharP.cast_eq_zero CharP.ofCharZero RCLike.charZero_rclike zero_sub deriv_descPochhammer_eval_eq_sum_prod_range_erase Finset.sum_le_sum IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Finset.prod_le_prod Real.instZeroLEOneClass IsOrderedRing.toPosMulMono Real.instIsOrderedRing sub_nonneg_of_le covariant_swap_add_of_covariant_add LE.le.trans' LT.lt.le add_sub_cancel_right Nat.cast_add_one Set.mem_Ioi Finset.mem_range Finset.mem_erase sub_le_sub_iff_right

---

← Back to Index