Basic

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

Statistics

Metric	Count
Definitions `GammaAux`, `GammaIntegral`, `partialGamma`, `evalGamma`	4
Theorems `GammaAux_recurrence1`, `GammaAux_recurrence2`, `GammaIntegral_add_one`, `GammaIntegral_conj`, `GammaIntegral_convergent`, `GammaIntegral_ofReal`, `GammaIntegral_one`, `Gamma_add_one`, `Gamma_conj`, `Gamma_def`, `Gamma_eq_GammaAux`, `Gamma_eq_integral`, `Gamma_nat_eq_factorial`, `Gamma_neg_nat_eq_zero`, `Gamma_ofNat_eq_factorial`, `Gamma_ofReal`, `Gamma_one`, `Gamma_zero`, `integral_cpow_mul_exp_neg_mul_Ioi`, `partialGamma_add_one`, `tendsto_partialGamma`, `GammaIntegral_convergent`, `Gamma_add_one`, `Gamma_eq_integral`, `Gamma_eq_zero_iff`, `Gamma_integrand_isLittleO`, `Gamma_nat_eq_factorial`, `Gamma_ne_zero`, `Gamma_neg_nat_eq_zero`, `Gamma_nonneg_of_nonneg`, `Gamma_ofNat_eq_factorial`, `Gamma_one`, `Gamma_pos_of_pos`, `Gamma_zero`, `integral_rpow_mul_exp_neg_mul_Ioi`	35
Total	39

Complex

Definitions

Name	Category	Theorems
`GammaAux` 📖	CompOp	5 math math: `differentiableAt_GammaAux`, `Gamma_eq_GammaAux`, `GammaAux_recurrence1`, `GammaAux_recurrence2`, `Gamma_def`
`GammaIntegral` 📖	CompOp	8 math math: `GammaIntegral_eq_mellin`, `hasDerivAt_GammaIntegral`, `GammaIntegral_ofReal`, `GammaIntegral_one`, `tendsto_partialGamma`, `Gamma_eq_integral`, `GammaIntegral_add_one`, `GammaIntegral_conj`
`partialGamma` 📖	CompOp	2 math math: `partialGamma_add_one`, `tendsto_partialGamma`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`GammaAux_recurrence1` 📖	mathematical	`Real` `Real.instLT` `Real.instNeg` `re` `Real.instNatCast`	`GammaAux` `Complex` `DivInvMonoid.toDiv` `instDivInvMonoid` `instAdd` `instOne`	—	`GammaIntegral_add_one` `CharP.cast_eq_zero` `CharP.ofCharZero` `RCLike.charZero_rclike` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `mul_comm` `mul_div_cancel_right₀` `EuclideanDomain.toMulDivCancelClass` `Mathlib.Tactic.Contrapose.contrapose₃` `add_re` `one_re` `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.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.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Nat.cast_add` `Mathlib.Tactic.Linarith.sub_nonpos_of_le`
`GammaAux_recurrence2` 📖	mathematical	`Real` `Real.instLT` `Real.instNeg` `re` `Real.instNatCast`	`GammaAux`	—	`GammaIntegral_add_one` `CharP.cast_eq_zero` `CharP.ofCharZero` `RCLike.charZero_rclike` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `mul_div_cancel_left₀` `EuclideanDomain.toMulDivCancelClass` `LT.lt.false` `zero_re` `add_re` `one_re` `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.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.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Nat.cast_add` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `GammaAux_recurrence1`
`GammaIntegral_add_one` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `re`	`GammaIntegral` `Complex` `instAdd` `instOne` `instMul`	—	`Filter.eventuallyEq_of_mem` `Filter.Ici_mem_atTop` `partialGamma_add_one` `Set.mem_Ici` `Mathlib.Tactic.Ring.sub_congr` `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` `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.RingNF.nat_rawCast_1` `pow_one` `mul_one` `Mathlib.Tactic.RingNF.int_rawCast_neg` `Mathlib.Tactic.RingNF.mul_neg` `add_zero` `Mathlib.Tactic.RingNF.add_neg` `Filter.Tendsto.congr'` `tendsto_zero_iff_norm_tendsto_zero` `Filter.Ioi_mem_atTop` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial` `norm_mul` `NormedDivisionRing.toNormMulClass` `norm_neg` `norm_cpow_eq_rpow_re_of_pos` `norm_of_nonneg` `LT.lt.le` `Real.exp_pos` `neg_mul` `one_mul` `Filter.tendsto_congr'` `tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `ofReal_exp` `ofReal_neg` `Filter.Tendsto.add` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Filter.Tendsto.const_mul` `IsTopologicalSemiring.toContinuousMul` `tendsto_partialGamma` `tendsto_nhds_unique` `instT2Space` `Filter.atTop_neBot` `instIsDirectedOrder` `Real.instArchimedean` `add_re` `one_re` `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.cast_zero` `Nat.cast_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` `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` `Mathlib.Tactic.Linarith.sub_nonpos_of_le`
`GammaIntegral_conj` 📖	mathematical	—	`GammaIntegral` `DFunLike.coe` `RingHom` `Complex` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `RingHom.instFunLike` `starRingEnd` `instStarRing`	—	`GammaIntegral.eq_1` `integral_conj` `MeasureTheory.setIntegral_congr_fun` `measurableSet_Ioi` `BorelSpace.opensMeasurable` `Real.borelSpace` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `conj_ofReal` `cpow_def_of_ne_zero` `ofReal_ne_zero` `ne_of_gt` `exp_conj` `ofReal_log` `le_of_lt` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `instCharZero` `SemilinearMapClass.distribMulActionSemiHomClass` `RingHomClass.toLinearMapClassNNRat` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass`
`GammaIntegral_convergent` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `re`	`MeasureTheory.IntegrableOn` `Complex` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `instMul` `ofReal` `Real.exp` `Real.instNeg` `instPow` `instSub` `instOne` `Set.Ioi` `Real.instPreorder` `MeasureTheory.MeasureSpace.volume`	—	`ContinuousOn.aestronglyMeasurable` `secondCountableTopologyEither_of_right` `secondCountable_of_proper` `instProperSpace` `BorelSpace.opensMeasurable` `Real.borelSpace` `PseudoEMetricSpace.pseudoMetrizableSpace` `ContinuousOn.mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Continuous.continuousOn` `Continuous.comp` `continuous_ofReal` `Continuous.rexp` `ContinuousNeg.continuous_neg` `IsTopologicalRing.toContinuousNeg` `instIsTopologicalRingReal` `continuousOn_of_forall_continuousAt` `continuousAt_cpow_const` `ofReal_mem_slitPlane` `ContinuousAt.comp` `Continuous.continuousAt` `measurableSet_Ioi` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `MeasureTheory.hasFiniteIntegral_norm_iff` `MeasureTheory.HasFiniteIntegral.congr` `Real.GammaIntegral_convergent` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.ae_restrict_iff'` `Filter.univ_mem'` `norm_mul` `NormedDivisionRing.toNormMulClass` `norm_of_nonneg` `le_of_lt` `Real.exp_pos` `norm_cpow_eq_rpow_re_of_pos`
`GammaIntegral_ofReal` 📖	mathematical	—	`GammaIntegral` `ofReal` `MeasureTheory.integral` `Real` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.Measure.restrict` `MeasureTheory.MeasureSpace.volume` `Set.Ioi` `Real.instPreorder` `Real.instZero` `Real.instMul` `Real.exp` `Real.instNeg` `Real.instPow` `Real.instSub` `Real.instOne`	—	`GammaIntegral.eq_1` `integral_ofReal` `MeasureTheory.setIntegral_congr_fun` `measurableSet_Ioi` `BorelSpace.opensMeasurable` `Real.borelSpace` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `ofReal_mul` `ofReal_cpow` `LT.lt.le` `Set.mem_Ioi` `ofReal_exp` `ofReal_neg` `ofReal_sub`
`GammaIntegral_one` 📖	mathematical	—	`GammaIntegral` `Complex` `instOne`	—	`GammaIntegral_ofReal` `sub_self` `Real.rpow_zero` `mul_one` `integral_exp_neg_Ioi_zero`
`Gamma_add_one` 📖	mathematical	—	`Gamma` `Complex` `instAdd` `instOne` `instMul`	—	`Real.instIsStrictOrderedRing` `sub_sub_cancel_left` `Nat.sub_one_lt_floor` `add_re` `one_re` `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.neg_mul` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.isInt_add` `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` `Real.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Gamma_eq_GammaAux` `GammaAux_recurrence1` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `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.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_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`
`Gamma_conj` 📖	mathematical	—	`Gamma` `DFunLike.coe` `RingHom` `Complex` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `RingHom.instFunLike` `starRingEnd` `instStarRing`	—	`GammaAux.eq_1` `GammaIntegral_conj` `GammaAux.eq_2` `div_eq_mul_inv` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `conj_inv` `map_add` `SemilinearMapClass.toAddHomClass` `instCharZero` `RingHomClass.toLinearMapClassNNRat` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `Real.instIsStrictOrderedRing` `Gamma_def`
`Gamma_def` 📖	mathematical	—	`Gamma` `GammaAux` `Nat.floor` `Real` `Real.semiring` `Real.partialOrder` `FloorRing.toFloorSemiring` `Real.instRing` `Real.linearOrder` `Real.instIsStrictOrderedRing` `Real.instFloorRing` `Real.instSub` `Real.instOne` `re`	—	`Real.instIsStrictOrderedRing`
`Gamma_eq_GammaAux` 📖	mathematical	`Real` `Real.instLT` `Real.instNeg` `re` `Real.instNatCast`	`Gamma` `GammaAux`	—	`Real.instIsStrictOrderedRing` `add_zero` `Gamma_def` `add_assoc` `GammaAux_recurrence2` `Nat.cast_add` `Nat.sub_one_lt_floor` `lt_add_of_lt_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `sub_sub_cancel_left` `Nat.cast_zero` `Nat.cast_le` `Real.instZeroLEOneClass` `RCLike.charZero_rclike` `Nat.cast_one` `lt_of_le_of_lt` `Nat.floor_le` `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.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.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `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.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.cast_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` `Nat.floor_of_nonpos` `le_of_not_gt` `Mathlib.Tactic.Linarith.add_neg`
`Gamma_eq_integral` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `re`	`Gamma` `GammaIntegral`	—	`Gamma_eq_GammaAux` `Nat.cast_zero` `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.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `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_neg_of_le` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le`
`Gamma_nat_eq_factorial` 📖	mathematical	—	`Gamma` `Complex` `instAdd` `instNatCast` `instOne` `Nat.factorial`	—	`CharP.cast_eq_zero` `CharP.ofCharZero` `instCharZero` `zero_add` `Gamma_one` `Nat.cast_one` `Gamma_add_one` `Nat.cast_ne_zero` `Nat.cast_succ` `Nat.cast_mul`
`Gamma_neg_nat_eq_zero` 📖	mathematical	—	`Gamma` `Complex` `instNeg` `instNatCast` `instZero`	—	`Nat.cast_zero` `neg_zero` `Gamma_zero` `neg_ne_zero` `Nat.cast_ne_zero` `instCharZero` `Nat.cast_add` `Nat.cast_one` `neg_add_rev` `neg_add_cancel_comm` `Mathlib.Tactic.Contrapose.contrapose₁` `mul_ne_zero` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `Gamma_add_one`
`Gamma_ofNat_eq_factorial` 📖	mathematical	—	`Gamma` `Complex` `instNatCast` `Nat.factorial`	—	`Nat.cast_one` `Gamma_nat_eq_factorial`
`Gamma_ofReal` 📖	mathematical	—	`Gamma` `ofReal` `Real.Gamma`	—	`Real.Gamma.eq_1` `conj_eq_iff_re` `Gamma_conj` `conj_ofReal`
`Gamma_one` 📖	mathematical	—	`Gamma` `Complex` `instOne`	—	`Gamma_eq_integral` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `GammaIntegral_one`
`Gamma_zero` 📖	mathematical	—	`Gamma` `Complex` `instZero`	—	`Real.instIsStrictOrderedRing` `Gamma_def` `sub_zero` `Nat.floor_one` `div_zero`
`integral_cpow_mul_exp_neg_mul_Ioi` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `re`	`MeasureTheory.integral` `Complex` `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` `exp` `instNeg` `DivInvMonoid.toDiv` `instDivInvMonoid` `Gamma`	—	`cpow_one` `cpow_add` `one_div_ne_zero` `ofReal_ne_zero` `LT.lt.ne'` `add_sub_cancel` `MeasureTheory.setIntegral_congr_fun` `measurableSet_Ioi` `BorelSpace.opensMeasurable` `Real.borelSpace` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `mul_cpow_ofReal_nonneg` `LT.lt.le` `Set.mem_Ioi` `mul_assoc` `one_div` `ofReal_inv` `inv_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `ofReal_mul` `inv_mul_cancel₀` `ofReal_one` `one_cpow` `one_mul` `MeasureTheory.integral_comp_mul_left_Ioi` `MulZeroClass.mul_zero` `real_smul` `ofReal_div` `Gamma_eq_integral` `ofReal_exp` `ofReal_neg` `mul_comm`
`partialGamma_add_one` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `re` `Real.instLE`	`partialGamma` `Complex` `instAdd` `instOne` `instSub` `instMul` `ofReal` `Real.exp` `Real.instNeg` `instPow`	—	`partialGamma.eq_1` `add_sub_cancel_right` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `HasDerivAt.congr_simp` `mul_neg` `mul_one` `HasDerivAt.exp` `hasDerivAt_neg` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `HasDerivAt.cpow_const` `hasDerivAt_id` `ofReal_mem_slitPlane` `HasDerivAt.comp_ofReal` `ofReal_neg` `neg_mul` `HasDerivAt.mul` `HasDerivAt.ofReal_comp` `Continuous.mul` `Continuous.comp` `continuous_ofReal` `Continuous.rexp` `ContinuousNeg.continuous_neg` `IsTopologicalRing.toContinuousNeg` `continuous_ofReal_cpow_const` `IntervalIntegrable.add` `IsTopologicalSemiring.toContinuousAdd` `intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le` `instCompleteSpace` `Continuous.continuousOn` `eq_sub_of_add_eq` `neg_neg` `neg_add` `intervalIntegral.integral_neg` `intervalIntegral.integral_add` `sub_neg_eq_add` `neg_sub` `add_comm` `add_sub` `Mathlib.Tactic.Contrapose.contrapose₃` `zero_re` `le_refl` `zero_cpow` `MulZeroClass.mul_zero` `add_zero` `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`
`tendsto_partialGamma` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `re`	`Filter.Tendsto` `Complex` `partialGamma` `Filter.atTop` `Real.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `GammaIntegral`	—	`MeasureTheory.intervalIntegral_tendsto_integral_Ioi` `instIsCountablyGenerated_atTop` `instOrderTopologyReal` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instSecondCountableTopologyReal` `GammaIntegral_convergent` `Filter.tendsto_id`

Mathlib.Meta.Positivity

Definitions

Name	Category	Theorems
`evalGamma` 📖	CompOp	—

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`GammaIntegral_convergent` 📖	mathematical	`Real` `instLT` `instZero`	`MeasureTheory.IntegrableOn` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `normedCommRing` `instMul` `exp` `instNeg` `instPow` `instSub` `instOne` `Set.Ioi` `instPreorder` `MeasureTheory.MeasureSpace.volume`	—	`Set.Ioc_union_Ioi_eq_Ioi` `zero_le_one` `instZeroLEOneClass` `MeasureTheory.integrableOn_union` `PseudoEMetricSpace.pseudoMetrizableSpace` `integrableOn_Icc_iff_integrableOn_Ioc` `instMeasurableSingletonClassOfMeasurableEq` `instMeasurableEqOfSecondCountableTopologyOfT2Space` `BorelSpace.opensMeasurable` `borelSpace` `instSecondCountableTopologyReal` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `noAtoms_volume` `enorm_ne_top` `MeasureTheory.IntegrableOn.continuousOn_mul` `secondCountableTopologyEither_of_right` `ContinuousOn.rexp` `ContinuousOn.neg` `IsTopologicalRing.toContinuousNeg` `instIsTopologicalRingReal` `continuousOn_id` `intervalIntegrable_iff_integrableOn_Icc_of_le` `intervalIntegral.intervalIntegrable_rpow'` `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.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.cast_pos` `Nat.cast_one` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `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.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `CompactIccSpace.isCompact_Icc` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `instOrderTopologyReal` `integrable_of_isBigO_exp_neg` `Nat.instAtLeastTwoHAddOfNat` `one_half_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `ContinuousOn.mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `ContinuousOn.rpow_const` `LT.lt.ne'` `LT.lt.trans_le` `zero_lt_one` `NeZero.charZero_one` `RCLike.charZero_rclike` `Asymptotics.IsLittleO.isBigO` `Gamma_integrand_isLittleO`
`Gamma_add_one` 📖	mathematical	—	`Gamma` `Real` `instAdd` `instOne` `instMul`	—	`Complex.ofReal_add` `Complex.ofReal_one` `Complex.Gamma_add_one` `Complex.ofReal_ne_zero` `Complex.re_ofReal_mul`
`Gamma_eq_integral` 📖	mathematical	`Real` `instLT` `instZero`	`Gamma` `MeasureTheory.integral` `normedAddCommGroup` `InnerProductSpace.toNormedSpace` `instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `MeasureTheory.Measure.restrict` `MeasureTheory.MeasureSpace.volume` `Set.Ioi` `instPreorder` `instMul` `exp` `instNeg` `instPow` `instSub` `instOne`	—	`Gamma.eq_1` `Complex.Gamma_eq_integral` `Complex.ofReal_re` `MeasureTheory.setIntegral_congr_fun` `measurableSet_Ioi` `BorelSpace.opensMeasurable` `borelSpace` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `instIsOrderedAddMonoid` `Complex.ofReal_exp` `Complex.ofReal_neg` `Complex.ofReal_sub` `Complex.ofReal_mul` `Complex.ofReal_cpow` `le_of_lt` `integral_ofReal`
`Gamma_eq_zero_iff` 📖	mathematical	—	`Gamma` `Real` `instZero` `instNeg` `instNatCast`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Gamma_ne_zero` `Gamma_neg_nat_eq_zero`
`Gamma_integrand_isLittleO` 📖	mathematical	—	`Asymptotics.IsLittleO` `Real` `norm` `Filter.atTop` `instPreorder` `instMul` `exp` `instNeg` `instPow` `DivInvMonoid.toDiv` `instDivInvMonoid` `instOne` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Asymptotics.isLittleO_of_tendsto` `Nat.instAtLeastTwoHAddOfNat` `LT.lt.ne'` `exp_pos` `exp_neg` `one_div` `neg_mul` `div_inv_eq_mul` `inv_div` `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.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `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.zpow'_ofNat` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `ne_of_gt` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `nsmul_eq_mul` `mul_inv_cancel_left₀` `RCLike.charZero_rclike` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Filter.Tendsto.inv_tendsto_atTop` `instIsStrictOrderedRing` `instOrderTopologyReal` `tendsto_exp_mul_div_rpow_atTop` `one_half_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono`
`Gamma_nat_eq_factorial` 📖	mathematical	—	`Gamma` `Real` `instAdd` `instNatCast` `instOne` `Nat.factorial`	—	`Gamma.eq_1` `Complex.ofReal_add` `Complex.ofReal_natCast` `Complex.ofReal_one` `Complex.Gamma_nat_eq_factorial` `Complex.ofReal_re`
`Gamma_ne_zero` 📖	—	—	—	—	`LT.lt.ne'` `Gamma_pos_of_pos` `neg_zero` `Nat.cast_zero` `Mathlib.Tactic.Contrapose.contrapose₄` `eq_sub_iff_add_eq` `Nat.cast_add` `Nat.cast_one` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_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.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `instIsOrderedRing` `neg_add` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `mul_ne_zero_iff` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `Gamma_add_one` `CharP.cast_eq_zero` `CharP.ofCharZero` `RCLike.charZero_rclike` `neg_lt` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `Nat.lt_floor_add_one`
`Gamma_neg_nat_eq_zero` 📖	mathematical	—	`Gamma` `Real` `instNeg` `instNatCast` `instZero`	—	`Complex.Gamma_ofReal` `Complex.Gamma_neg_nat_eq_zero`
`Gamma_nonneg_of_nonneg` 📖	mathematical	`Real` `instLE` `instZero`	`Gamma`	—	`eq_or_lt_of_le` `Gamma_zero` `le_refl` `LT.lt.le` `Gamma_pos_of_pos`
`Gamma_ofNat_eq_factorial` 📖	mathematical	—	`Gamma` `Real` `instNatCast` `Nat.factorial`	—	`Nat.cast_one` `Gamma_nat_eq_factorial`
`Gamma_one` 📖	mathematical	—	`Gamma` `Real` `instOne`	—	`Gamma.eq_1` `Complex.ofReal_one` `Complex.Gamma_one` `Complex.one_re`
`Gamma_pos_of_pos` 📖	mathematical	`Real` `instLT` `instZero`	`Gamma`	—	`Gamma_eq_integral` `Set.inter_eq_right` `Function.mem_support` `mul_ne_zero` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `LT.lt.ne'` `exp_pos` `rpow_pos_of_pos` `MeasureTheory.setIntegral_pos_iff_support_of_nonneg_ae` `Filter.eventually_of_mem` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.self_mem_ae_restrict` `measurableSet_Ioi` `BorelSpace.opensMeasurable` `borelSpace` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `instIsOrderedAddMonoid` `LT.lt.le` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing` `GammaIntegral_convergent` `volume_Ioi` `ENNReal.ofReal_zero` `ENNReal.ofReal_lt_top`
`Gamma_zero` 📖	mathematical	—	`Gamma` `Real` `instZero`	—	`Complex.Gamma_ofReal` `Complex.Gamma_zero`
`integral_rpow_mul_exp_neg_mul_Ioi` 📖	mathematical	`Real` `instLT` `instZero`	`MeasureTheory.integral` `normedAddCommGroup` `InnerProductSpace.toNormedSpace` `instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `MeasureTheory.Measure.restrict` `MeasureTheory.MeasureSpace.volume` `Set.Ioi` `instPreorder` `instMul` `instPow` `instSub` `instOne` `exp` `instNeg` `DivInvMonoid.toDiv` `instDivInvMonoid` `Gamma`	—	`Complex.ofReal_mul` `Complex.Gamma_ofReal` `Complex.ofReal_cpow` `le_of_lt` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing` `Mathlib.Meta.Positivity.pos_of_isNat` `instIsOrderedRing` `instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Complex.ofReal_div` `integral_ofReal` `MeasureTheory.setIntegral_congr_fun` `measurableSet_Ioi` `BorelSpace.opensMeasurable` `borelSpace` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `instIsOrderedAddMonoid` `LT.lt.le` `RCLike.ofReal_mul` `Complex.integral_cpow_mul_exp_neg_mul_Ioi` `Complex.ofReal_re`

---

← Back to Index