BrunTitchmarsh

📁 Source: PrimeNumberTheoremAnd/BrunTitchmarsh.lean

Statistics

Metric	Count
Definitions `primeInterSieve`, `primesBetween`	2
Theorems `Ioc_filter_dvd_eq`, `nat_Top_of_atTop`, `ceil_le_self_add_one`, `abs_rem_le`, `boudingSum_ge`, `card_Ioc_filter_dvd`, `card_isPrimePow_isBigO`, `card_pows_aux`, `card_range_filter_isPrimePow_le`, `card_range_filter_prime_isBigO`, `ceil_approx`, `err_isBigO`, `floor_approx`, `floor_div_approx`, `multSum_eq`, `nat_div_approx`, `one_add_log_div_log_two_isBigO`, `pow_half_mul_one_add_log_div_isBigO`, `pows_small_primes_le`, `primeSieve_rem_sum_le`, `prime_or_pow`, `primesBetween_le`, `primesBetween_le_siftedSum_add`, `primesBetween_mono_right`, `primesBetween_one`, `primesBetween_subset`, `range_filter_isPrimePow_subset_union`, `rem_eq`, `rpow_mul_rpow_log_isBigO_id_div_log`, `siftedSum_eq_card`, `siftedSum_le`, `tmp`	32
Total	34

BrunTitchmarsh

Definitions

Name	Category	Theorems
`primeInterSieve` 📖	CompOp	8 math math: `primesBetween_le_siftedSum_add`, `boudingSum_ge`, `primeSieve_rem_sum_le`, `siftedSum_le`, `rem_eq`, `multSum_eq`, `abs_rem_le`, `siftedSum_eq_card`
`primesBetween` 📖	CompOp	4 math math: `primesBetween_le_siftedSum_add`, `primesBetween_le`, `primesBetween_mono_right`, `primesBetween_one`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Ioc_filter_dvd_eq` 📖	—	—	—	—	—
`abs_rem_le` 📖	mathematical	—	`primeInterSieve`	—	`rem_eq` `Nat.ceil_le_self_add_one` `floor_div_approx` `nat_div_approx` `ceil_approx`
`boudingSum_ge` 📖	mathematical	—	`SelbergSieve.selbergBoundingSum` `primeInterSieve`	—	`Sieve.boundingSum_ge_log` `Sieve.prime_dvd_primorial_iff`
`card_Ioc_filter_dvd` 📖	—	—	—	—	`Ioc_filter_dvd_eq`
`card_isPrimePow_isBigO` 📖	—	—	—	—	`range_filter_isPrimePow_subset_union` `card_range_filter_prime_isBigO` `card_pows_aux`
`card_pows_aux` 📖	—	—	—	—	`pows_small_primes_le` `Asymptotics.IsBigO.natCast` `pow_half_mul_one_add_log_div_isBigO`
`card_range_filter_isPrimePow_le` 📖	—	—	—	—	`IsBigO.nat_Top_of_atTop` `card_isPrimePow_isBigO`
`card_range_filter_prime_isBigO` 📖	—	—	—	—	`tmp` `Asymptotics.IsBigO.natCast` `err_isBigO`
`ceil_approx` 📖	—	—	—	—	`Nat.ceil_le_self_add_one`
`err_isBigO` 📖	—	—	—	—	`rpow_mul_rpow_log_isBigO_id_div_log`
`floor_approx` 📖	—	—	—	—	—
`floor_div_approx` 📖	—	—	—	—	`nat_div_approx` `floor_approx`
`multSum_eq` 📖	mathematical	—	`primeInterSieve`	—	`primeInterSieve.eq_1` `card_Ioc_filter_dvd`
`nat_div_approx` 📖	—	—	—	—	`floor_approx`
`one_add_log_div_log_two_isBigO` 📖	—	—	—	—	—
`pow_half_mul_one_add_log_div_isBigO` 📖	—	—	—	—	`one_add_log_div_log_two_isBigO` `rpow_mul_rpow_log_isBigO_id_div_log`
`pows_small_primes_le` 📖	—	—	—	—	—
`primeSieve_rem_sum_le` 📖	mathematical	—	`primeInterSieve`	—	`Sieve.rem_sum_le_of_const` `abs_rem_le`
`prime_or_pow` 📖	—	—	—	—	—
`primesBetween_le` 📖	mathematical	—	`primesBetween`	—	`siftedSum_le` `primesBetween_le_siftedSum_add`
`primesBetween_le_siftedSum_add` 📖	mathematical	—	`primesBetween` `primeInterSieve`	—	`primesBetween.eq_1` `primesBetween_subset` `siftedSum_eq_card`
`primesBetween_mono_right` 📖	mathematical	—	`primesBetween`	—	—
`primesBetween_one` 📖	mathematical	—	`primesBetween`	—	`primesBetween.eq_1`
`primesBetween_subset` 📖	—	—	—	—	—
`range_filter_isPrimePow_subset_union` 📖	—	—	—	—	`prime_or_pow`
`rem_eq` 📖	mathematical	—	`primeInterSieve`	—	`multSum_eq`
`rpow_mul_rpow_log_isBigO_id_div_log` 📖	—	—	—	—	—
`siftedSum_eq_card` 📖	mathematical	—	`primeInterSieve`	—	`Sieve.siftedSum_eq`
`siftedSum_le` 📖	mathematical	—	`primeInterSieve`	—	`SelbergSieve.selberg_bound_simple` `boudingSum_ge` `primeSieve_rem_sum_le`
`tmp` 📖	—	—	—	—	`primesBetween_one` `primesBetween_le` `primesBetween_mono_right`

BrunTitchmarsh.IsBigO

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nat_Top_of_atTop` 📖	—	—	—	—	—

BrunTitchmarsh.Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ceil_le_self_add_one` 📖	—	—	—	—	—

---

← Back to Index