AlexKontorovich/PrimeNumberTheoremAnd
maintenance drain Indexed 15795 theorem-like declarations
Sorries left 1% 194 markers in 193 declarations
Blueprint 142 nodes to go
788 of 930 proved
141 ready 1 deprecated
| Theorem | Status | Owner | Module | Last run |
|---|---|---|---|---|
| a1_large_le_two | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_regime3_4900_6500.lean | |
| a1_large_le_two | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_regime3_4400_4875.lean | |
| a1_large_le_two | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_regime3_3400_3875.lean | |
| a1_large_le_two | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_regime3_2400_2875.lean | |
| a1_large_le_two | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_regime3_8600_10500.lean | |
| a1_large_le_two | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_regime3_100_1875.lean | |
| a1_large_le_two | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_regime3_10600_12500.lean | |
| a1_large_le_two | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_regime3_2900_3375.lean | |
| a1_large_le_two | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_regime3_12600_24000.lean | |
| a1_large_le_two | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_regime3_1900_2375.lean | |
| a1_large_le_two | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_regime3_3900_4375.lean | |
| a1_large_le_two | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_regime3_6600_8500.lean | |
| a1_le_small | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_core.lean | |
| a2_100_exp_lower | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_100_exp_upper | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_100_lower | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_100_mem_Icc | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_100_upper | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_150_exp_lower | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_150_exp_upper | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_150_lower | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_150_mem_Icc | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_150_upper | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_200_exp_lower | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_200_exp_upper | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_200_lower | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_200_mem_Icc | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_200_upper | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_20_exp_lower | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_20_exp_upper | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_20_lower | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_20_mem_Icc | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_20_upper | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_250_exp_lower | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_250_exp_upper | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_250_lower | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_250_mem_Icc | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_250_upper | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_25_exp_lower | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_25_exp_upper | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_25_lower | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_25_mem_Icc | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_25_upper | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_300_exp_lower | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_300_exp_upper | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_300_lower | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_300_mem_Icc | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_300_upper | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_30_exp_lower | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_30_exp_upper | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_30_lower | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_30_mem_Icc | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_30_upper | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_35_exp_lower | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_35_exp_upper | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_35_lower | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_35_mem_Icc | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_35_upper | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_40_exp_lower | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_40_exp_upper | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_40_lower | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_40_mem_Icc | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_40_upper | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_43_exp_lower | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_43_exp_upper | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_43_lower | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_43_mem_Icc | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_43_upper | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a2_crude_le | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_core.lean | |
| a2_mid_le | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_core.lean | |
| a_3870_upper | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean | |
| _abel_1_1 | Checked | unowned | PrimeNumberTheoremAnd/LaplaceInversion.lean | |
| _abel_1_1 | Checked | unowned | PrimeNumberTheoremAnd/LaplaceInversion.lean | |
| _abel_1_1 | Checked | unowned | PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean | |
| _abel_1_1 | Checked | unowned | PrimeNumberTheoremAnd/LaplaceInversion.lean | |
| _abel_1_1 | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/Kadiri.lean | |
| _abel_1_1 | Checked | unowned | PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean | |
| _abel_1_1 | Checked | unowned | PrimeNumberTheoremAnd/LaplaceInversion.lean | |
| _abel_1_1 | Checked | unowned | PrimeNumberTheoremAnd/LaplaceInversion.lean | |
| _abel_1_1 | Checked | unowned | PrimeNumberTheoremAnd/LaplaceInversion.lean | |
| _abel_1_12 | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/MobiusLemma.lean | |
| _abel_1_2 | Checked | unowned | PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean | |
| _abel_1_2 | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/Kadiri.lean | |
| _abel_1_3 | Checked | unowned | PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean | |
| _abel_1_3 | Checked | unowned | PrimeNumberTheoremAnd/Wiener.lean | |
| _abel_1_4 | Checked | unowned | PrimeNumberTheoremAnd/Wiener.lean | |
| _abel_1_4 | Checked | unowned | PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean | |
| _abel_1_9 | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean | |
| abel_formula | Checked | unowned | PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZetaPartialSum.lean | |
| abel_split | Checked | unowned | PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZetaPartialSum.lean | |
| abel_sub_fract | Checked | unowned | PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZetaPartialSum.lean | |
| abel_summation | Checked | unowned | PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZetaPartialSum.lean | |
| a_bound | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/Chebyshev.lean | |
| abs_B1_le_half | Checked | unowned | PrimeNumberTheoremAnd/EulerMaclaurin.lean | |
| abscissa_powR_le | Checked | unowned | PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean | |
| abs_E₂Λ_le_const | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/Mertens.lean | |
| abs_E₂Λ_le_on_Ioo | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/Mertens.lean | |
| abs_le | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/Mertens.lean | |
| abs_le | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/Mertens.lean | |
| abs_le | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/Mertens.lean | |
| abs_le_max_abs_of_mem_uIcc | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/LiSeries.lean | |
| abs_log_dyadic_div_two_pi_le | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean | |
| abs_mul_exp_isBigO | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.lean | |
| abs_rem_le | Checked | unowned | PrimeNumberTheoremAnd/BrunTitchmarsh.lean | |
| abs_setIntegral_Iic_le | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean | |
| abs_sum_le | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/Chebyshev.lean | |
| abs_zetaCountingMainTerm_core_le | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean | |
| add | Checked | unowned | PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean | |
| add_const | Checked | unowned | PrimeNumberTheoremAnd/Wiener.lean | |
| addFactor_balance | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/Erdos392.lean | |
| addFactor_deficit_balance_eq_zero | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/Erdos392.lean | |
| addFactor_submultiset_total_imbalance | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/Erdos392.lean | |
| addFactor_waste | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/Erdos392.lean | |
| add_four_le_add_two_mul_of_le | Checked | unowned | PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/CartanMajorantBound.lean | |
| add_isLittleO' | Checked | unowned | PrimeNumberTheoremAnd/Consequences.lean | |
| add_isLittleO'' | Checked | unowned | PrimeNumberTheoremAnd/Consequences.lean | |
| add_isLittleO_right | Checked | unowned | PrimeNumberTheoremAnd/Wiener.lean | |
| admissible_bound_anti | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/FKS2.lean | |
| admissible_bound_le_0826 | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/FKS2.lean | |
| admissible_bound_mul | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/FKS2.lean | |
| admissible_bound_pos | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/FKS2.lean | |
| admissible_bound_weaken | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean | |
| admissible_contour_subset_R | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean | |
| admissible_contour_subset_R4 | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean | |
| admissible_contour_subset_RC | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean | |
| ae_bound_Ioi | Checked | unowned | PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZetaAbelKernel.lean | |
| ae_eq_NF_vseg | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean | |
| ae_eq_NF_vseg_general | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean | |
| ae_eq_of_codiscreteWithin_along_path | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean | |
| ae_norm_Phi_lambda_bot_hray_le | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean | |
| ae_norm_Phi_lambda_top_hray_le | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean | |
| ae_one_sub_div_ne | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean | |
| ae_on_Ioi_of_all | Checked | unowned | PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZetaAbelKernel.lean | |
| a_eq_admissible_ge_3000 | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean | |
| ae_restrict_norm_phi_le_of_forall_mem | Checked | unowned | PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/CartanBound.lean | |
| aestronglyMeasurable | Checked | unowned | PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZetaAbelKernel.lean | |
| aestronglyMeasurable_B1 | Checked | unowned | PrimeNumberTheoremAnd/EulerMaclaurin.lean | |
| aestronglyMeasurable_horizontal_path_mul_cpow_of_meromorphic | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean | |
| aestronglyMeasurable_hray_of_meromorphic | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean | |
| aestronglyMeasurable_param_deriv | Checked | unowned | PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZetaAbelKernel.lean | |
| ae_volume_of_contains_compl_singleton_zero | Checked | unowned | PrimeNumberTheoremAnd/MediumPNT.lean | |
| a_exa_upper_tight | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean | |
| a_exp_upper | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean | |
| a_exp_upper_of | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/Ramanujan/RamanujanCalculations.lean | |
| a_le_low_huge | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean | |
| allCells_chain | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean | |
| allCells_checked | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean | |
| allCells_last | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean | |
| allCells_ne_nil | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean | |
| allCells_trusted | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean | |
| allChecks_11723 | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/Chebyshev.lean | |
| allThetaChecks_3_599 | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean | |
| alpha_eq | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean | |
| a_mono | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean | |
| a_mono_3000 | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean | |
| analyticAt_B | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean | |
| analyticAt_conj_conj | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean | |
| analyticAt_conj_reflect | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean | |
| analyticAt_divisorCanonicalProduct_univ | Checked | unowned | PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/HadamardFactorization.lean | |
| analyticAt_divisorPartialProduct | Checked | unowned | PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/DivisorComplement.lean | |
| analyticAt_finset_prod_sub_pow | Checked | unowned | PrimeNumberTheoremAnd/StrongPNT.lean | |
| analyticAt_of_im_gt_pole | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean | |
| analyticAt_of_im_gt_pole | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean | |
| analyticAt_of_im_ne_pole | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean | |
| analyticAt_of_im_ne_pole | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean | |
| analyticAt_of_im_nonneg | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean | |
| analyticAt_of_im_nonneg | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean | |
| analyticAt_of_not_pole | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean | |
| analyticAt_of_not_pole | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean | |
| analyticAt_of_not_pole_nz | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean | |
| analyticAt_of_re_ne_int | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean | |
| analyticAt_of_re_ne_int | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean | |
| analyticAt_removable_sing_mul_E | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean | |
| analyticAt_riemannZeta | Checked | unowned | PrimeNumberTheoremAnd/ZetaBounds.lean | |
| analyticAt_rpow | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean | |
| analyticAt_tanh | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean | |
| analyticAt_update_limUnder_divisorCanonicalProduct_div_pow | Checked | unowned | PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/DivisorQuotientRemovable.lean | |
| analyticAt_zOf | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean | |
| analytic_deriv_bounded_near_point | Checked | unowned | PrimeNumberTheoremAnd/ZetaBounds.lean | |
| analytic_mul | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean | |
| analyticOn_deriv_z_coth_z | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean | |
| AnalyticOn_divRemovable_zero | Checked | unowned | PrimeNumberTheoremAnd/BorelCaratheodory.lean | |
| AnalyticOn_divRemovable_zero_closedBall | Checked | unowned | PrimeNumberTheoremAnd/BorelCaratheodory.lean | |
| analyticOn_dslope_deriv_z_coth_z_zero | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean | |
| analyticOnNhd | Checked | unowned | PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/CauchyIntegral.lean | |
| analyticOnNhd_canonicalProduct | Checked | unowned | PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/CanonicalProduct.lean | |
| analyticOn_zetaAbelContinuationFormula | Checked | unowned | PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZetaAbelContinuation.lean | |
| analyticOrderAt_conj_conj | Checked | unowned | PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean | |
| analyticOrderAt_divisorCanonicalProduct_at_index | Checked | unowned | PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/Divisor.lean | |
| analyticOrderAt_divisorCanonicalProduct_eq_fiber_card | Checked | unowned | PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/Divisor.lean | |
| analyticOrderAt_finset_prod_weierstrassFactor_divisorZeroIndex₀ | Checked | unowned | PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/DivisorPartialProductFactor.lean | |
| analyticOrderAt_ne_top_of_exists_ne_zero | Checked | unowned | PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/Divisor.lean | |
| analyticOrderAt_partialProduct_eq_fiberCard_of_subset | Checked | unowned | PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/DivisorPartialProductFactor.lean | |
| analyticOrderAt_prod_fiberFinset | Checked | unowned | PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/Divisor.lean | |
| analyticOrderAt_weierstrassFactor_div_self | Checked | unowned | PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/WeierstrassFactor.lean | |
| analyticOrderNatAt_comp_add_const | Checked | unowned | PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/HadamardFactorization/Order.lean | |
| analyticOrderNatAt_completedRiemannZeta₀_zero | Checked | unowned | PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZetaHadamard.lean | |
| analyticOrderNatAt_comp_sub_const | Checked | unowned | PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/HadamardFactorization/Order.lean | |
| analyticOrderNatAt_divisorCanonicalProduct_eq_analyticOrderNatAt | Checked | unowned | PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/DivisorQuotientRemovable.lean | |
| analyticOrderNatAt_divisorCanonicalProduct_eq_fiber_card | Checked | unowned | PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/DivisorQuotientRemovable.lean |
No theorems match the active view.
Showing the highest-priority 200 proofs for fast server render.