| Name | Category | Theorems |
|---|
Eθ 📖 | CompOp | 15 mathmath: BKLNW.lem_6, Ramanujan.pi_bound_1, Dusart.theorem_4_2, FKS2.Eθ_eq_abs, Ramanujan.pi_bound_6, Ramanujan.pi_bound_5, FKS2.theorem_6_1, Ramanujan.pi_bound_3, FKS2.integral_term_bound, Ramanujan.pi_bound_4, FKS2.Eθ_nonneg, BKLNW.cor_14_1, FKS2.lemma_12, Ramanujan.pi_bound_2, Ramanujan.pi_bound
|
Eπ 📖 | CompOp | 7 mathmath: FKS2.theorem_6, FKS2.corollary_24, FKS2.corollary_21, FKS2.theorem_6_1, FKS2.corollary_8, FKS2.theorem_6_alt, FKS2.corollary_8_apply_theorem_6
|
Eπ_star 📖 | CompOp | — |
Eψ 📖 | CompOp | 15 mathmath: BKLNW_app.thm_14, BKLNW_app.bklnw_cor_15_1, FKS.lemma_5_3, FKS.theorem_1_1b, BKLNW_app.bklnw_thm_16, BKLNW_app.bklnw_eq_A_26, FKS.proposition_3_4, FKS.theorem_3_1, FKS.theorem_1_1, Dusart.proposition_3_2, BKLNW_app.bklnw_cor_15_1', FKS.lemma_5_4, Buthe.theorem_2a, BKLNW_app.bklnw_lemma_15, Dusart.theorem_3_3
|
HasPrimeInInterval 📖 | MathDef | 25 mathmath: Dusart.proposition_5_4c, CullyHugill2021.has_prime_in_interval, RamareSaouter2003.has_prime_in_interval, HasPrimeInInterval.iff_theta_ge, GourdonDemichel2004.has_prime_in_interval, Dudek2014.has_prime_in_interval, CarneiroEtAl2019RH.has_prime_in_interval, Dusart.corollary_5_5, Eθ.numericalBound.hasPrimeInInterval, PrimeGaps2014.has_prime_in_interval, Axler2018.has_prime_in_interval_2, PrimeGaps2024.has_prime_in_interval, Trudgian2016.has_prime_in_interval, HasPrimeInInterval.iff_pi_ge, RHPrimeInterval2002.has_prime_in_interval, Schoenfeld1976.has_prime_in_interval, Eθ.classicalBound.hasPrimeInInterval, Axler2018.has_prime_in_interval_1, theta_pos_implies_prime_in_interval, Eθ.hasPrimeInInterval, Dudek2015RH.has_prime_in_interval, prime_gap_record.hasPrimeInInterval, RamareSaouter2003.has_prime_in_interval_2, Dusart.proposition_5_4b, KadiriLumley.has_prime_in_interval
|
Li 📖 | CompOp | 14 mathmath: Ramanujan.pi_error_identity, li.sub_Li, FKS2.hasDerivAt_Li, Ramanujan.Li_eq_sub_add_integral, FKS2.theorem_6_3, FKS2.he, FKS2.theorem_6_1, FKS2.lemma_20_a, FKS2.integral_one_div_log_sq, FKS2.lemma_20_b, FKS2.hasDerivAt_Li_sub_div_log, FKS2.lemma_19, FKS2.Li_identity', FKS2.Li_identity
|
M 📖 | CompOp | 3 mathmath: M_isLittleO, M_isLittleO', M_log_identity
|
Psi 📖 | CompOp | 2 mathmath: M_log_identity, sum_mu_Lambda
|
admissible_bound 📖 | CompOp | 17 mathmath: FKS2.ratio_eq_g, FKS2.delta_term_bound, Eψ.classicalBound.to_numericalBound, Eθ.classicalBound.to_numericalBound, FKS2.admissible_bound_mul, PT.admissible_bound_weaken, FKS2.corollary_21, FKS2.admissible_bound_pos, FKS2.integral_term_bound, FKS2.logx_over_x_bound, Eπ.classicalBound.to_numericalBound, FKS2.admissible_bound_le_0826, BKLNW.cor_14_1, FKS2.corollary_14_small_adm, admissible_bound.mono, FKS2.integral_algebra, FKS2.ratio_mono
|
first_gap 📖 | CompOp | 9 mathmath: eSHP.first_gap_4, eSHP.first_gap_2, eSHP.first_gap_1, eSHP.first_gap_5, eSHP.first_gap_odd_gt_1, eSHP.first_gap_3, eSHP.first_gap_6, eSHP.first_gap_7, eSHP.exists_prime_gap
|
first_gap_record 📖 | MathDef | 2 mathmath: eSHP.table_9_prime_gap, eSHP.table_9_prime_gap_test
|
li 📖 | CompOp | 13 mathmath: li.sub_Li, li.two_approx, li_eq_eulerMascheroni_add_log_log_add_tsum, li.two_approx_weak, Buthe2.theorem_2c, Buthe.theorem_2d, li_eq_Li2Bounds_li, Buthe2.theorem_2d, Buthe.theorem_2f, li2_symmetric_eq_li2, Buthe.theorem_b, Buthe.theorem_2e, LiSeries.li_eq_eulerMascheroni_add_log_log_add_tsum
|
nth_prime 📖 | CompOp | 9 mathmath: eSHP.exists_prime_gap_record_le, nth_prime_asymp, pn_pn_plus_one, log_nth_prime_asymp, pn_asymptotic, eSHP.nth_prime_vals, pi_nth_prime_asymp, pi_nth_prime, tendsto_nth_prime_atTop
|
nth_prime' 📖 | CompOp | 31 mathmath: Dusart.lemma_5_14, Axler.sum_prime_upper, Rosser1941.p_n_upper, Dusart.proposition_5_16, RS_prime_helper.p_n_lower_large, Dusart.proposition_5_11a, Robin.p_n_lower_const1, Dusart.proposition_5_12, Dusart.lemma_5_10a, Rosser1941.p_n_lower, Dusart1999.p_n_lower, Dusart1999.p_n_upper, DeKoninckLetendre.sum_log_prime, Rosser1938.p_n_gt_1, DeKoninckLetendre.sum_loglog_prime, MassiasRobin.p_n_lower, Rosser1938.p_n_lt_2, Dusart.lemma_5_10b, CMS.prime_gap, Cipolla.p_n_asym, RS_prime_helper.nth_prime_gt_bound, RS_prime.p_n_lower, Robin.p_n_lower, RS_prime.p_n_upper, Dusart.proposition_5_11b, Dusart.proposition_5_15, Axler.sum_prime_lower, RS_prime_helper.p_n_lower_small, Rosser1938.p_n_gt_2, Dusart.massias_robin_thm_Bv, RS_prime_helper.pi_nth_prime'
|
nth_prime_gap 📖 | CompOp | 2 mathmath: eSHP.exists_prime_gap_record_le, eSHP.max_prime_gap
|
pi 📖 | CompOp | 31 mathmath: Ramanujan.pi_error_identity, Dusart.corollary_5_3_a, Ramanujan.ex_pi_gt_nonneg, Ramanujan.sq_pi_lt, Dusart.corollary_5_3_b, Ramanujan.pi_upper, Dusart1999.pi_inequality, Ramanujan.pi_lower, Ramanujan.criterion, Dusart.theorem_5_1, Ramanujan.pi_upper_specific, FKS2.he, Dusart.corollary_5_2_d, Buthe2.theorem_2d, Ramanujan.pi_lower_specific, Ramanujan.ex_pi_gt, Dusart.corollary_5_2_b, Buthe.theorem_2f, RS_prime.theorem_b, Dusart.corollary_5_3_d, HasPrimeInInterval.iff_pi_ge, Ramanujan.ex_pi_gt_neg, Dusart.corollary_5_2_f, Dusart.corollary_5_2_e, Dusart.corollary_5_2_c, Dusart.corollary_5_3_c, Buthe.theorem_b, RS_prime_helper.pi_nth_prime', Buthe.theorem_2e, Dusart.corollary_5_2_a, Ramanujan.ramanujan_final
|
pi_star 📖 | CompOp | 1 mathmath: Buthe2.theorem_2c
|
prime_gap_record 📖 | MathDef | 3 mathmath: eSHP.exists_prime_gap_record_le, eSHP.table_8_prime_gap_test, eSHP.table_8_prime_gap
|