Documentation Verification Report

LFunction

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

Statistics

Metric	Count
Definitions `eulerProduct`, `uniformSpace`, `LFunction`, `LFunction`	4
Theorems `instCompleteSpace`, `tendsTo_eulerProduct_of_tendsTo`	2
Total	6

ArithmeticFunction

Definitions

Name	Category	Theorems
`eulerProduct` 📖	CompOp	1 math math: `tendsTo_eulerProduct_of_tendsTo`
`uniformSpace` 📖	CompOp	1 math math: `instCompleteSpace`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instCompleteSpace` 📖	mathematical	—	`CompleteSpace` `ArithmeticFunction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `uniformSpace`	—	`IsUniformInducing.completeSpace` `IsClosed.isComplete` `Pi.complete` `DiscreteUniformity.instCompleteSpace` `DiscreteUniformity.inst` `Set.ext` `map_zero` `range_coe` `isClosed_setOf_map_zero` `T25Space.t2Space` `T3Space.t25Space` `instT3Space` `T1Space.t0Space` `instT1SpaceOfDiscreteTopology` `DiscreteUniformity.instDiscreteTopology` `UniformSpace.to_regularSpace`
`tendsTo_eulerProduct_of_tendsTo` 📖	mathematical	`Filter.Eventually` `DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instFunLikeNat` `one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Filter.cofinite`	`Filter.Eventually` `Finset` `DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instFunLikeNat` `Finset.prod` `CommSemiring.toCommMonoid` `instCommSemiring` `eulerProduct` `Filter.atTop` `PartialOrder.toPreorder` `Finset.partialOrder`	—	`instCompleteSpace` `IsUniformInducing.cauchy_map_iff` `Filter.map_map` `Filter.atTop_neBot` `Finset.isDirected_le` `Pi.uniformity` `DiscreteUniformity.eq_principal_setRelId` `DiscreteUniformity.inst` `Filter.prod_atTop_atTop_eq` `Filter.eventually_iff_exists_mem` `Filter.eventually_all_finite` `Set.finite_Iic` `Filter.mem_cofinite` `Finset.prod_sdiff` `Set.notMem_compl_iff` `Set.Finite.mem_toFinset` `Finset.mem_sdiff` `Finset.induction_on` `one_mul` `Finset.prod_insert` `mul_apply` `Finset.sum_congr` `Finset.mem_insert_self` `LE.le.trans` `Nat.divisor_le` `Nat.fst_mem_divisors_of_mem_antidiagonal` `Finset.mem_insert_of_mem` `Nat.snd_mem_divisors_of_mem_antidiagonal` `Multipliable.hasProd`

DirichletCharacter

Definitions

Name	Category	Theorems
`LFunction` 📖	CompOp	14 math math: `continuousOn_neg_logDeriv_LFunction_of_nontriv`, `LFunction_eq_LSeries`, `deriv_LFunction_eq_deriv_LSeries`, `LFunction_changeLevel`, `LFunction_modOne_eq`, `differentiableAt_LFunction`, `LFunction_eq_completed_div_gammaFactor`, `differentiable_LFunction`, `norm_LFunction_product_ge_one`, `Even.LFunction_neg_two_mul_nat`, `ArithmeticFunction.vonMangoldt.LSeries_residueClass_eq`, `Even.LFunction_neg_two_mul_nat_add_one`, `Odd.LFunction_neg_two_mul_nat_sub_one`, `LFunction_isBigO_horizontal`

ZMod

Definitions

Name	Category	Theorems
`LFunction` 📖	CompOp	15 math math: `differentiableAt_LFunction`, `LFunction_modOne_eq`, `LFunction_stdAddChar_eq_expZeta`, `LFunction_one_sub`, `LFunction_eq_LSeries`, `LFunction_def_odd`, `LFunction_eq_completed_div_gammaFactor_even`, `LFunction_neg_two_mul_nat_sub_one`, `LFunction_eq_completed_div_gammaFactor_odd`, `LFunction_def_even`, `LFunction_neg_two_mul_nat_add_one`, `LFunction_apply_zero_of_even`, `LFunction_residue_one`, `differentiable_LFunction_of_sum_zero`, `LFunction_dft`

---

← Back to Index