RosserSchoenfeldPrime

📁 Source: PrimeNumberTheoremAnd/RosserSchoenfeldPrime.lean

Statistics

Metric	Count
Definitions `L`, `Stieltjes`, `meisselMertensConstant`, `mertensConstant`	4
Theorems `bound_deriv`, `deriv_eq`, `integrableOn_deriv`, `integrableOn_deriv_inv`, `integrableOn_deriv_inv_div_log`, `intervalIntegrable_inv_log_pow`, `intervalIntegral_eq`, `ioiIntegrable_inv_log_pow`, `ioiIntegral_tendsto_zero`, `leftLim_theta_succ`, `log_div_log_eq`, `meisselMertensConstant_identity`, `mertens_first_theorem`, `mertens_first_theorem'`, `mertens_second_theorem`, `mertens_second_theorem'`, `pnt`, `pntBigO`, `pre_413`, `pre_413_measure_inter`, `summable_pre413`, `support_pre413`, `theorem_12`, `theta_one`, `theta_succ_sub`, `theta_two`, `interval_add_Ioi`	27
Total	31
⚠️ With sorry `theorem_12`	1

RS_prime

Definitions

Name	Category	Theorems
`L` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bound_deriv` 📖	—	—	—	—	—
`deriv_eq` 📖	—	—	—	—	`log_div_log_eq`
`integrableOn_deriv` 📖	—	—	—	—	`pnt` `ioiIntegrable_inv_log_pow` `bound_deriv` `intervalIntegrable_inv_log_pow`
`integrableOn_deriv_inv` 📖	—	—	—	—	`pnt` `ioiIntegrable_inv_log_pow`
`integrableOn_deriv_inv_div_log` 📖	—	—	—	—	`integrableOn_deriv`
`intervalIntegrable_inv_log_pow` 📖	—	—	—	—	—
`intervalIntegral_eq` 📖	—	—	—	—	`log_div_log_eq`
`ioiIntegrable_inv_log_pow` 📖	—	—	—	—	`intervalIntegrable_inv_log_pow`
`ioiIntegral_tendsto_zero` 📖	—	—	—	—	`intervalIntegral.interval_add_Ioi`
`leftLim_theta_succ` 📖	—	—	—	—	—
`log_div_log_eq` 📖	—	—	—	—	—
`meisselMertensConstant_identity` 📖	mathematical	—	`meisselMertensConstant`	—	`eq_415` `integrableOn_deriv_inv_div_log` `meisselMertensConstant.eq_1`
`mertens_first_theorem` 📖	mathematical	—	`mertensConstant`	—	`eq_420` `pnt` `ioiIntegral_tendsto_zero` `integrableOn_deriv_inv`
`mertens_first_theorem'` 📖	—	—	—	—	`pnt` `eq_420` `integrableOn_deriv_inv`
`mertens_second_theorem` 📖	mathematical	—	`meisselMertensConstant`	—	`meisselMertensConstant_identity` `pnt` `ioiIntegral_tendsto_zero` `integrableOn_deriv_inv_div_log`
`mertens_second_theorem'` 📖	—	—	—	—	`pnt` `meisselMertensConstant_identity` `integrableOn_deriv_inv_div_log`
`pnt` 📖	—	—	—	—	`pntBigO`
`pntBigO` 📖	—	—	—	—	`MediumPNT`
`pre_413` 📖	mathematical	—	`θ.Stieltjes`	—	`summable_pre413` `support_pre413` `leftLim_theta_succ` `theta_succ_sub` `pre_413_measure_inter`
`pre_413_measure_inter` 📖	mathematical	—	`θ.Stieltjes`	—	`theta_two` `leftLim_theta_succ` `theta_one` `theta_succ_sub`
`summable_pre413` 📖	mathematical	—	`θ.Stieltjes`	—	—
`support_pre413` 📖	mathematical	—	`θ.Stieltjes`	—	—
`theorem_12` 📖 ⚠️	mathematical	—	`c₀`	—	—
`theta_one` 📖	—	—	—	—	—
`theta_succ_sub` 📖	—	—	—	—	—
`theta_two` 📖	—	—	—	—	—

RS_prime.θ

Definitions

Name	Category	Theorems
`Stieltjes` 📖	CompOp	4 math math: `RS_prime.pre_413`, `RS_prime.support_pre413`, `RS_prime.pre_413_measure_inter`, `RS_prime.summable_pre413`

(root)

Definitions

Name	Category	Theorems
`meisselMertensConstant` 📖	CompOp	3 math math: `Dusart.theorem_5_6`, `RS_prime.mertens_second_theorem`, `RS_prime.meisselMertensConstant_identity`
`mertensConstant` 📖	CompOp	2 math math: `Dusart.theorem_5_7`, `RS_prime.mertens_first_theorem`

intervalIntegral

Theorems

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

---

← Back to Index