ZetaAppendix

📁 Source: PrimeNumberTheoremAnd/ZetaAppendix.lean

Statistics

Metric	Count
Definitions `IsHalfInteger`, `e`	2
Theorems `asummable`, `asummable''`, `bernsteinApproximation_monotone`, `cos_ne_zero`, `cpow_split_re_im`, `hsummable`, `hsummable'`, `hsummable''`, `integral_power_phase_ibp`, `lemma_IBP_bound_C1`, `lemma_IBP_bound_C1_monotone`, `lemma_IBP_bound_abs_antitone`, `lemma_IBP_bound_monotone`, `lemma_aachIBP`, `lemma_aachcanc`, `lemma_aachcanc_pointwise`, `lemma_aachdecre`, `lemma_aachfour`, `lemma_aachmonophase`, `lemma_aachra`, `lemma_abadeuleulmit1`, `lemma_abadeulmac`, `lemma_abadeulmac'`, `lemma_abadeulmit2`, `lemma_abadeulmit2_continuousAt_integral_tsum_one_div_sub_int_sq`, `lemma_abadeulmit2_deriv_neg_pi_mul_cot_pi_mul`, `lemma_abadeulmit2_integral_eq_cot_diff`, `lemma_abadeulmit2_integral_tsum_inv_sub_int_sq`, `lemma_abadeulmit2_tsum_one_div_sub_int_sq`, `lemma_abadimpseri`, `lemma_abadsumas`, `lemma_abadtoabsum`, `lemma_abadusepoisson`, `lemma_approx_monotone_C1`, `lemma_approx_monotone_C1_I`, `neg_one_pow`, `proposition_applem`, `proposition_dadaro`, `sin_ne_zero`, `summable_inv_sub_inv_aux`, `telescoping_sum`, `trig`, `trig'`, `trig''`, `tsum_even_add_odd'`	45
Total	47
⚠️ With sorry `lemma_abadsumas`, `lemma_abadusepoisson`, `proposition_dadaro`	3

Real

Definitions

Name	Category	Theorems
`IsHalfInteger` 📖	MathDef	—

ZetaAppendix

Definitions

Name	Category	Theorems
`e` 📖	CompOp	6 math math: `lemma_aachIBP`, `lemma_aachfour`, `lemma_abadsumas`, `lemma_aachmonophase`, `integral_power_phase_ibp`, `lemma_abadusepoisson`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`asummable` 📖	—	—	—	—	`hsummable`
`asummable''` 📖	—	—	—	—	`neg_one_pow` `hsummable''`
`bernsteinApproximation_monotone` 📖	—	—	—	—	—
`cos_ne_zero` 📖	—	—	—	—	—
`cpow_split_re_im` 📖	—	—	—	—	—
`hsummable` 📖	—	—	—	—	—
`hsummable'` 📖	—	—	—	—	`hsummable`
`hsummable''` 📖	—	—	—	—	—
`integral_power_phase_ibp` 📖	mathematical	—	`e`	—	—
`lemma_IBP_bound_C1` 📖	—	—	—	—	—
`lemma_IBP_bound_C1_monotone` 📖	—	—	—	—	`lemma_IBP_bound_C1`
`lemma_IBP_bound_abs_antitone` 📖	—	—	—	—	`lemma_IBP_bound_monotone`
`lemma_IBP_bound_monotone` 📖	—	—	—	—	`lemma_approx_monotone_C1` `lemma_IBP_bound_C1_monotone`
`lemma_aachIBP` 📖	mathematical	—	`e`	—	`integral_power_phase_ibp`
`lemma_aachcanc` 📖	—	`Real.IsHalfInteger`	—	—	`lemma_aachcanc_pointwise`
`lemma_aachcanc_pointwise` 📖	—	`Real.IsHalfInteger`	—	—	—
`lemma_aachdecre` 📖	—	—	—	—	—
`lemma_aachfour` 📖	mathematical	—	`e`	—	`lemma_aachIBP` `lemma_aachdecre` `lemma_aachmonophase`
`lemma_aachmonophase` 📖	mathematical	—	`e`	—	`lemma_IBP_bound_abs_antitone`
`lemma_aachra` 📖	—	—	—	—	—
`lemma_abadeuleulmit1` 📖	—	—	—	—	`trig''` `hsummable` `hsummable'` `hsummable''` `telescoping_sum` `neg_one_pow` `tsum_even_add_odd'` `asummable` `asummable''`
`lemma_abadeulmac` 📖	—	`Real.IsHalfInteger`	—	—	`lemma_abadeulmac'`
`lemma_abadeulmac'` 📖	—	—	—	—	`Zeta0EqZeta`
`lemma_abadeulmit2` 📖	—	—	—	—	`lemma_abadeulmit2_deriv_neg_pi_mul_cot_pi_mul` `lemma_abadeulmit2_tsum_one_div_sub_int_sq`
`lemma_abadeulmit2_continuousAt_integral_tsum_one_div_sub_int_sq` 📖	—	—	—	—	—
`lemma_abadeulmit2_deriv_neg_pi_mul_cot_pi_mul` 📖	—	—	—	—	—
`lemma_abadeulmit2_integral_eq_cot_diff` 📖	—	—	—	—	`lemma_abadeulmit2_integral_tsum_inv_sub_int_sq` `summable_inv_sub_inv_aux`
`lemma_abadeulmit2_integral_tsum_inv_sub_int_sq` 📖	—	—	—	—	`Complex.hasDerivAt_ofReal`
`lemma_abadeulmit2_tsum_one_div_sub_int_sq` 📖	—	—	—	—	`lemma_abadeulmit2_continuousAt_integral_tsum_one_div_sub_int_sq` `lemma_abadeulmit2_integral_eq_cot_diff`
`lemma_abadimpseri` 📖	—	—	—	—	—
`lemma_abadsumas` 📖 ⚠️	mathematical	`Real.IsHalfInteger`	`e`	—	—
`lemma_abadtoabsum` 📖	—	`Real.IsHalfInteger`	—	—	`lemma_abadeulmac`
`lemma_abadusepoisson` 📖 ⚠️	mathematical	—	`e`	—	—
`lemma_approx_monotone_C1` 📖	—	—	—	—	`lemma_approx_monotone_C1_I`
`lemma_approx_monotone_C1_I` 📖	—	—	—	—	`bernsteinApproximation_monotone`
`neg_one_pow` 📖	—	—	—	—	—
`proposition_applem` 📖	—	`Real.IsHalfInteger`	—	—	`lemma_aachfour` `lemma_aachcanc`
`proposition_dadaro` 📖 ⚠️	—	`Real.IsHalfInteger`	—	—	—
`sin_ne_zero` 📖	—	—	—	—	—
`summable_inv_sub_inv_aux` 📖	—	—	—	—	—
`telescoping_sum` 📖	—	—	—	—	—
`trig` 📖	—	—	—	—	—
`trig'` 📖	—	—	—	—	`sin_ne_zero` `cos_ne_zero`
`trig''` 📖	—	—	—	—	`trig'`
`tsum_even_add_odd'` 📖	—	—	—	—	—

---

← Back to Index