Documentation Verification Report

Nonvanishing

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

Statistics

Metric	Count
Definitions `zetaMul`	1
Theorems `LFunctionTrivChar_isBigO_near_one_horizontal`, `LFunction_apply_one_ne_zero`, `LFunction_isBigO_horizontal`, `LFunction_ne_zero_of_one_le_re`, `LFunction_ne_zero_of_re_eq_one`, `LSeriesSummable_zetaMul`, `isMultiplicative_zetaMul`, `norm_LFunction_product_ge_one`, `norm_LSeries_product_ge_one`, `summable_neg_log_one_sub_mul_prime_cpow`, `zetaMul_nonneg`, `zetaMul_prime_pow_nonneg`, `riemannZeta_ne_zero_of_one_le_re`	13
Total	14

DirichletCharacter

Definitions

Name	Category	Theorems
`zetaMul` 📖	CompOp	4 math math: `zetaMul_prime_pow_nonneg`, `zetaMul_nonneg`, `isMultiplicative_zetaMul`, `LSeriesSummable_zetaMul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`LFunctionTrivChar_isBigO_near_one_horizontal` 📖	mathematical	—	`Asymptotics.IsBigO` `Real` `Complex` `Complex.instNorm` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero` `Set.Ioi` `Real.instPreorder` `LFunctionTrivChar` `Complex.instAdd` `Complex.instOne` `Complex.ofReal` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid`	—	`add_sub_cancel_left` `Filter.Tendsto.comp` `LFunctionTrivChar_residue_one` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `add_zero` `Eq.le` `Homeomorph.map_punctured_nhds_eq` `Asymptotics.isBigO_mul_iff_isBigO_div` `eventually_mem_nhdsWithin` `Filter.Tendsto.isBigO_one` `NormedDivisionRing.to_normOneClass` `Asymptotics.IsBigO.mono` `Complex.isBigO_comp_ofReal_nhds_ne` `nhdsGT_le_nhdsNE`
`LFunction_apply_one_ne_zero` 📖	—	—	—	—	`LFunction_ne_zero_of_one_le_re` `le_rfl` `Complex.one_re`
`LFunction_isBigO_horizontal` 📖	mathematical	—	`Asymptotics.IsBigO` `Real` `Complex` `Complex.instNorm` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero` `Set.Ioi` `Real.instPreorder` `LFunction` `Complex.instAdd` `Complex.instOne` `Complex.ofReal` `Complex.instMul` `Complex.I`	—	`Asymptotics.IsBigO.mono` `LFunction.congr_simp` `add_comm` `add_assoc` `DifferentiableAt.continuousAt` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `differentiableAt_LFunction` `Filter.Tendsto.isBigO_one` `NormedDivisionRing.to_normOneClass` `ContinuousAt.tendsto` `ContinuousAt.comp` `zero_add` `ContinuousAt.fun_add` `Continuous.continuousAt` `Complex.continuous_ofReal` `continuousAt_const` `nhdsWithin_le_nhds`
`LFunction_ne_zero_of_one_le_re` 📖	—	`Real` `Real.instLE` `Real.instOne` `Complex.re`	—	—	`LE.le.eq_or_lt` `LFunction_ne_zero_of_re_eq_one` `LSeries_ne_zero_of_one_lt_re` `LFunction_eq_LSeries`
`LFunction_ne_zero_of_re_eq_one` 📖	—	`Complex.re` `Real` `Real.instOne`	—	—	`Complex.re_add_im` `Complex.ofReal_one` `mul_comm` `Nat.cast_zero` `right_ne_zero_of_mul` `add_ne_left` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `not_and_or`
`LSeriesSummable_zetaMul` 📖	mathematical	`Real` `Real.instLT` `Real.instOne` `Complex.re`	`LSeriesSummable` `DFunLike.coe` `ArithmeticFunction` `Complex` `Complex.instZero` `ArithmeticFunction.instFunLikeNat` `zetaMul`	—	`ArithmeticFunction.LSeriesSummable_mul` `ArithmeticFunction.LSeriesSummable_zeta_iff` `LSeriesSummable_of_bounded_of_one_lt_re` `norm_le_one`
`isMultiplicative_zetaMul` 📖	mathematical	—	`ArithmeticFunction.IsMultiplicative` `Complex` `Semiring.toMonoidWithZero` `Complex.instSemiring` `zetaMul`	—	`ArithmeticFunction.IsMultiplicative.mul` `ArithmeticFunction.IsMultiplicative.natCast` `ArithmeticFunction.isMultiplicative_zeta` `isMultiplicative_toArithmeticFunction`
`norm_LFunction_product_ge_one` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Real.instLE` `Norm.norm` `Complex` `Complex.instNorm` `Complex.instMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `LFunctionTrivChar` `Complex.instAdd` `Complex.instOne` `Complex.ofReal` `LFunction` `Complex.I` `DirichletCharacter` `CommGroupWithZero.toCommMonoidWithZero` `Semifield.toCommGroupWithZero` `Field.toSemifield` `Complex.instField` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `MulChar.commGroup` `ZMod` `CommRing.toCommMonoid` `ZMod.commRing` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.instOne`	—	`Nat.instAtLeastTwoHAddOfNat` `LFunctionTrivChar.eq_1` `LFunction_eq_LSeries` `norm_LSeries_product_ge_one`
`norm_LSeries_product_ge_one` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Real.instLE` `Norm.norm` `Complex` `Complex.instNorm` `Complex.instMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `LSeries` `DFunLike.coe` `DirichletCharacter` `CommGroupWithZero.toCommMonoidWithZero` `Semifield.toCommGroupWithZero` `Field.toSemifield` `Complex.instField` `ZMod` `MulChar.instFunLike` `CommRing.toCommMonoid` `ZMod.commRing` `MulChar.hasOne` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Complex.instAdd` `Complex.instOne` `Complex.ofReal` `Complex.I` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `MulChar.commGroup` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.instOne`	—	`Nat.instAtLeastTwoHAddOfNat` `summable_neg_log_one_sub_mul_prime_cpow` `Summable.mul_left` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `HasSum.summable` `Complex.hasSum_re` `Summable.hasSum` `LSeries_eulerProduct_exp_log` `Complex.norm_exp` `MulZeroClass.zero_mul` `sub_zero` `Complex.re_tsum` `SummationFilter.instNeBotUnconditional` `tsum_mul_left` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Summable.tsum_add` `IsTopologicalSemiring.toContinuousAdd` `Summable.add` `neg_add_rev` `mul_neg` `MulChar.pow_apply'` `two_ne_zero` `Complex.ofReal_add` `tsum_nonneg` `Real.instIsOrderedAddMonoid` `RCLike.instOrderClosedTopology` `Nat.Prime.two_le` `Subtype.prop`
`summable_neg_log_one_sub_mul_prime_cpow` 📖	mathematical	`Real` `Real.instLT` `Real.instOne` `Complex.re`	`Summable` `Complex` `Nat.Primes` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `Complex.instNeg` `Complex.log` `Complex.instSub` `Complex.instOne` `Complex.instMul` `DFunLike.coe` `DirichletCharacter` `CommGroupWithZero.toCommMonoidWithZero` `Semifield.toCommGroupWithZero` `Field.toSemifield` `Complex.instField` `ZMod` `MulChar.instFunLike` `CommRing.toCommMonoid` `ZMod.commRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Nat.Prime` `Complex.instPow` `Complex.instNatCast` `SummationFilter.unconditional`	—	`norm_mul` `NormedDivisionRing.toNormMulClass` `Complex.norm_natCast_cpow_of_re_ne_zero` `Complex.re_neg_ne_zero_of_one_lt_re` `mul_le_of_le_one_left` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `Real.rpow_nonneg` `Nat.cast_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `norm_le_one` `Summable.neg` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Summable.clog_one_sub` `Summable.of_norm` `Complex.instCompleteSpace` `Summable.of_nonneg_of_le` `norm_nonneg` `Nat.Primes.summable_rpow` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add`
`zetaMul_nonneg` 📖	mathematical	`DirichletCharacter` `Complex` `CommGroupWithZero.toCommMonoidWithZero` `Semifield.toCommGroupWithZero` `Field.toSemifield` `Complex.instField` `Monoid.toNatPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `MulChar.commGroup` `ZMod` `CommRing.toCommMonoid` `ZMod.commRing` `MulChar.hasOne`	`Preorder.toLE` `PartialOrder.toPreorder` `Complex.partialOrder` `Complex.instZero` `DFunLike.coe` `ArithmeticFunction` `ArithmeticFunction.instFunLikeNat` `zetaMul`	—	`eq_or_ne` `ArithmeticFunction.map_zero` `ArithmeticFunction.IsMultiplicative.multiplicative_factorization` `isMultiplicative_zetaMul` `Finset.prod_nonneg` `RCLike.toZeroLEOneClass` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `RCLike.toIsStrictOrderedRing` `zetaMul_prime_pow_nonneg` `Nat.prime_of_mem_primeFactors`
`zetaMul_prime_pow_nonneg` 📖	mathematical	`DirichletCharacter` `Complex` `CommGroupWithZero.toCommMonoidWithZero` `Semifield.toCommGroupWithZero` `Field.toSemifield` `Complex.instField` `Monoid.toNatPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `MulChar.commGroup` `ZMod` `CommRing.toCommMonoid` `ZMod.commRing` `MulChar.hasOne` `Nat.Prime`	`Preorder.toLE` `PartialOrder.toPreorder` `Complex.partialOrder` `Complex.instZero` `DFunLike.coe` `ArithmeticFunction` `ArithmeticFunction.instFunLikeNat` `zetaMul` `Nat.instMonoid`	—	`ArithmeticFunction.coe_zeta_mul_apply` `Finset.sum_congr` `Nat.sum_divisors_prime_pow` `isReduced_of_noZeroDivisors` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `StarOrderedRing.toExistsAddOfLE` `Nat.instStarOrderedRing` `Nat.instNontrivial` `Nat.Prime.ne_zero` `Nat.cast_pow` `map_pow` `MulCharClass.toMonoidHomClass` `MulChar.instMulCharClass` `MulChar.isQuadratic_iff_sq_eq_one` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `Complex.instNontrivial` `Finset.sum_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `RCLike.toIsOrderedAddMonoid` `RCLike.toZeroLEOneClass` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `RCLike.toIsStrictOrderedRing` `one_pow` `neg_one_geom_sum` `le_rfl` `zero_le_one`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`riemannZeta_ne_zero_of_one_le_re` 📖	—	`Real` `Real.instLE` `Real.instOne` `Complex.re`	—	—	`eq_or_ne` `riemannZeta_one_ne_zero` `DirichletCharacter.LFunction_ne_zero_of_one_le_re` `DirichletCharacter.LFunction_modOne_eq`

---

← Back to Index