| Metric | Count |
|---|
DefinitionsAbsolutelyContinuous, S, cheby, chebyWith, cumsum, exists_trunc, gg, hh, hh', instCoeForallRealForallComplex_primeNumberTheoremAnd_1, instMeasurableSpace, nabla, nnabla, nterm, pp, pp', shift, toSchwartz | 18 |
Theoremsadd_isLittleO_right, sq, add_const, comp_add, summable, sum_shift_back, sum_shift_back', sum_shift_front, sum_shift_front', fourierIntegral_conj_neg, fourierIntegral_convolution, log_eventually_gt_atTop, S_sub_S, integrable_fourier, WI_sum_Iab_le, WI_sum_Iab_le', WI_sum_le, WI_summable, WI_tendsto_aux, WI_tendsto_aux', WeakPNT, WeakPNT_AP, WeakPNT_AP_prelim, WeakPNT_character, WienerIkeharaInterval, WienerIkeharaInterval_discrete, WienerIkeharaInterval_discrete', WienerIkeharaTheorem', WienerIkeharaTheorem'', auto_cheby, auto_cheby_bootstrap_induction, auto_cheby_exists_smooth_nonneg_fourier_kernel, auto_cheby_fourier_summable, auto_cheby_short_interval_bound, bound_I1, bound_I1', bound_I2, bound_main, bound_sum_log, bound_sum_log', bound_sum_log0, bounded_of_shift, cancel_aux, cancel_aux', cancel_main, cancel_main', ceil_mul_le_iff, bigO, comp_exp_support, comp_exp_support0, comp_exp_support1, comp_exp_support2, continuous_FourierIntegral, continuous_LSeries_aux, continuous_multiplicative_ofAdd, crude_upper_bound, cumsum_nonneg, cumsum_succ, cumsum_zero, decay_alt, decay_bounds, decay_bounds_W21, decay_bounds_aux, decay_bounds_cor, decay_bounds_cor_aux, decay_bounds_key, dirichlet_test', exists_antitone_of_eventually, exists_bound_norm_G_on_tsupport, first_fourier, first_fourier_aux1, first_fourier_aux2, first_fourier_aux2a, fourier_decay_of_CS2, fourier_surjection_on_schwartz, ge_of_eventually_nhdsWithin, gg_l1, gg_le_one, gg_of_hh, hf_coe1, hh'_nonpos, hh_antitone, hh_continuous, hh_deriv, hh_integrable, hh_integrable_aux, hh_integral, hh_integral', hh_le, hh_nonneg, instBorelSpace, integrable_norm_fourier_scaled_of_CS2, interval_approx_inf, interval_approx_sup, isBigO_log_mul_add, isBigO_pow_pow_of_le, isLittleO_const_of_tendsto_atTop, isLittleO_mul_add_sq, le_floor_mul_iff, le_of_eventually_nhdsWithin, limiting_cor, limiting_cor_W21, limiting_cor_aux, limiting_cor_schwartz, limiting_fourier, limiting_fourier_aux, limiting_fourier_aux_gt_zero, limiting_fourier_lim1, limiting_fourier_lim1_aux, limiting_fourier_lim2, limiting_fourier_lim2_aux, limiting_fourier_lim2_gt_zero, limiting_fourier_lim3, limiting_fourier_lim3_gt_zero, limiting_fourier_variant, limiting_fourier_variant_lim1, limiting_fourier_variant_lim1_aux, log_add_div_isBigO_log, log_add_one_sub_log_le, log_isbigo_log_div, log_mul_add_isBigO_log, log_sq_isbigo_mul, lt_ceil_mul_iff, mem_Icc_iff_div, mem_Ico_iff_div, nabla_cumsum, nabla_log, nabla_log_main, nabla_mul, neg_cumsum, neg_nabla, nnabla_bound, nnabla_bound_aux, nnabla_bound_aux1, nnabla_bound_aux2, nnabla_cast, nnabla_mul, nnabla_mul_log_sq, norm_error_integral_le, norm_integrand_le_K_mul_norm_psi, norm_lt_norm_of_nonneg, norm_mul_integral_Ici_le_integral_norm, norm_term_eq_nterm_re, norm_x_cpow_it, nterm_eq_norm_term, one_add_sq_pos, one_div_sub_one, one_div_two_pi_mem_Ioo, pp'_deriv, pp'_deriv_eq, pp_deriv, pp_deriv_eq, pp_pos, prelim_decay, prelim_decay_2, prelim_decay_3, quadratic_pos, residue_nonneg, second_fourier, second_fourier_aux, second_fourier_integrable_aux1, second_fourier_integrable_aux1a, second_fourier_integrable_aux2, set_integral_ofReal, smooth_urysohn, sum_le_integral, sum_range_succ, sum_telescopic, summable_congr_ae, summable_fourier, summable_fourier_aux, summable_iff_bounded, summable_iff_bounded', summable_inv_mul_log_sq, summable_vonMangoldt_div_rpow, summation_by_parts, summation_by_parts', summation_by_parts'', tendsto_S_S_zero, tendsto_mul_add_atTop, tendsto_mul_ceil_div, tendsto_tsum_of_monotone_convergence, tendsto_tsum_of_monotone_convergence_nhdsGT_one, toSchwartz_apply, tsum_indicator, vonMangoldt_cheby, wiener_ikehara_smooth, wiener_ikehara_smooth', wiener_ikehara_smooth_aux, wiener_ikehara_smooth_real, wiener_ikehara_smooth_sub | 191 |
| Total | 209 |
⚠️ With sorryprelim_decay_2, prelim_decay_3 | 2 |
| Name | Category | Theorems |
|---|
AbsolutelyContinuous 📖 | MathDef | 1 mathmath: CH2.ϕ_continuous
|
S 📖 | CompOp | 2 mathmath: tendsto_S_S_zero, S_sub_S
|
cheby 📖 | MathDef | 3 mathmath: auto_cheby, auto_cheby_bootstrap_induction, vonMangoldt_cheby
|
chebyWith 📖 | MathDef | — |
cumsum 📖 | CompOp | 20 mathmath: summation_by_parts', summable_iff_bounded', summation_by_parts, WienerIkeharaTheorem'', Finset.sum_shift_back, Finset.sum_shift_back', cheby.bigO, WienerIkeharaTheorem', summation_by_parts'', cumsum_succ, Finset.sum_shift_front', cumsum_nonneg, nabla_cumsum, S_sub_S, summable_iff_bounded, cumsum_zero, neg_cumsum, WeakPNT, Finset.sum_shift_front, WeakPNT_AP
|
exists_trunc 📖 | CompOp | — |
gg 📖 | CompOp | 3 mathmath: gg_of_hh, gg_l1, gg_le_one
|
hh 📖 | CompOp | 12 mathmath: hh_antitone, gg_of_hh, hh_integral, hh_le, hh_integrable, hh_integrable_aux, hh_continuous, hh_deriv, bound_sum_log, hh_nonneg, bound_sum_log0, hh_integral'
|
hh' 📖 | CompOp | 2 mathmath: hh_deriv, hh'_nonpos
|
instCoeForallRealForallComplex_primeNumberTheoremAnd_1 📖 | CompOp | — |
instMeasurableSpace 📖 | CompOp | 1 mathmath: instBorelSpace
|
nabla 📖 | CompOp | 9 mathmath: summation_by_parts', summation_by_parts'', log_add_one_sub_log_le, nabla_cumsum, nabla_log, nabla_log_main, nnabla_mul_log_sq, neg_nabla, nabla_mul
|
nnabla 📖 | CompOp | 5 mathmath: nnabla_bound_aux, nnabla_mul, nnabla_bound, nnabla_cast, neg_nabla
|
nterm 📖 | CompOp | 2 mathmath: nterm_eq_norm_term, norm_term_eq_nterm_re
|
pp 📖 | CompOp | 3 mathmath: pp_deriv_eq, pp_pos, pp_deriv
|
pp' 📖 | CompOp | 4 mathmath: pp_deriv_eq, pp_deriv, pp'_deriv, pp'_deriv_eq
|
shift 📖 | CompOp | 6 mathmath: summation_by_parts', summation_by_parts, Finset.sum_shift_back', summation_by_parts'', Finset.sum_shift_front', Finset.sum_shift_front
|
toSchwartz 📖 | CompOp | — |