Documentation Verification Report

Deriv

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

Statistics

Metric	Count
Definitions `logMul`	1
Theorems `abscissaOfAbsConv_logMul`, `absicssaOfAbsConv_logPowMul`, `hasDerivAt_term`, `LSeriesSummable_logMul_of_lt_re`, `LSeries_analyticOn`, `LSeries_analyticOnNhd`, `LSeries_deriv`, `LSeries_deriv_eqOn`, `LSeries_differentiableOn`, `LSeries_hasDerivAt`, `LSeries_iteratedDeriv`	11
Total	12

LSeries

Definitions

Name	Category	Theorems
`logMul` 📖	CompOp	8 math math: `LSeries_iteratedDeriv`, `LSeries_deriv_eqOn`, `LSeries_deriv`, `absicssaOfAbsConv_logPowMul`, `abscissaOfAbsConv_logMul`, `LSeries_hasDerivAt`, `LSeriesSummable_logMul_of_lt_re`, `hasDerivAt_term`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abscissaOfAbsConv_logMul` 📖	mathematical	—	`abscissaOfAbsConv` `logMul`	—	`le_antisymm` `abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable'` `LSeriesSummable_logMul_of_lt_re` `Summable.of_norm_bounded_eventually_nat` `Complex.instCompleteSpace` `Summable.norm` `Complex.instFiniteDimensionalReal` `LSeriesSummable_of_abscissaOfAbsConv_lt_re` `Filter.mp_mem` `Real.instIsStrictOrderedRing` `Filter.eventually_ge_atTop` `Filter.univ_mem'` `term_of_ne_zero` `mul_div_assoc` `norm_mul` `NormedDivisionRing.toNormMulClass` `Complex.norm_real` `le_mul_of_one_le_left` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `norm_nonneg` `LE.le.trans` `Real.log_exp` `Real.log_le_log` `Real.exp_pos` `Nat.ceil_le` `le_max_right` `Real.le_norm_self`
`absicssaOfAbsConv_logPowMul` 📖	mathematical	—	`abscissaOfAbsConv` `Nat.iterate` `logMul`	—	`Function.iterate_succ'` `abscissaOfAbsConv_logMul`
`hasDerivAt_term` 📖	mathematical	—	`HasDerivAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `IsModuleTopology.toContinuousSMul` `NontriviallyNormedField.toNormedField` `Complex.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` `Complex.instSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `term` `Complex.instNeg` `logMul`	—	`IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `eq_or_ne` `HasDerivAt.congr_simp` `neg_zero` `term_of_ne_zero` `mul_comm` `mul_div_assoc` `div_eq_mul_inv` `HasDerivAt.const_mul` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `mul_neg_one` `ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `HasDerivAt.const_cpow` `hasDerivAt_neg'` `Nat.cast_ne_zero` `Complex.instCharZero`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`LSeriesSummable_logMul_of_lt_re` 📖	mathematical	`EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `LSeries.abscissaOfAbsConv` `Real.toEReal` `Complex.re`	`LSeriesSummable` `LSeries.logMul`	—	`IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing`
`LSeries_analyticOn` 📖	mathematical	—	`AnalyticOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `LSeries` `setOf` `EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `LSeries.abscissaOfAbsConv` `Real.toEReal` `Complex.re`	—	`AnalyticOnNhd.analyticOn` `LSeries_analyticOnNhd`
`LSeries_analyticOnNhd` 📖	mathematical	—	`AnalyticOnNhd` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `LSeries` `setOf` `EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `LSeries.abscissaOfAbsConv` `Real.toEReal` `Complex.re`	—	`DifferentiableOn.analyticOnNhd` `Complex.instCompleteSpace` `LSeries_differentiableOn` `Complex.isOpen_re_gt_EReal`
`LSeries_deriv` 📖	mathematical	`EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `LSeries.abscissaOfAbsConv` `Real.toEReal` `Complex.re`	`deriv` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `LSeries` `Complex.instNeg` `LSeries.logMul`	—	`HasDerivAt.deriv` `LSeries_hasDerivAt`
`LSeries_deriv_eqOn` 📖	mathematical	—	`Set.EqOn` `Complex` `deriv` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `LSeries` `Pi.instNeg` `Complex.instNeg` `LSeries.logMul` `setOf` `EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `LSeries.abscissaOfAbsConv` `Real.toEReal` `Complex.re`	—	`deriv_eqOn` `Complex.isOpen_re_gt_EReal` `HasDerivAt.hasDerivWithinAt` `LSeries_hasDerivAt`
`LSeries_differentiableOn` 📖	mathematical	—	`DifferentiableOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `LSeries` `setOf` `EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `LSeries.abscissaOfAbsConv` `Real.toEReal` `Complex.re`	—	`DifferentiableAt.differentiableWithinAt` `HasDerivAt.differentiableAt` `LSeries_hasDerivAt`
`LSeries_hasDerivAt` 📖	mathematical	`EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `LSeries.abscissaOfAbsConv` `Real.toEReal` `Complex.re`	`HasDerivAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `IsModuleTopology.toContinuousSMul` `NontriviallyNormedField.toNormedField` `Complex.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` `Complex.instSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `LSeries` `Complex.instNeg` `LSeries.logMul`	—	`IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing`
`LSeries_iteratedDeriv` 📖	mathematical	`EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `LSeries.abscissaOfAbsConv` `Real.toEReal` `Complex.re`	`iteratedDeriv` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `LSeries` `Complex.instMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Complex.instNeg` `Complex.instOne` `Nat.iterate` `LSeries.logMul`	—	`iteratedDeriv_zero` `pow_zero` `one_mul` `derivWithin_congr` `iteratedDeriv_succ` `derivWithin_of_isOpen` `Complex.isOpen_re_gt_EReal` `deriv_const_mul_field'` `LSeries_deriv` `LSeries.absicssaOfAbsConv_logPowMul` `mul_neg` `pow_succ` `mul_one` `Function.iterate_succ'` `neg_mul`

---

← Back to Index