Documentation Verification Report

Convergence

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

Statistics

Metric	Count
Definitions `abscissaOfAbsConv`	1
Theorems `abscissaOfAbsConv_binop_le`, `abscissaOfAbsConv_congr`, `abscissaOfAbsConv_congr'`, `abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable`, `abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable'`, `abscissaOfAbsConv_le_of_isBigO_rpow`, `abscissaOfAbsConv_le_of_le_const`, `abscissaOfAbsConv_le_of_le_const_mul_rpow`, `abscissaOfAbsConv_le_one_of_isBigO_one`, `summable_real_of_abscissaOfAbsConv_lt`, `abscissaOfAbsConv_le`, `LSeriesSummable_lt_re_of_abscissaOfAbsConv_lt_re`, `LSeriesSummable_of_abscissaOfAbsConv_lt_re`	13
Total	14

LSeries

Definitions

Name	Category	Theorems
`abscissaOfAbsConv` 📖	CompOp	27 math math: `abscissaOfAbsConv_one`, `LSeries_injOn`, `LSeries_eventually_eq_zero_iff'`, `LSeriesSummable.abscissaOfAbsConv_le`, `ArithmeticFunction.abscissaOfAbsConv_zeta`, `abscissaOfAbsConv_congr`, `LSeries_deriv_eqOn`, `abscissaOfAbsConv_le_of_le_const`, `LSeries_analyticOnNhd`, `ArithmeticFunction.vonMangoldt.abscissaOfAbsConv_residueClass_le_one`, `abscissaOfAbsConv_congr'`, `absicssaOfAbsConv_logPowMul`, `abscissaOfAbsConv_le_one_of_isBigO_one`, `abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable`, `abscissaOfAbsConv_logMul`, `abscissaOfAbsConv_binop_le`, `abscissaOfAbsConv_add_le`, `abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable'`, `abscissaOfAbsConv_convolution_le`, `DirichletCharacter.absicssaOfAbsConv_eq_one`, `abscissaOfAbsConv_le_of_le_const_mul_rpow`, `LSeries_differentiableOn`, `LSeries_analyticOn`, `abscissaOfAbsConv_sub_le`, `LSeries_eq_zero_iff`, `abscissaOfAbsConv_le_of_isBigO_rpow`, `ArithmeticFunction.abscissaOfAbsConv_moebius`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abscissaOfAbsConv_binop_le` 📖	mathematical	`LSeriesSummable`	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `abscissaOfAbsConv` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal`	—	`abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable'` `LSeriesSummable_of_abscissaOfAbsConv_lt_re` `LE.le.trans_lt` `le_max_left` `Complex.ofReal_re` `le_max_right`
`abscissaOfAbsConv_congr` 📖	mathematical	—	`abscissaOfAbsConv`	—	`Set.ext` `LSeriesSummable_congr`
`abscissaOfAbsConv_congr'` 📖	mathematical	`Filter.EventuallyEq` `Complex` `Filter.atTop` `Nat.instPreorder`	`abscissaOfAbsConv`	—	`Set.ext` `LSeriesSummable_congr'`
`abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable` 📖	mathematical	`LSeriesSummable` `Complex.ofReal`	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `abscissaOfAbsConv` `Real.toEReal`	—	`sInf_le_iff` `le_of_forall_gt_imp_ge_of_dense` `instDenselyOrderedEReal` `instIsEmptyFalse`
`abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable'` 📖	mathematical	`LSeriesSummable` `Complex.ofReal`	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `abscissaOfAbsConv`	—	`le_of_eq` `sInf_eq_bot` `EReal.bot_lt_coe` `Nat.cast_one` `sub_one_lt` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `EReal.zero_lt_top` `abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable` `le_top`
`abscissaOfAbsConv_le_of_isBigO_rpow` 📖	mathematical	`Asymptotics.IsBigO` `Complex` `Real` `Complex.instNorm` `Real.norm` `Filter.atTop` `Nat.instPreorder` `Real.instPow` `Real.instNatCast`	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `abscissaOfAbsConv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidEReal` `Real.toEReal` `instOneEReal`	—	`EReal.exists_between_coe_real` `LT.lt.false` `LE.le.trans_lt` `LSeriesSummable.abscissaOfAbsConv_le` `LSeriesSummable_of_isBigO_rpow` `EReal.coe_lt_coe_iff` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.add_congr` `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.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.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add`
`abscissaOfAbsConv_le_of_le_const` 📖	mathematical	`Real` `Real.instLE` `Norm.norm` `Complex` `Complex.instNorm`	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `abscissaOfAbsConv` `instOneEReal`	—	`zero_add` `abscissaOfAbsConv_le_of_le_const_mul_rpow` `Real.rpow_zero` `mul_one`
`abscissaOfAbsConv_le_of_le_const_mul_rpow` 📖	mathematical	`Real` `Real.instLE` `Norm.norm` `Complex` `Complex.instNorm` `Real.instMul` `Real.instPow` `Real.instNatCast`	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `abscissaOfAbsConv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidEReal` `Real.toEReal` `instOneEReal`	—	`EReal.exists_between_coe_real` `LT.lt.false` `LE.le.trans_lt` `LSeriesSummable.abscissaOfAbsConv_le` `LSeriesSummable_of_le_const_mul_rpow` `EReal.coe_lt_coe_iff` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.add_congr` `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.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.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add`
`abscissaOfAbsConv_le_one_of_isBigO_one` 📖	mathematical	`Asymptotics.IsBigO` `Complex` `Real` `Complex.instNorm` `Real.norm` `Filter.atTop` `Nat.instPreorder` `Real.instOne`	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `abscissaOfAbsConv` `instOneEReal`	—	`zero_add` `abscissaOfAbsConv_le_of_isBigO_rpow` `Real.rpow_zero` `NormedDivisionRing.to_normOneClass`
`summable_real_of_abscissaOfAbsConv_lt` 📖	mathematical	`EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `abscissaOfAbsConv` `Complex.ofReal` `Real.toEReal`	`Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instPow` `Real.instNatCast` `SummationFilter.unconditional`	—	`Complex.ofReal_div` `Complex.ofReal_cpow` `Nat.cast_nonneg` `Real.instIsOrderedRing` `LSeriesSummable_of_abscissaOfAbsConv_lt_re` `Complex.ofReal_re` `Summable.congr_cofinite` `instIsTopologicalAddGroupReal` `Filter.mp_mem` `Set.Finite.compl_mem_cofinite` `Set.finite_singleton` `Filter.univ_mem'`

LSeriesSummable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abscissaOfAbsConv_le` 📖	mathematical	`LSeriesSummable`	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `LSeries.abscissaOfAbsConv` `Real.toEReal` `Complex.re`	—	`sInf_le` `of_re_le_re`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`LSeriesSummable_lt_re_of_abscissaOfAbsConv_lt_re` 📖	mathematical	`EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `LSeries.abscissaOfAbsConv` `Real.toEReal` `Complex.re`	`Real` `Real.instLT` `LSeriesSummable` `Complex.ofReal`	—	`EReal.exists_between_coe_real` `LSeriesSummable_of_abscissaOfAbsConv_lt_re`
`LSeriesSummable_of_abscissaOfAbsConv_lt_re` 📖	mathematical	`EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `LSeries.abscissaOfAbsConv` `Real.toEReal` `Complex.re`	`LSeriesSummable`	—	`LSeriesSummable.of_re_le_re` `LT.lt.le` `Complex.ofReal_re`

---

← Back to Index