ZetaAppendix

📁 Source: PrimeNumberTheoremAnd/ZetaAppendix.lean

Statistics

Metric	Count
Definitions `IsHalfInteger`, `dadaro_g`, `e`	3
Theorems `floor_add_three_halfs`, `not_isInteger`, `floor_add_three_halfs_gt`, `asummable`, `asummable''`, `bernsteinApproximation_monotone`, `cos_ne_zero`, `cpow_split_re_im`, `deriv_e`, `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_abadsumas_integrable_explog`, `lemma_abadsumas_quad`, `lemma_abadsumas_sum_fourier`, `lemma_abadsumas_summable_alternating_theta`, `lemma_abadtoabsum`, `lemma_abadusepoisson`, `lemma_approx_monotone_C1`, `lemma_approx_monotone_C1_I`, `neg_one_pow`, `proposition_applem`, `proposition_dadaro`, `proposition_dadaro_b_tendsto_zero_atTop`, `proposition_dadaro_zero_eq`, `proposition_dadaro_zero_lt`, `sin_ne_zero`, `summable_inv_sub_inv_aux`, `telescoping_sum`, `trig`, `trig'`, `trig''`, `tsum_even_add_odd'`	56
Total	59
⚠️ With sorry `lemma_abadusepoisson`	1

Real

Definitions

Name	Category	Theorems
`IsHalfInteger` 📖	MathDef	1 math math: `IsHalfInteger.floor_add_three_halfs`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`floor_add_three_halfs_gt` 📖	—	—	—	—	—

Real.IsHalfInteger

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`floor_add_three_halfs` 📖	mathematical	—	`Real.IsHalfInteger`	—	—
`not_isInteger` 📖	—	`Real.IsHalfInteger`	—	—	—

ZetaAppendix

Definitions

Name	Category	Theorems
`dadaro_g` 📖	CompOp	1 math math: `proposition_dadaro_b_tendsto_zero_atTop`
`e` 📖	CompOp	9 math math: `lemma_abadsumas_integrable_explog`, `lemma_abadsumas_sum_fourier`, `lemma_aachIBP`, `lemma_aachfour`, `lemma_abadsumas`, `lemma_aachmonophase`, `deriv_e`, `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` 📖	—	—	—	—	—
`deriv_e` 📖	mathematical	—	`e`	—	—
`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`	—	`proposition_applem` `lemma_abadsumas_sum_fourier` `lemma_abadsumas_summable_alternating_theta` `lemma_abadsumas_quad` `lemma_abadimpseri`
`lemma_abadsumas_integrable_explog` 📖	mathematical	—	`e`	—	—
`lemma_abadsumas_quad` 📖	—	—	—	—	`lemma_abadeulmit2`
`lemma_abadsumas_sum_fourier` 📖	mathematical	—	`e`	—	`e.eq_1` `lemma_abadsumas_integrable_explog`
`lemma_abadsumas_summable_alternating_theta` 📖	—	—	—	—	—
`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`	—	—	`proposition_dadaro_zero_eq` `proposition_dadaro_zero_lt`
`proposition_dadaro_b_tendsto_zero_atTop` 📖	mathematical	—	`dadaro_g`	—	—
`proposition_dadaro_zero_eq` 📖	—	`Real.IsHalfInteger`	—	—	`proposition_dadaro_zero_lt`
`proposition_dadaro_zero_lt` 📖	—	`Real.IsHalfInteger`	—	—	`proposition_dadaro_b_tendsto_zero_atTop` `lemma_abadtoabsum` `lemma_abadusepoisson` `Real.IsHalfInteger.not_isInteger` `lemma_abadsumas` `Real.floor_add_three_halfs_gt` `Real.IsHalfInteger.floor_add_three_halfs`
`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