Documentation Verification Report

Positivity

📁 Source: Mathlib/NumberTheory/LSeries/Positivity.lean

Statistics

Metric	Count
Definitions	0
Theorems `LSeries_positive`, `LSeries_positive_of_differentiable_of_eqOn`, `iteratedDeriv_LSeries_alternating`, `iteratedDeriv_alternating`, `positive`, `positive_of_differentiable_of_eqOn`	6
Total	6

ArithmeticFunction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`LSeries_positive` 📖	mathematical	`Pi.hasLe` `Complex` `Preorder.toLE` `PartialOrder.toPreorder` `Complex.partialOrder` `Pi.instZero` `Complex.instZero` `Preorder.toLT` `EReal` `instPartialOrderEReal` `LSeries.abscissaOfAbsConv` `Real.toEReal`	`LSeries` `Complex.ofReal`	—	`LSeries.positive`
`LSeries_positive_of_differentiable_of_eqOn` 📖	mathematical	`Pi.hasLe` `Complex` `Preorder.toLE` `PartialOrder.toPreorder` `Complex.partialOrder` `Pi.instZero` `Complex.instZero` `DFunLike.coe` `ArithmeticFunction` `instFunLikeNat` `Preorder.toLT` `Differentiable` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `EReal` `instPartialOrderEReal` `LSeries.abscissaOfAbsConv` `Real.toEReal` `Set.EqOn` `LSeries` `setOf` `Real` `Real.instLT` `Complex.re`	`Complex.ofReal`	—	`LSeries.positive_of_differentiable_of_eqOn`
`iteratedDeriv_LSeries_alternating` 📖	mathematical	`Complex` `Preorder.toLE` `PartialOrder.toPreorder` `Complex.partialOrder` `Complex.instZero` `DFunLike.coe` `ArithmeticFunction` `instFunLikeNat` `EReal` `Preorder.toLT` `instPartialOrderEReal` `LSeries.abscissaOfAbsConv` `Real.toEReal`	`Complex.instMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Complex.instNeg` `Complex.instOne` `iteratedDeriv` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `LSeries` `Complex.ofReal`	—	`LSeries.iteratedDeriv_alternating`

LSeries

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iteratedDeriv_alternating` 📖	mathematical	`Pi.hasLe` `Complex` `Preorder.toLE` `PartialOrder.toPreorder` `Complex.partialOrder` `Pi.instZero` `Complex.instZero` `EReal` `Preorder.toLT` `instPartialOrderEReal` `abscissaOfAbsConv` `Real.toEReal`	`Complex.instMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Complex.instNeg` `Complex.instOne` `iteratedDeriv` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `LSeries` `Complex.ofReal`	—	`LSeries_iteratedDeriv` `eq_1` `mul_assoc` `pow_add` `Even.neg_one_pow` `one_mul` `tsum_nonneg` `RCLike.toIsOrderedAddMonoid` `Complex.orderClosedTopology` `term_def` `mul_nonneg` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `RCLike.toIsStrictOrderedRing` `Function.iterate_succ_apply'` `LT.lt.le` `Complex.inv_natCast_cpow_ofReal_pos` `le_rfl`
`positive` 📖	mathematical	`Pi.hasLe` `Complex` `Preorder.toLE` `PartialOrder.toPreorder` `Complex.partialOrder` `Pi.instZero` `Complex.instZero` `Preorder.toLT` `EReal` `instPartialOrderEReal` `abscissaOfAbsConv` `Real.toEReal`	`LSeries` `Complex.ofReal`	—	`eq_1` `Summable.tsum_pos` `RCLike.toIsOrderedAddMonoid` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Complex.orderClosedTopology` `SummationFilter.instLeAtTopUnconditional` `SummationFilter.instNeBotUnconditional` `LSeriesSummable_of_abscissaOfAbsConv_lt_re` `term_nonneg` `term_pos` `one_ne_zero`
`positive_of_differentiable_of_eqOn` 📖	mathematical	`Pi.hasLe` `Complex` `Preorder.toLE` `PartialOrder.toPreorder` `Complex.partialOrder` `Pi.instZero` `Complex.instZero` `Preorder.toLT` `Differentiable` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `EReal` `instPartialOrderEReal` `abscissaOfAbsConv` `Real.toEReal` `Set.EqOn` `LSeries` `setOf` `Real` `Real.instLT` `Complex.re`	`Complex.ofReal`	—	`LE.le.trans_lt` `le_max_left` `lt_add_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Nat.cast_one` `Complex.ofReal_add` `positive` `LT.lt.trans_le` `Differentiable.apply_le_of_iteratedDeriv_alternating` `Continuous.isOpen_preimage` `Complex.continuous_re` `isOpen_Ioi` `instClosedIicTopology` `RCLike.instOrderClosedTopology` `Set.EqOn.iteratedDeriv_of_isOpen` `iteratedDeriv_alternating` `LE.le.trans` `le_max_right` `LT.lt.le`

---

← Back to Index