Documentation Verification Report

VonMangoldt

📁 Source: Mathlib/NumberTheory/ArithmeticFunction/VonMangoldt.lean

Statistics

Metric	Count
Definitions `termΛ`, `vonMangoldt`, `termΛ`	3
Theorems `log_apply`, `log_mul_moebius_eq_vonMangoldt`, `moebius_mul_log_eq_vonMangoldt`, `sum_moebius_mul_log_eq`, `vonMangoldt_apply`, `vonMangoldt_apply_one`, `vonMangoldt_apply_pow`, `vonMangoldt_apply_prime`, `vonMangoldt_eq_zero_iff`, `vonMangoldt_le_log`, `vonMangoldt_mul_zeta`, `vonMangoldt_ne_zero_iff`, `vonMangoldt_nonneg`, `vonMangoldt_pos_iff`, `vonMangoldt_sum`, `zeta_mul_vonMangoldt`	16
Total	19

ArithmeticFunction

Definitions

Name	Category	Theorems
`termΛ` 📖	CompOp	—
`vonMangoldt` 📖	CompOp	27 math math: `vonMangoldt.residueClass_eq`, `DirichletCharacter.LSeries_twist_vonMangoldt_eq`, `Chebyshev.psi_sub_theta_eq_sum_not_prime`, `vonMangoldt.residueClass_apply`, `LSeries_vonMangoldt_eq_deriv_riemannZeta_div`, `convolution_vonMangoldt_const_one`, `convolution_vonMangoldt_zeta`, `vonMangoldt_pos_iff`, `vonMangoldt_sum`, `DirichletCharacter.LSeriesSummable_twist_vonMangoldt`, `DirichletCharacter.convolution_twist_vonMangoldt`, `LSeries_vonMangoldt_eq`, `log_mul_moebius_eq_vonMangoldt`, `vonMangoldt.residueClass_le`, `moebius_mul_log_eq_vonMangoldt`, `vonMangoldt_nonneg`, `sum_moebius_mul_log_eq`, `vonMangoldt_apply`, `vonMangoldt_apply_one`, `Chebyshev.psi_eq_sum_Icc`, `vonMangoldt_eq_zero_iff`, `vonMangoldt_le_log`, `LSeriesSummable_vonMangoldt`, `vonMangoldt_mul_zeta`, `vonMangoldt_apply_prime`, `vonMangoldt_apply_pow`, `zeta_mul_vonMangoldt`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`log_apply` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `Real` `Real.instZero` `instFunLikeNat` `log` `Real.log` `Real.instNatCast`	—	—
`log_mul_moebius_eq_vonMangoldt` 📖	mathematical	—	`ArithmeticFunction` `Real` `Real.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Real.instRing` `instMul` `Real.semiring` `log` `ofInt` `moebius` `vonMangoldt`	—	`vonMangoldt_mul_zeta` `mul_assoc` `coe_zeta_mul_coe_moebius` `mul_one`
`moebius_mul_log_eq_vonMangoldt` 📖	mathematical	—	`ArithmeticFunction` `Real` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Real.instRing` `Real.instZero` `instMul` `Real.semiring` `ofInt` `moebius` `log` `vonMangoldt`	—	`mul_comm` `log_mul_moebius_eq_vonMangoldt`
`sum_moebius_mul_log_eq` 📖	mathematical	—	`Finset.sum` `Real` `Real.instAddCommMonoid` `Nat.divisors` `Real.instMul` `Real.instIntCast` `DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `instFunLikeNat` `moebius` `Real.instZero` `log` `Real.instNeg` `vonMangoldt`	—	`Finset.sum_congr` `mul_comm` `neg_mul_eq_mul_neg` `Nat.sum_divisorsAntidiagonal` `Nat.cast_ne_zero` `RCLike.charZero_rclike` `Nat.cast_div` `Real.log_div` `neg_sub` `mul_sub` `Finset.sum_sub_distrib` `Finset.sum_mul` `Int.cast_sum` `coe_mul_zeta_apply` `sub_eq_self` `moebius_mul_coe_zeta` `eq_or_ne` `Int.cast_one` `Nat.cast_one` `Real.log_one` `MulZeroClass.mul_zero` `one_apply_ne` `Int.cast_zero` `MulZeroClass.zero_mul`
`vonMangoldt_apply` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `Real` `Real.instZero` `instFunLikeNat` `vonMangoldt` `IsPrimePow` `Nat.instCommMonoidWithZero` `instDecidableIsPrimePowNat` `Real.log` `Real.instNatCast` `Nat.minFac`	—	—
`vonMangoldt_apply_one` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `Real` `Real.instZero` `instFunLikeNat` `vonMangoldt`	—	`Nat.minFac_one` `Nat.cast_one` `Real.log_one`
`vonMangoldt_apply_pow` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `Real` `Real.instZero` `instFunLikeNat` `vonMangoldt` `Monoid.toNatPow` `Nat.instMonoid`	—	`isPrimePow_pow_iff` `Nat.pow_minFac`
`vonMangoldt_apply_prime` 📖	mathematical	`Nat.Prime`	`DFunLike.coe` `ArithmeticFunction` `Real` `Real.instZero` `instFunLikeNat` `vonMangoldt` `Real.log` `Real.instNatCast`	—	`vonMangoldt_apply` `Nat.Prime.minFac_eq` `Prime.isPrimePow` `Nat.Prime.prime`
`vonMangoldt_eq_zero_iff` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `Real` `Real.instZero` `instFunLikeNat` `vonMangoldt` `IsPrimePow` `Nat.instCommMonoidWithZero`	—	`Iff.not_right` `vonMangoldt_ne_zero_iff`
`vonMangoldt_le_log` 📖	mathematical	—	`Real` `Real.instLE` `DFunLike.coe` `ArithmeticFunction` `Real.instZero` `instFunLikeNat` `vonMangoldt` `Real.log` `Real.instNatCast`	—	`map_zero` `CharP.cast_eq_zero` `CharP.ofCharZero` `RCLike.charZero_rclike` `Real.log_zero` `vonMangoldt_sum` `Finset.single_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `vonMangoldt_nonneg` `Nat.mem_divisors_self`
`vonMangoldt_mul_zeta` 📖	mathematical	—	`ArithmeticFunction` `Real` `Real.instZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Real.instRing` `instMul` `Real.semiring` `vonMangoldt` `natToArithmeticFunction` `zeta` `log`	—	`ext` `coe_mul_zeta_apply` `vonMangoldt_sum`
`vonMangoldt_ne_zero_iff` 📖	mathematical	—	`IsPrimePow` `Nat.instCommMonoidWithZero`	—	`eq_or_ne` `vonMangoldt_apply_one` `Ne.ite_ne_right_iff` `LT.lt.ne'` `Real.log_pos` `Nat.one_lt_cast` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `RCLike.charZero_rclike` `Nat.Prime.one_lt` `Nat.minFac_prime`
`vonMangoldt_nonneg` 📖	mathematical	—	`Real` `Real.instLE` `Real.instZero` `DFunLike.coe` `ArithmeticFunction` `instFunLikeNat` `vonMangoldt`	—	`vonMangoldt_apply` `Real.log_nonneg` `Nat.one_le_cast` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `RCLike.charZero_rclike` `Nat.minFac_pos` `le_refl`
`vonMangoldt_pos_iff` 📖	mathematical	—	`Real` `Real.instLT` `Real.instZero` `DFunLike.coe` `ArithmeticFunction` `instFunLikeNat` `vonMangoldt` `IsPrimePow` `Nat.instCommMonoidWithZero`	—	`LE.le.lt_iff_ne` `vonMangoldt_nonneg` `vonMangoldt_ne_zero_iff`
`vonMangoldt_sum` 📖	mathematical	—	`Finset.sum` `Real` `Real.instAddCommMonoid` `Nat.divisors` `DFunLike.coe` `ArithmeticFunction` `Real.instZero` `instFunLikeNat` `vonMangoldt` `Real.log` `Real.instNatCast`	—	`Finset.sum_congr` `Nat.divisors_zero` `CharP.cast_eq_zero` `CharP.ofCharZero` `RCLike.charZero_rclike` `Real.log_zero` `Nat.sum_divisors_prime_pow` `Nat.cast_pow` `Real.log_pow` `Finset.sum_range_succ'` `vonMangoldt_apply_one` `vonMangoldt_apply_pow` `vonMangoldt_apply_prime` `Finset.sum_const` `Finset.card_range` `nsmul_eq_mul` `add_zero` `Nat.mul_divisors_filter_prime_pow` `Finset.filter_union` `Finset.sum_union` `Nat.disjoint_divisors_filter_isPrimePow` `Nat.cast_mul` `Real.log_mul` `Nat.cast_ne_zero` `LT.lt.ne'` `pos_of_gt` `Nat.instCanonicallyOrderedAdd`
`zeta_mul_vonMangoldt` 📖	mathematical	—	`ArithmeticFunction` `Real` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Real.instRing` `Real.instZero` `instMul` `Real.semiring` `natToArithmeticFunction` `zeta` `vonMangoldt` `log`	—	`mul_comm` `vonMangoldt_mul_zeta`

ArithmeticFunction.vonMangoldt

Definitions

Name	Category	Theorems
`termΛ` 📖	CompOp	—

---

← Back to Index