IwaniecKowalskiCh1

📁 Source: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean

Statistics

Metric	Count
Definitions `IsAdditive`, `IsCompletelyAdditive`, `d`, `powR`, `sigmaR`, `tau`, `termτ`, `«termσᴿ»`	8
Theorems `isAdditive`, `LSeries_d_eq_riemannZeta_pow`, `LSeries_d_summable`, `LSeries_powR_eq`, `LSeries_sigma_eq_riemannZeta_mul`, `LSeries_tau_eq_riemannZeta_sq`, `sum_divisorsAntidiagonal_prime_pow`, `abscissa_powR_le`, `d_apply`, `d_apply_prime_pow`, `d_isMultiplicative`, `d_one`, `d_succ`, `d_two`, `d_zero`, `sigmaR_eq_zeta_mul_powR`, `sigmaR_natCast`, `sum_divisors_mul_of_coprime`, `sum_moebius_pmul_eq_prod_one_sub`, `unique_divisor_decomposition`, `zeta_mul_tau_square_eq`, `zeta_mul_zeta`, `zeta_mul_zeta_mul_zeta_mul_zeta_eq`, `zeta_pow_four_eq`, `zeta_pow_three_eq`, `zeta_pow_three_eq_alt`	26
Total	34
⚠️ With sorry `sum_divisorsAntidiagonal_prime_pow`, `sum_divisors_mul_of_coprime`, `unique_divisor_decomposition`, `zeta_mul_tau_square_eq`, `zeta_mul_zeta_mul_zeta_mul_zeta_eq`, `zeta_pow_four_eq`, `zeta_pow_three_eq`, `zeta_pow_three_eq_alt`	8

ArithmeticFunction

Definitions

Name	Category	Theorems
`IsAdditive` 📖	MathDef	1 math math: `IsCompletelyAdditive.isAdditive`
`IsCompletelyAdditive` 📖	MathDef	—
`d` 📖	CompOp	9 math math: `d_zero`, `LSeries_d_summable`, `d_one`, `d_two`, `d_apply_prime_pow`, `LSeries_d_eq_riemannZeta_pow`, `d_apply`, `d_succ`, `d_isMultiplicative`
`powR` 📖	CompOp	3 math math: `abscissa_powR_le`, `LSeries_powR_eq`, `sigmaR_eq_zeta_mul_powR`
`sigmaR` 📖	CompOp	4 math math: `zeta_mul_zeta_mul_zeta_mul_zeta_eq`, `sigmaR_eq_zeta_mul_powR`, `sigmaR_natCast`, `LSeries_sigma_eq_riemannZeta_mul`
`tau` 📖	CompOp	7 math math: `zeta_pow_three_eq_alt`, `zeta_mul_tau_square_eq`, `d_two`, `zeta_mul_zeta`, `zeta_pow_three_eq`, `zeta_pow_four_eq`, `LSeries_tau_eq_riemannZeta_sq`
`termτ` 📖	CompOp	—
`«termσᴿ»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`LSeries_d_eq_riemannZeta_pow` 📖	mathematical	—	`d`	—	`d_zero` `d_succ` `LSeries_d_summable`
`LSeries_d_summable` 📖	mathematical	—	`d`	—	`d_zero` `d_succ`
`LSeries_powR_eq` 📖	mathematical	—	`powR`	—	—
`LSeries_sigma_eq_riemannZeta_mul` 📖	mathematical	—	`sigmaR`	—	`LSeries_powR_eq` `sigmaR_eq_zeta_mul_powR` `abscissa_powR_le`
`LSeries_tau_eq_riemannZeta_sq` 📖	mathematical	—	`tau`	—	`zeta_mul_zeta`
`abscissa_powR_le` 📖	mathematical	—	`powR`	—	—
`d_apply` 📖	mathematical	—	`d`	—	`d_isMultiplicative` `d_apply_prime_pow`
`d_apply_prime_pow` 📖	mathematical	—	`d`	—	`d_one` `d_succ`
`d_isMultiplicative` 📖	mathematical	—	`d`	—	`d_zero` `d_succ`
`d_one` 📖	mathematical	—	`d`	—	—
`d_succ` 📖	mathematical	—	`d`	—	—
`d_two` 📖	mathematical	—	`d` `tau`	—	`zeta_mul_zeta`
`d_zero` 📖	mathematical	—	`d`	—	—
`sigmaR_eq_zeta_mul_powR` 📖	mathematical	—	`sigmaR` `powR`	—	—
`sigmaR_natCast` 📖	mathematical	—	`sigmaR`	—	—
`sum_divisors_mul_of_coprime` 📖 ⚠️	—	—	—	—	—
`sum_moebius_pmul_eq_prod_one_sub` 📖	—	—	—	—	`sum_divisors_mul_of_coprime`
`unique_divisor_decomposition` 📖 ⚠️	—	—	—	—	—
`zeta_mul_tau_square_eq` 📖 ⚠️	mathematical	—	`tau`	—	—
`zeta_mul_zeta` 📖	mathematical	—	`tau`	—	—
`zeta_mul_zeta_mul_zeta_mul_zeta_eq` 📖 ⚠️	mathematical	—	`sigmaR`	—	—
`zeta_pow_four_eq` 📖 ⚠️	mathematical	—	`tau`	—	—
`zeta_pow_three_eq` 📖 ⚠️	mathematical	—	`tau`	—	—
`zeta_pow_three_eq_alt` 📖 ⚠️	mathematical	—	`tau`	—	—

ArithmeticFunction.IsCompletelyAdditive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isAdditive` 📖	mathematical	`ArithmeticFunction.IsCompletelyAdditive`	`ArithmeticFunction.IsAdditive`	—	—

ArithmeticFunction.Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sum_divisorsAntidiagonal_prime_pow` 📖 ⚠️	—	—	—	—	—

---

← Back to Index