PrimeCounting

📁 Source: Mathlib/NumberTheory/PrimeCounting.lean

Statistics

Metric	Count
Definitions termπ, termπ', primeCounting, primeCounting'	4
Theorems add_two_le_nth_prime, monotone_primeCounting, monotone_primeCounting', primeCounting'_add_le, primeCounting'_eq_zero_iff, primeCounting'_nth_eq, primeCounting_eq_zero_iff, primeCounting_one, primeCounting_sub_one, primeCounting_zero, prime_nth_prime, primesBelow_card_eq_primeCounting', surjective_primeCounting, surjective_primeCounting', tendsto_primeCounting, tendsto_primeCounting'	16
Total	20

Nat

Definitions

Name	Category	Theorems
primeCounting 📖	CompOp	10 math math: primeCounting_sub_one, tendsto_primeCounting, Chebyshev.primeCounting_eq_theta_div_log_add_integral, Chebyshev.primeCounting_sub_theta_div_log_isBigO, surjective_primeCounting, primeCounting_zero, primeCounting_eq_zero_iff, monotone_primeCounting, Chebyshev.eventually_primeCounting_le, primeCounting_one
primeCounting' 📖	CompOp	8 math math: primeCounting_sub_one, monotone_primeCounting', primeCounting'_add_le, surjective_primeCounting', primesBelow_card_eq_primeCounting', primeCounting'_nth_eq, tendsto_primeCounting', primeCounting'_eq_zero_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_two_le_nth_prime 📖	mathematical	—	nth Prime	—	StrictMono.add_le_nat nth_strictMono infinite_setOf_prime nth_prime_zero_eq_two
monotone_primeCounting 📖	mathematical	—	Monotone instPreorder primeCounting	—	Monotone.comp monotone_primeCounting' Monotone.add_const covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid monotone_id
monotone_primeCounting' 📖	mathematical	—	Monotone instPreorder primeCounting'	—	count_monotone
primeCounting'_add_le 📖	mathematical	—	primeCounting' totient	—	primeCounting'.eq_1 count_eq_card_filter_range Finset.range_eq_Ico Finset.Ico_union_Ico_eq_Ico le_self_add instCanonicallyOrderedAdd Finset.filter_union Finset.card_union_le le_refl add_le_add_right IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid Finset.card_le_card Finset.monotone_filter_right coprime_of_lt_prime LT.lt.trans_le Finset.mem_Ico add_le_add_iff_left IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Ico_filter_coprime_le
primeCounting'_eq_zero_iff 📖	mathematical	—	primeCounting'	—	primeCounting'.eq_1 count_eq_zero prime_two nth_prime_zero_eq_two
primeCounting'_nth_eq 📖	mathematical	—	primeCounting' nth Prime	—	count_nth_of_infinite infinite_setOf_prime
primeCounting_eq_zero_iff 📖	mathematical	—	primeCounting	—	—
primeCounting_one 📖	mathematical	—	primeCounting	—	primeCounting_eq_zero_iff le_rfl
primeCounting_sub_one 📖	mathematical	—	primeCounting primeCounting'	—	—
primeCounting_zero 📖	mathematical	—	primeCounting	—	primeCounting_eq_zero_iff zero_le_one instZeroLEOneClass
prime_nth_prime 📖	mathematical	—	Prime nth	—	nth_mem_of_infinite infinite_setOf_prime
primesBelow_card_eq_primeCounting' 📖	mathematical	—	Finset.card primesBelow primeCounting'	—	count_eq_card_filter_range
surjective_primeCounting 📖	mathematical	—	primeCounting	—	primeCounting_sub_one surjective_primeCounting' Function.Surjective.of_comp
surjective_primeCounting' 📖	mathematical	—	primeCounting'	—	surjective_count_of_infinite_setOf infinite_setOf_prime
tendsto_primeCounting 📖	mathematical	—	Filter.Tendsto primeCounting Filter.atTop instPreorder	—	Filter.tendsto_add_atTop_iff_nat tendsto_primeCounting'
tendsto_primeCounting' 📖	mathematical	—	Filter.Tendsto primeCounting' Filter.atTop instPreorder	—	Filter.tendsto_atTop_atTop_of_monotone' monotone_primeCounting' Set.range_eq_univ surjective_primeCounting' instNoTopOrderOfNoMaxOrder instNoMaxOrder

Nat.Prime

Definitions

Name	Category	Theorems
termπ 📖	CompOp	—
termπ' 📖	CompOp	—

---

← Back to Index