ZetaBounds

📁 Source: PrimeNumberTheoremAnd/ZetaBounds.lean

Statistics

Metric	Count
Definitions riemannZeta0, ζ₀'	2
Theorems BddAbove_to_IsBigO, cpow_inv_tendsto, cpow_tendsto, one_div_cpow_eq, continuousOn_deriv, hasDeriv_deriv, DerivUpperBnd_aux1, DerivUpperBnd_aux2, DerivUpperBnd_aux3, DerivUpperBnd_aux4, DerivUpperBnd_aux5, DerivUpperBnd_aux6, DerivUpperBnd_aux7, DerivUpperBnd_aux7_1, DerivUpperBnd_aux7_2, DerivUpperBnd_aux7_3, DerivUpperBnd_aux7_3', DerivUpperBnd_aux7_4, DerivUpperBnd_aux7_5, DerivUpperBnd_aux7_integral_eq, DerivUpperBnd_aux7_nonneg, DerivUpperBnd_aux7_tendsto, DerivZeta0EqDerivZeta, Icc0_eq, Icc_eq_Ico, Ioc_eq_Icc, Ioc_eq_Ico, Finset_coe_Nat_Int, HasDerivAtZeta0, HasDerivAt_cpow_over_var, HasDerivAt_neg_cpow_over2, HolomophicOn_riemannZeta, HolomorphicOn_riemannZeta0, Ioi_union_Iio_mem_cocompact, LinearDerivative_ofReal, LogDerivZetaBnd, LogDerivZetaBndUnif, LogDerivZetaHolcLargeT, LogDerivZetaHolcSmallT, LogDerivZetaHoloOn, self_div_floor_bound, differentiableAt_cpow_const_of_ne, log_natCast_monotone, ResidueMult, ResidueOfTendsTo, Tendsto_nhdsWithin_punctured_add, Tendsto_nhdsWithin_punctured_map_add, UpperBnd_aux, UpperBnd_aux2, UpperBnd_aux3, UpperBnd_aux5, UpperBnd_aux6, Zeta0EqZeta, ZetaBnd_aux1, ZetaBnd_aux1a, ZetaBnd_aux1b, ZetaBnd_aux1p, ZetaBnd_aux2, ZetaCont, ZetaDerivUpperBnd, ZetaDerivUpperBnd', ZetaInvBnd, ZetaInvBnd_aux, ZetaInvBnd_aux', ZetaInvBnd_aux2, ZetaInvBound1, ZetaInvBound2, ZetaLowerBnd, ZetaLowerBound1, ZetaLowerBound1_aux1, ZetaLowerBound2, ZetaLowerBound3, ZetaLowerBound3_aux1, ZetaLowerBound3_aux2, ZetaLowerBound3_aux3, ZetaLowerBound3_aux4, ZetaLowerBound3_aux5, ZetaNear1BndExact, ZetaNear1BndFilter, ZetaNoZerosInBox, ZetaNoZerosOn1Line, ZetaSum_aux1, ZetaSum_aux1_1, ZetaSum_aux1_1', ZetaSum_aux1_2, ZetaSum_aux1_3, ZetaSum_aux1_3a, ZetaSum_aux1_3b, ZetaSum_aux1_4, ZetaSum_aux1_4', ZetaSum_aux1_5, ZetaSum_aux1_5a, ZetaSum_aux1_5b, ZetaSum_aux1_5c, ZetaSum_aux1_5d, ZetaSum_aux1derivφCont, ZetaSum_aux1φDiff, ZetaSum_aux1φderiv, ZetaSum_aux1₁, ZetaSum_aux2, ZetaSum_aux2a, ZetaSum_aux3, ZetaUpperBnd, ZetaUpperBnd', ZetaZeroFree, Zeta_diff_Bnd, Zeta_eq_int_derivZeta, add_le_add_le_add, add_le_add_le_add_le_add, analyticAt_riemannZeta, analytic_deriv_bounded_near_point, deriv_eqOn_of_eqOn_punctured, deriv_f_minus_A_inv_sub_clean, deriv_fun_re, deriv_inv_sub, derivative_const_plus_product, diff_translation, differentiableAt_deriv_riemannZeta, div_cpow_eq_cpow_neg, div_rpow_eq_rpow_div_neg, div_rpow_eq_rpow_neg, div_rpow_neg_eq_rpow_div, dlog_riemannZeta_bdd_on_vertical_lines_generalized, finsetSum_tendsto_tsum, harmonic_eq_sum_Icc0, harmonic_eq_sum_Icc0_aux, hasDerivAt_Zeta0Integral, integrability_aux, integrability_aux₀, integrability_aux₁, integrability_aux₂, integrableOn_of_Zeta0_fun, integrableOn_of_Zeta0_fun_log, integrable_log_over_pow, isOpen_aux, isPathConnected_aux, le_trans₄, logDerivResidue, logDerivResidue', logDerivResidue'', logt_gt_one, lt_abs_mem_cocompact, lt_trans₄, measurable_floor_add_half_sub, mul_le_mul₃, neg_s_ne_neg_one, nonZeroOfBddAbove, norm_add₄_le, norm_add₅_le, norm_add₆_le, norm_complex_log_ofNat, norm_zeta_product_ge_one, one_div_cpow_eq_cpow_neg, riemannZeta0_apply, riemannZeta0_zero_aux, riemannZetaLogDerivResidue, riemannZetaLogDerivResidueBigO, riemannZetaResidue, riemannZeta_isBigO_near_one_horizontal, sum_eq_int_deriv, sum_eq_int_deriv_aux2, summable_complex_then_summable_real_part, triv_bound_zeta, tsum_eq_partial_add_tail, xpos_of_uIcc	165
Total	167

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cpow_inv_tendsto 📖	—	—	—	—	—
cpow_tendsto 📖	—	—	—	—	—
one_div_cpow_eq 📖	—	—	—	—	—

ContDiffOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousOn_deriv 📖	—	—	—	—	—
hasDeriv_deriv 📖	—	—	—	—	—

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Icc0_eq 📖	—	—	—	—	—
Icc_eq_Ico 📖	—	—	—	—	—
Ioc_eq_Icc 📖	—	—	—	—	—
Ioc_eq_Ico 📖	—	—	—	—	—

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
self_div_floor_bound 📖	—	—	—	—	—

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
differentiableAt_cpow_const_of_ne 📖	—	—	—	—	DifferentiableAt.comp_ofReal
log_natCast_monotone 📖	—	—	—	—	—

(root)

Definitions

Name	Category	Theorems
riemannZeta0 📖	CompOp	5 math math: DerivZeta0EqDerivZeta, HasDerivAtZeta0, Zeta0EqZeta, HolomorphicOn_riemannZeta0, riemannZeta0_apply
ζ₀' 📖	CompOp	1 math math: HasDerivAtZeta0

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
BddAbove_to_IsBigO 📖	—	—	—	—	—
DerivUpperBnd_aux1 📖	—	—	—	—	UpperBnd_aux logt_gt_one ZetaBnd_aux2 norm_complex_log_ofNat Finset.Icc_eq_Ico harmonic_eq_sum_Icc0
DerivUpperBnd_aux2 📖	—	—	—	—	UpperBnd_aux6 UpperBnd_aux2
DerivUpperBnd_aux3 📖	—	—	—	—	UpperBnd_aux6 UpperBnd_aux2 norm_complex_log_ofNat
DerivUpperBnd_aux4 📖	—	—	—	—	UpperBnd_aux6 UpperBnd_aux2 norm_complex_log_ofNat
DerivUpperBnd_aux5 📖	—	—	—	—	ZetaBnd_aux1 div_cpow_eq_cpow_neg
DerivUpperBnd_aux6 📖	—	—	—	—	UpperBnd_aux6 UpperBnd_aux2
DerivUpperBnd_aux7 📖	—	—	—	—	DerivUpperBnd_aux7_1 DerivUpperBnd_aux7_5 DerivUpperBnd_aux7_4 DerivUpperBnd_aux7_2 DerivUpperBnd_aux7_integral_eq logt_gt_one
DerivUpperBnd_aux7_1 📖	—	—	—	—	—
DerivUpperBnd_aux7_2 📖	—	—	—	—	ZetaSum_aux1_3
DerivUpperBnd_aux7_3 📖	—	—	—	—	—
DerivUpperBnd_aux7_3' 📖	—	—	—	—	DerivUpperBnd_aux7_3
DerivUpperBnd_aux7_4 📖	—	—	—	—	DerivUpperBnd_aux7_3' DerivUpperBnd_aux7_nonneg DerivUpperBnd_aux7_tendsto
DerivUpperBnd_aux7_5 📖	—	—	—	—	DerivUpperBnd_aux7_4 measurable_floor_add_half_sub ZetaSum_aux1_3
DerivUpperBnd_aux7_integral_eq 📖	—	—	—	—	DerivUpperBnd_aux7_3' DerivUpperBnd_aux7_nonneg DerivUpperBnd_aux7_tendsto
DerivUpperBnd_aux7_nonneg 📖	—	—	—	—	—
DerivUpperBnd_aux7_tendsto 📖	—	—	—	—	Real.tendsto_pow_log_div_pow_atTop div_rpow_eq_rpow_neg
DerivZeta0EqDerivZeta 📖	mathematical	—	riemannZeta0	—	Zeta0EqZeta isOpen_aux HolomophicOn_riemannZeta
Finset_coe_Nat_Int 📖	—	—	—	—	—
HasDerivAtZeta0 📖	mathematical	—	riemannZeta0 ζ₀'	—	HasDerivAt_cpow_over_var HasDerivAt_neg_cpow_over2 div_cpow_eq_cpow_neg hasDerivAt_Zeta0Integral
HasDerivAt_cpow_over_var 📖	—	—	—	—	—
HasDerivAt_neg_cpow_over2 📖	—	—	—	—	—
HolomophicOn_riemannZeta 📖	mathematical	—	HolomorphicOn	—	—
HolomorphicOn_riemannZeta0 📖	mathematical	—	HolomorphicOn riemannZeta0	—	HasDerivAtZeta0
Ioi_union_Iio_mem_cocompact 📖	—	—	—	—	—
LinearDerivative_ofReal 📖	—	—	—	—	—
LogDerivZetaBnd 📖	—	—	—	—	ZetaInvBnd ZetaDerivUpperBnd logt_gt_one
LogDerivZetaBndUnif 📖	—	—	—	—	LogDerivZetaBnd triv_bound_zeta logt_gt_one ZetaInvBnd_aux
LogDerivZetaHolcLargeT 📖	mathematical	—	HolomorphicOn	—	ZetaZeroFree ZetaNoZerosInBox LogDerivZetaHoloOn
LogDerivZetaHolcSmallT 📖	mathematical	—	HolomorphicOn	—	ZetaNoZerosInBox LogDerivZetaHoloOn
LogDerivZetaHoloOn 📖	mathematical	—	HolomorphicOn	—	differentiableAt_deriv_riemannZeta
ResidueMult 📖	—	HolomorphicOn	—	—	—
ResidueOfTendsTo 📖	—	HolomorphicOn	—	—	existsDifferentiableOn_of_bddAbove IsBigO_to_BddAbove
Tendsto_nhdsWithin_punctured_add 📖	—	—	—	—	Tendsto_nhdsWithin_punctured_map_add
Tendsto_nhdsWithin_punctured_map_add 📖	—	—	—	—	—
UpperBnd_aux 📖	—	—	—	—	logt_gt_one
UpperBnd_aux2 📖	—	—	—	—	—
UpperBnd_aux3 📖	—	—	—	—	UpperBnd_aux logt_gt_one ZetaBnd_aux2 riemannZeta0_zero_aux
UpperBnd_aux5 📖	—	—	—	—	Nat.self_div_floor_bound
UpperBnd_aux6 📖	—	—	—	—	UpperBnd_aux5 div_rpow_eq_rpow_div_neg le_trans₄ div_rpow_neg_eq_rpow_div
Zeta0EqZeta 📖	mathematical	—	riemannZeta0	—	HolomophicOn_riemannZeta HolomorphicOn_riemannZeta0 isOpen_aux isPathConnected_aux riemannZeta0_apply ZetaSum_aux2
ZetaBnd_aux1 📖	—	—	—	—	ZetaBnd_aux1b
ZetaBnd_aux1a 📖	—	—	—	—	ZetaSum_aux1_4 ZetaSum_aux1_5 ZetaSum_aux1_2 ZetaSum_aux1_1
ZetaBnd_aux1b 📖	—	—	—	—	integrableOn_of_Zeta0_fun ZetaBnd_aux1a
ZetaBnd_aux1p 📖	—	—	—	—	ZetaBnd_aux1b
ZetaBnd_aux2 📖	—	—	—	—	—
ZetaCont 📖	—	—	—	—	—
ZetaDerivUpperBnd 📖	—	—	—	—	ZetaUpperBnd UpperBnd_aux DerivZeta0EqDerivZeta HasDerivAtZeta0 norm_add₆_le ZetaDerivUpperBnd'
ZetaDerivUpperBnd' 📖	—	—	—	—	UpperBnd_aux DerivUpperBnd_aux1 DerivUpperBnd_aux2 DerivUpperBnd_aux3 DerivUpperBnd_aux4 DerivUpperBnd_aux5 DerivUpperBnd_aux6 DerivUpperBnd_aux7
ZetaInvBnd 📖	—	—	—	—	ZetaInvBound2 Zeta_diff_Bnd ZetaInvBnd_aux2 logt_gt_one ZetaInvBnd_aux UpperBnd_aux lt_trans₄ ZetaInvBnd_aux'
ZetaInvBnd_aux 📖	—	—	—	—	ZetaInvBnd_aux'
ZetaInvBnd_aux' 📖	—	—	—	—	—
ZetaInvBnd_aux2 📖	—	—	—	—	—
ZetaInvBound1 📖	—	—	—	—	norm_zeta_product_ge_one
ZetaInvBound2 📖	—	—	—	—	ZetaUpperBnd ZetaNear1BndExact ZetaInvBound1
ZetaLowerBnd 📖	—	—	—	—	ZetaLowerBound3 Zeta_diff_Bnd logt_gt_one
ZetaLowerBound1 📖	—	—	—	—	norm_zeta_product_ge_one ZetaLowerBound1_aux1
ZetaLowerBound1_aux1 📖	—	—	—	—	—
ZetaLowerBound2 📖	—	—	—	—	ZetaLowerBound1
ZetaLowerBound3 📖	—	—	—	—	ZetaUpperBnd ZetaNear1BndExact ZetaLowerBound2 ZetaLowerBound3_aux1 ZetaLowerBound3_aux2 ZetaLowerBound3_aux3 ZetaLowerBound3_aux4 ZetaLowerBound3_aux5 ZetaLowerBound1
ZetaLowerBound3_aux1 📖	—	—	—	—	—
ZetaLowerBound3_aux2 📖	—	—	—	—	—
ZetaLowerBound3_aux3 📖	—	—	—	—	—
ZetaLowerBound3_aux4 📖	—	—	—	—	—
ZetaLowerBound3_aux5 📖	—	—	—	—	—
ZetaNear1BndExact 📖	—	—	—	—	ZetaNear1BndFilter
ZetaNear1BndFilter 📖	—	—	—	—	Tendsto_nhdsWithin_punctured_add riemannZeta_isBigO_near_one_horizontal
ZetaNoZerosInBox 📖	—	—	—	—	ZetaCont
ZetaNoZerosOn1Line 📖	—	—	—	—	—
ZetaSum_aux1 📖	—	—	—	—	xpos_of_uIcc ZetaSum_aux1φDiff ZetaSum_aux1φderiv ZetaSum_aux1derivφCont ZetaSum_aux1₁ sum_eq_int_deriv
ZetaSum_aux1_1 📖	—	—	—	—	—
ZetaSum_aux1_1' 📖	—	—	—	—	—
ZetaSum_aux1_2 📖	—	—	—	—	ZetaSum_aux1_1 div_rpow_eq_rpow_neg
ZetaSum_aux1_3 📖	—	—	—	—	ZetaSum_aux1_3a ZetaSum_aux1_3b
ZetaSum_aux1_3a 📖	—	—	—	—	—
ZetaSum_aux1_3b 📖	—	—	—	—	—
ZetaSum_aux1_4 📖	—	—	—	—	ZetaSum_aux1_4' ZetaSum_aux1_1
ZetaSum_aux1_4' 📖	—	—	—	—	—
ZetaSum_aux1_5 📖	—	—	—	—	ZetaSum_aux1_5d ZetaSum_aux1_5b ZetaSum_aux1_5a
ZetaSum_aux1_5a 📖	—	—	—	—	ZetaSum_aux1_3 ZetaSum_aux1_1'
ZetaSum_aux1_5b 📖	—	—	—	—	ZetaSum_aux1_1'
ZetaSum_aux1_5c 📖	—	—	—	—	measurable_floor_add_half_sub
ZetaSum_aux1_5d 📖	—	—	—	—	ZetaSum_aux1_5b ZetaSum_aux1_5c ZetaSum_aux1_3
ZetaSum_aux1derivφCont 📖	—	—	—	—	ZetaSum_aux1φderiv xpos_of_uIcc
ZetaSum_aux1φDiff 📖	—	—	—	—	Real.differentiableAt_cpow_const_of_ne
ZetaSum_aux1φderiv 📖	—	—	—	—	—
ZetaSum_aux1₁ 📖	—	—	—	—	Complex.one_div_cpow_eq xpos_of_uIcc neg_s_ne_neg_one
ZetaSum_aux2 📖	—	—	—	—	Finset_coe_Nat_Int ZetaSum_aux1 ZetaSum_aux3 Complex.cpow_tendsto Complex.cpow_inv_tendsto integrableOn_of_Zeta0_fun
ZetaSum_aux2a 📖	—	—	—	—	ZetaSum_aux1_3
ZetaSum_aux3 📖	—	—	—	—	Finset.Ioc_eq_Ico finsetSum_tendsto_tsum
ZetaUpperBnd 📖	—	—	—	—	UpperBnd_aux Zeta0EqZeta norm_add₄_le ZetaUpperBnd'
ZetaUpperBnd' 📖	—	—	—	—	UpperBnd_aux one_div_cpow_eq_cpow_neg UpperBnd_aux3 ZetaBnd_aux1 UpperBnd_aux6 add_le_add_le_add_le_add UpperBnd_aux2
ZetaZeroFree 📖	—	—	—	—	ZetaLowerBnd
Zeta_diff_Bnd 📖	—	—	—	—	ZetaDerivUpperBnd Zeta_eq_int_derivZeta
Zeta_eq_int_derivZeta 📖	—	—	—	—	deriv_fun_re Complex.differentiableAt_ofReal differentiableAt_deriv_riemannZeta
add_le_add_le_add 📖	—	—	—	—	—
add_le_add_le_add_le_add 📖	—	—	—	—	add_le_add_le_add
analyticAt_riemannZeta 📖	—	—	—	—	—
analytic_deriv_bounded_near_point 📖	—	HolomorphicOn	—	—	—
deriv_eqOn_of_eqOn_punctured 📖	—	—	—	—	—
deriv_f_minus_A_inv_sub_clean 📖	—	—	—	—	deriv_inv_sub
deriv_fun_re 📖	—	—	—	—	Complex.differentiableAt_ofReal deriv_ofReal
deriv_inv_sub 📖	—	—	—	—	diff_translation
derivative_const_plus_product 📖	—	—	—	—	—
diff_translation 📖	—	—	—	—	—
differentiableAt_deriv_riemannZeta 📖	—	—	—	—	analyticAt_riemannZeta
div_cpow_eq_cpow_neg 📖	—	—	—	—	—
div_rpow_eq_rpow_div_neg 📖	—	—	—	—	div_rpow_neg_eq_rpow_div
div_rpow_eq_rpow_neg 📖	—	—	—	—	—
div_rpow_neg_eq_rpow_div 📖	—	—	—	—	—
dlog_riemannZeta_bdd_on_vertical_lines_generalized 📖	—	—	—	—	summable_complex_then_summable_real_part
finsetSum_tendsto_tsum 📖	—	—	—	—	tsum_eq_partial_add_tail
harmonic_eq_sum_Icc0 📖	—	—	—	—	harmonic_eq_sum_Icc0_aux
harmonic_eq_sum_Icc0_aux 📖	—	—	—	—	Finset.Icc0_eq
hasDerivAt_Zeta0Integral 📖	—	—	—	—	integrableOn_of_Zeta0_fun integrableOn_of_Zeta0_fun_log ZetaSum_aux1_3 integrable_log_over_pow
integrability_aux 📖	—	—	—	—	integrability_aux₁ integrability_aux₂
integrability_aux₀ 📖	—	—	—	—	—
integrability_aux₁ 📖	—	—	—	—	integrability_aux₀
integrability_aux₂ 📖	—	—	—	—	—
integrableOn_of_Zeta0_fun 📖	—	—	—	—	ZetaSum_aux2a
integrableOn_of_Zeta0_fun_log 📖	—	—	—	—	ZetaSum_aux2a integrable_log_over_pow
integrable_log_over_pow 📖	—	—	—	—	—
isOpen_aux 📖	—	—	—	—	—
isPathConnected_aux 📖	—	—	—	—	—
le_trans₄ 📖	—	—	—	—	—
logDerivResidue 📖	—	HolomorphicOn	—	—	logDerivResidue'
logDerivResidue' 📖	—	HolomorphicOn	—	—	existsDifferentiableOn_of_bddAbove derivative_const_plus_product deriv_eqOn_of_eqOn_punctured deriv_f_minus_A_inv_sub_clean analytic_deriv_bounded_near_point
logDerivResidue'' 📖	—	HolomorphicOn	—	—	IsBigO_to_BddAbove logDerivResidue
logt_gt_one 📖	—	—	—	—	—
lt_abs_mem_cocompact 📖	—	—	—	—	Ioi_union_Iio_mem_cocompact
lt_trans₄ 📖	—	—	—	—	—
measurable_floor_add_half_sub 📖	—	—	—	—	—
mul_le_mul₃ 📖	—	—	—	—	—
neg_s_ne_neg_one 📖	—	—	—	—	—
nonZeroOfBddAbove 📖	—	—	—	—	—
norm_add₄_le 📖	—	—	—	—	—
norm_add₅_le 📖	—	—	—	—	norm_add₄_le
norm_add₆_le 📖	—	—	—	—	norm_add₅_le
norm_complex_log_ofNat 📖	—	—	—	—	—
norm_zeta_product_ge_one 📖	—	—	—	—	—
one_div_cpow_eq_cpow_neg 📖	—	—	—	—	div_cpow_eq_cpow_neg
riemannZeta0_apply 📖	mathematical	—	riemannZeta0	—	div_cpow_eq_cpow_neg
riemannZeta0_zero_aux 📖	—	—	—	—	—
riemannZetaLogDerivResidue 📖	—	—	—	—	riemannZetaResidue nonZeroOfBddAbove logDerivResidue''
riemannZetaLogDerivResidueBigO 📖	—	—	—	—	riemannZetaLogDerivResidue BddAbove_to_IsBigO
riemannZetaResidue 📖	—	—	—	—	ResidueOfTendsTo
riemannZeta_isBigO_near_one_horizontal 📖	—	—	—	—	—
sum_eq_int_deriv 📖	—	—	—	—	Finset_coe_Nat_Int integrability_aux sum_eq_int_deriv_aux2
sum_eq_int_deriv_aux2 📖	—	—	—	—	LinearDerivative_ofReal
summable_complex_then_summable_real_part 📖	—	—	—	—	—
triv_bound_zeta 📖	—	—	—	—	riemannZetaLogDerivResidue dlog_riemannZeta_bdd_on_vertical_lines_generalized
tsum_eq_partial_add_tail 📖	—	—	—	—	—
xpos_of_uIcc 📖	—	—	—	—	—

---

← Back to Index