Deriv

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

Statistics

Metric	Count
Definitions	0
Theorems GammaIntegral_eq_mellin, continuousAt_Gamma, continuousAt_Gamma_one, deriv_Gamma_add_one, differentiableAt_Gamma, differentiableAt_GammaAux, differentiableAt_Gamma_one, hasDerivAt_GammaIntegral, not_continuousAt_Gamma_neg_nat, not_continuousAt_Gamma_zero, not_differentiableAt_Gamma_neg_nat, not_differentiableAt_Gamma_zero, tendsto_self_mul_Gamma_nhds_zero, differentiableAt_Gamma, differentiableOn_Gamma_Ioi	15
Total	15

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
GammaIntegral_eq_mellin 📖	mathematical	—	GammaIntegral mellin Complex instNormedAddCommGroup InnerProductSpace.toNormedSpace instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace ofReal Real.exp Real Real.instNeg	—	mul_comm
continuousAt_Gamma 📖	mathematical	—	ContinuousAt Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField Gamma	—	DifferentiableAt.continuousAt IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology differentiableAt_Gamma
continuousAt_Gamma_one 📖	mathematical	—	ContinuousAt Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField Gamma instOne	—	DifferentiableAt.continuousAt IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology differentiableAt_Gamma_one
deriv_Gamma_add_one 📖	mathematical	—	deriv Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField Gamma instAdd instOne instMul	—	sub_neg_eq_add neg_sub' Nat.cast_one Nat.cast_sub Nat.cast_ne_zero instCharZero neg_ne_zero deriv_zero_of_not_differentiableAt not_differentiableAt_Gamma_neg_nat Gamma_neg_nat_eq_zero zero_add MulZeroClass.mul_zero IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing HasDerivWithinAt.congr IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul HasDerivWithinAt.congr_simp one_mul HasDerivWithinAt.mul hasDerivWithinAt_id HasDerivAt.hasDerivWithinAt DifferentiableAt.hasDerivAt differentiableAt_Gamma Gamma_add_one deriv_comp_add_const HasDerivAt.deriv HasDerivWithinAt.hasDerivAt compl_singleton_mem_nhds T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace
differentiableAt_Gamma 📖	mathematical	—	DifferentiableAt Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField Gamma	—	Real.instIsStrictOrderedRing Nat.cast_one Nat.lt_floor_add_one DifferentiableAt.congr_of_eventuallyEq differentiableAt_GammaAux mem_nhds_iff Set.Subset.rfl Set.ext Set.preimage.eq_1 Set.Ioi.eq_1 Set.mem_setOf_eq sub_lt_comm IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Continuous.isOpen_preimage continuous_re isOpen_Ioi instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Filter.eventuallyEq_of_mem Gamma_eq_GammaAux lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl 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.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.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.add_neg neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le
differentiableAt_GammaAux 📖	mathematical	Real Real.instLT Real.instSub Real.instOne re Real.instNatCast	DifferentiableAt Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField GammaAux	—	HasDerivAt.differentiableAt hasDerivAt_GammaIntegral lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl 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 Nat.cast_one 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.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_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 Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.add_neg neg_neg_of_pos Real.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le add_re one_re Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Meta.NormNum.IsNat.to_raw_eq Nat.cast_succ Mathlib.Tactic.Contrapose.contrapose₄ Nat.cast_add neg_add_rev eq_sub_iff_add_eq DifferentiableAt.div DifferentiableAt.comp differentiableAt_add_const_iff differentiableAt_id CharP.cast_eq_zero CharP.ofCharZero instCharZero neg_zero
differentiableAt_Gamma_one 📖	mathematical	—	DifferentiableAt Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField Gamma instOne	—	differentiableAt_Gamma Nat.cast_one Int.cast_one instCharZero Int.instIsStrictOrderedRing
hasDerivAt_GammaIntegral 📖	mathematical	Real Real.instLT Real.instZero re	HasDerivAt Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField IsModuleTopology.toContinuousSMul NontriviallyNormedField.toNormedField instAdd SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid IsTopologicalSemiring.toIsModuleTopology instSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing GammaIntegral MeasureTheory.integral instNormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.Ioi Real.instPreorder instMul instPow ofReal instSub instOne Real.log Real.exp Real.instNeg	—	IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing GammaIntegral_eq_mellin IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul mellin_hasDerivAt_of_isBigO_rpow ContinuousOn.locallyIntegrableOn BorelSpace.opensMeasurable Real.borelSpace Real.locallyFinite_volume secondCountableTopologyEither_of_right UniformSpace.secondCountable_of_separable EMetric.instIsCountablyGeneratedUniformity TopologicalSpace.SecondCountableTopology.to_separableSpace secondCountable_of_proper instProperSpace Continuous.continuousOn Continuous.comp continuous_ofReal Real.continuous_exp ContinuousNeg.continuous_neg IsTopologicalRing.toContinuousNeg instIsTopologicalRingReal measurableSet_Ioi instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Asymptotics.isBigO_norm_left norm_real neg_one_mul Asymptotics.IsLittleO.isBigO isLittleO_exp_neg_mul_rpow_atTop zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike lt_add_one IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono neg_zero Real.rpow_zero Asymptotics.isBigO_const_of_tendsto Real.exp_zero Continuous.continuousWithinAt one_ne_zero
not_continuousAt_Gamma_neg_nat 📖	mathematical	—	ContinuousAt Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField Gamma instNeg instNatCast	—	Nat.cast_zero neg_zero not_continuousAt_Gamma_zero Mathlib.Tactic.Contrapose.contrapose₄ neg_add' neg_ne_zero Nat.cast_add_one_ne_zero instCharZero ContinuousWithinAt.continuousAt ContinuousWithinAt.congr ContinuousAt.continuousWithinAt ContinuousAt.mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing continuousAt_id Nat.cast_one Nat.cast_add Gamma_add_one compl_singleton_mem_nhds T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace ContinuousAt.comp' Continuous.continuousAt continuous_sub_right IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup sub_add_cancel
not_continuousAt_Gamma_zero 📖	mathematical	—	ContinuousAt Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField Gamma instZero	—	Filter.Tendsto.not_tendsto tendsto_self_mul_Gamma_nhds_zero PerfectSpace.not_isolated instPerfectSpace Gamma_zero MulZeroClass.mul_zero instT2Space NeZero.charZero_one instCharZero continuousAt_iff_punctured_nhds ContinuousAt.mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing continuousAt_id
not_differentiableAt_Gamma_neg_nat 📖	mathematical	—	DifferentiableAt Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField Gamma instNeg instNatCast	—	DifferentiableAt.continuousAt IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology not_continuousAt_Gamma_neg_nat
not_differentiableAt_Gamma_zero 📖	mathematical	—	DifferentiableAt Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField Gamma instZero	—	DifferentiableAt.continuousAt IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology not_continuousAt_Gamma_zero
tendsto_self_mul_Gamma_nhds_zero 📖	mathematical	—	Filter.Tendsto Complex instMul Gamma nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField instZero Compl.compl Set Set.instCompl Set.instSingletonSet nhds instOne	—	zero_add Gamma_one tendsto_nhdsWithin_congr Gamma_add_one continuousAt_iff_punctured_nhds ContinuousAt.comp' Continuous.continuousAt continuous_add_right IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
differentiableAt_Gamma 📖	mathematical	—	DifferentiableAt Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing InnerProductSpace.toNormedSpace instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace Gamma	—	HasDerivAt.differentiableAt HasDerivAt.real_of_complex DifferentiableAt.hasDerivAt Complex.differentiableAt_Gamma
differentiableOn_Gamma_Ioi 📖	mathematical	—	DifferentiableOn Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing InnerProductSpace.toNormedSpace instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace Gamma Set.Ioi instPreorder instZero	—	DifferentiableAt.differentiableWithinAt differentiableAt_Gamma Set.mem_Ioi 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.Meta.NormNum.isNat_ofNat Nat.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.neg_congr Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_lt_of_le_of_neg instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le instIsOrderedRing Mathlib.Tactic.Linarith.natCast_nonneg Mathlib.Tactic.Linarith.sub_neg_of_lt

---

← Back to Index