CH2

📁 Source: PrimeNumberTheoremAnd/CH2.lean

Statistics

Metric	Count
Definitions B, E, I, I', Phi_circ, Phi_star, S, coth, ϕ_pm	9
Theorems continuous_zero, B_affine_periodic, B_im_eq_zero, B_minus_mono, B_minus_real, B_plus_mono, B_plus_real, CH2_lemma_4_2a, CH2_lemma_4_2b, div_real_complex, Inu_bounds, Phi_cancel, contDiff_real, meromorphic, poles, poles_simple, residue, contDiff_real, meromorphic, poles, poles_simple, residue, Phi_star_zero, S_eq_I, cont_E, cor_1_2_a, cor_1_2_b, cor_1_3_a, cor_1_3_b, cosh_zero_iff, first_contour_limit, fourier_formula_neg, fourier_formula_pos, fourier_real, fourier_scale_div_noscalar, fun_meromorphicOrderAt_div, meromorphicAt_B, meromorphicOrderAt_div, meromorphic_coth, meromorphic_coth', meromorphic_coth'', meromorphic_tanh, phi_star_affine_periodic, prop_2_3, prop_2_3_1, prop_2_4_minus, prop_2_4_plus, second_contour_limit, shift_downwards, shift_downwards_simplified, shift_upwards, shift_upwards_simplified, sinh_zero_iff, summable_nterm_of_log_weight, third_contour_limit, varphi_abs, varphi_deriv_integ, varphi_deriv_tv, varphi_fourier_decay, varphi_fourier_ident, varphi_fourier_minus_error, varphi_fourier_plus_error, varphi_integ, ϕ_c2_left, ϕ_c2_right, ϕ_circ_bound_left, ϕ_circ_bound_right, ϕ_continuous, ϕ_star_bound_left, ϕ_star_bound_right	70
Total	79
⚠️ With sorry CH2_lemma_4_2a, CH2_lemma_4_2b, Inu_bounds, poles, cor_1_2_a, cor_1_2_b, cor_1_3_a, cor_1_3_b, first_contour_limit, fourier_formula_neg, fourier_formula_pos, fourier_real, prop_2_3, prop_2_4_minus, prop_2_4_plus, second_contour_limit, shift_downwards, shift_downwards_simplified, shift_upwards, shift_upwards_simplified, third_contour_limit, varphi_abs, varphi_deriv_integ, varphi_deriv_tv, varphi_fourier_decay, varphi_fourier_minus_error, varphi_fourier_plus_error, varphi_integ	28

CH2

Definitions

Name	Category	Theorems
B 📖	CompOp	12 math math: fourier_formula_pos, B.continuous_zero, B_plus_mono, B_minus_mono, B_minus_real, shift_upwards_simplified, B_plus_real, B_affine_periodic, meromorphicAt_B, shift_downwards_simplified, B_im_eq_zero, fourier_formula_neg
E 📖	CompOp	7 math math: cont_E, first_contour_limit, shift_upwards, third_contour_limit, varphi_fourier_ident, second_contour_limit, shift_downwards
I 📖	CompOp	3 math math: varphi_fourier_plus_error, Inu_bounds, varphi_fourier_minus_error
I' 📖	CompOp	1 math math: S_eq_I
Phi_circ 📖	CompOp	14 math math: Phi_circ.poles_simple, Phi_circ.poles, first_contour_limit, ϕ_circ_bound_right, phi_star_affine_periodic, Phi_circ.meromorphic, Phi_circ.residue, shift_upwards, Phi_cancel, varphi_fourier_ident, ϕ_circ_bound_left, Phi_circ.contDiff_real, B_affine_periodic, shift_downwards
Phi_star 📖	CompOp	15 math math: Phi_star.meromorphic, phi_star_affine_periodic, Phi_star_zero, Phi_star.poles_simple, Phi_star.contDiff_real, shift_upwards, Phi_cancel, Phi_star.poles, ϕ_star_bound_left, third_contour_limit, varphi_fourier_ident, Phi_star.residue, ϕ_star_bound_right, second_contour_limit, shift_downwards
S 📖	CompOp	3 math math: S_eq_I, prop_2_4_minus, prop_2_4_plus
coth 📖	CompOp	4 math math: CH2_lemma_4_2a, cor_1_2_a, CH2_lemma_4_2b, meromorphic_coth
ϕ_pm 📖	CompOp	19 math math: fourier_formula_pos, varphi_deriv_integ, varphi_deriv_tv, ϕ_c2_left, varphi_integ, varphi_fourier_decay, varphi_abs, fourier_real, varphi_fourier_plus_error, shift_upwards, shift_upwards_simplified, ϕ_c2_right, Inu_bounds, varphi_fourier_minus_error, varphi_fourier_ident, ϕ_continuous, shift_downwards_simplified, shift_downwards, fourier_formula_neg

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
B_affine_periodic 📖	mathematical	—	B Phi_circ	—	—
B_im_eq_zero 📖	mathematical	—	B	—	coth.eq_1
B_minus_mono 📖	mathematical	—	B	—	—
B_minus_real 📖	mathematical	—	B	—	B_im_eq_zero
B_plus_mono 📖	mathematical	—	B	—	—
B_plus_real 📖	mathematical	—	B	—	B_im_eq_zero
CH2_lemma_4_2a 📖 ⚠️	mathematical	—	coth	—	—
CH2_lemma_4_2b 📖 ⚠️	mathematical	—	coth	—	—
Inu_bounds 📖 ⚠️	mathematical	—	ϕ_pm I	—	—
Phi_cancel 📖	mathematical	—	Phi_circ Phi_star	—	Phi_circ.meromorphic Phi_star.meromorphic Phi_circ.residue Phi_star.residue
Phi_star_zero 📖	mathematical	—	Phi_star	—	—
S_eq_I 📖	mathematical	—	S I'	—	—
cont_E 📖	mathematical	—	E	—	—
cor_1_2_a 📖 ⚠️	mathematical	—	coth	—	—
cor_1_2_b 📖 ⚠️	—	—	—	—	—
cor_1_3_a 📖 ⚠️	—	—	—	—	—
cor_1_3_b 📖 ⚠️	—	—	—	—	—
cosh_zero_iff 📖	—	—	—	—	—
first_contour_limit 📖 ⚠️	mathematical	—	Phi_circ E	—	—
fourier_formula_neg 📖 ⚠️	mathematical	—	B ϕ_pm	—	—
fourier_formula_pos 📖 ⚠️	mathematical	—	B ϕ_pm	—	—
fourier_real 📖 ⚠️	mathematical	—	ϕ_pm	—	—
fourier_scale_div_noscalar 📖	—	—	—	—	—
fun_meromorphicOrderAt_div 📖	—	—	—	—	meromorphicOrderAt_div
meromorphicAt_B 📖	mathematical	—	B	—	meromorphic_coth''
meromorphicOrderAt_div 📖	—	—	—	—	—
meromorphic_coth 📖	mathematical	—	coth	—	meromorphic_tanh
meromorphic_coth' 📖	—	—	—	—	meromorphic_coth
meromorphic_coth'' 📖	—	—	—	—	meromorphic_coth'
meromorphic_tanh 📖	—	—	—	—	—
phi_star_affine_periodic 📖	mathematical	—	Phi_star Phi_circ	—	B_affine_periodic Phi_star.eq_1
prop_2_3 📖 ⚠️	—	—	—	—	—
prop_2_3_1 📖	—	—	—	—	summable_nterm_of_log_weight first_fourier second_fourier norm_term_eq_nterm_re continuous_LSeries_aux fourier_scale_div_noscalar
prop_2_4_minus 📖 ⚠️	mathematical	I'	S	—	—
prop_2_4_plus 📖 ⚠️	mathematical	I'	S	—	—
second_contour_limit 📖 ⚠️	mathematical	—	Phi_star E	—	—
shift_downwards 📖 ⚠️	mathematical	—	Phi_circ Phi_star E ϕ_pm	—	—
shift_downwards_simplified 📖 ⚠️	mathematical	—	B ϕ_pm	—	—
shift_upwards 📖 ⚠️	mathematical	—	Phi_circ Phi_star E ϕ_pm	—	—
shift_upwards_simplified 📖 ⚠️	mathematical	—	B ϕ_pm	—	—
sinh_zero_iff 📖	—	—	—	—	—
summable_nterm_of_log_weight 📖	mathematical	—	nterm	—	—
third_contour_limit 📖 ⚠️	mathematical	—	Phi_star E	—	—
varphi_abs 📖 ⚠️	mathematical	—	AbsolutelyContinuous ϕ_pm	—	—
varphi_deriv_integ 📖 ⚠️	mathematical	—	ϕ_pm	—	—
varphi_deriv_tv 📖 ⚠️	mathematical	—	ϕ_pm	—	—
varphi_fourier_decay 📖 ⚠️	mathematical	—	ϕ_pm	—	—
varphi_fourier_ident 📖	mathematical	—	ϕ_pm Phi_circ Phi_star E	—	ϕ_continuous cont_E Phi_star_zero Phi_circ.contDiff_real Phi_star.contDiff_real
varphi_fourier_minus_error 📖 ⚠️	mathematical	—	I ϕ_pm	—	—
varphi_fourier_plus_error 📖 ⚠️	mathematical	—	ϕ_pm I	—	—
varphi_integ 📖 ⚠️	mathematical	—	ϕ_pm	—	—
ϕ_c2_left 📖	mathematical	—	ϕ_pm	—	Phi_star.contDiff_real Phi_circ.contDiff_real
ϕ_c2_right 📖	mathematical	—	ϕ_pm	—	Phi_star.contDiff_real Phi_circ.contDiff_real Phi_star_zero
ϕ_circ_bound_left 📖	mathematical	—	Phi_circ	—	—
ϕ_circ_bound_right 📖	mathematical	—	Phi_circ	—	—
ϕ_continuous 📖	mathematical	—	ϕ_pm	—	ϕ_c2_left ϕ_c2_right
ϕ_star_bound_left 📖	mathematical	—	Phi_star	—	ϕ_circ_bound_left Phi_star.eq_1
ϕ_star_bound_right 📖	mathematical	—	Phi_star	—	ϕ_circ_bound_right

CH2.B

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_zero 📖	mathematical	—	CH2.B	—	—

CH2.ContDiff

Theorems

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

CH2.Phi_circ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contDiff_real 📖	mathematical	—	CH2.Phi_circ	—	—
meromorphic 📖	mathematical	—	CH2.Phi_circ	—	—
poles 📖	mathematical	—	CH2.Phi_circ	—	CH2.fun_meromorphicOrderAt_div CH2.sinh_zero_iff
poles_simple 📖	mathematical	—	CH2.Phi_circ	—	poles meromorphic residue
residue 📖	mathematical	—	CH2.Phi_circ	—	eq_1 CH2.coth.eq_1

CH2.Phi_star

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contDiff_real 📖	mathematical	—	CH2.Phi_star	—	—
meromorphic 📖	mathematical	—	CH2.Phi_star	—	CH2.meromorphicAt_B
poles 📖 ⚠️	mathematical	—	CH2.Phi_star	—	—
poles_simple 📖	mathematical	—	CH2.Phi_star	—	poles meromorphic residue
residue 📖	mathematical	—	CH2.Phi_star	—	CH2.Phi_circ.residue

---

← Back to Index