MediumPNT

📁 Source: PrimeNumberTheoremAnd/MediumPNT.lean

Statistics

Metric	Count
Definitions `ChebyshevPsi`, `I₁`, `I₂`, `I₃`, `I₃₇`, `I₄`, `I₅`, `I₆`, `I₇`, `I₈`, `I₉`, `LogDerivZetaHasBound`, `LogDerivZetaIsHoloSmall`, `SmoothedChebyshev`, `SmoothedChebyshevIntegrand`	15
Theorems `BddAboveOnRect`, `psi_eq_sum_range`, `I1Bound`, `I2Bound`, `I3Bound`, `I4Bound`, `I5Bound`, `I6Bound`, `I6I4`, `I7Bound`, `I7I3`, `I8Bound`, `I8I2`, `I9Bound`, `I9I1`, `IBound_aux1`, `LogDerivZetaBoundedAndHolo`, `LogDerivativeDirichlet`, `MediumPNT`, `MellinOfSmooth1cExplicit`, `SmoothedChebyshevClose`, `SmoothedChebyshevClose_aux`, `SmoothedChebyshevDirichlet`, `SmoothedChebyshevDirichlet_aux_integrable`, `SmoothedChebyshevDirichlet_aux_tsum_integral`, `SmoothedChebyshevPull1`, `SmoothedChebyshevPull1_aux_integrable`, `SmoothedChebyshevPull2`, `SmoothedChebyshevPull2_aux1`, `ZetaBoxEval`, `ae_volume_of_contains_compl_singleton_zero`, `dlog_riemannZeta_bdd_on_vertical_lines`, `dlog_riemannZeta_bdd_on_vertical_lines_explicit`, `integral_evaluation`, `interval_membership`, `log_pow_over_xsq_integral_bounded`, `one_add_inv_log`, `poisson_kernel_integrable`, `realDiff_of_complexDiff`, `smoothedChebyshevIntegrand_conj`, `verticalIntegral_split_three_finite`, `verticalIntegral_split_three_finite'`, `x_ε_to_inf`	43
Total	58

Chebyshev

Theorems

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

(root)

Definitions

Name	Category	Theorems
`ChebyshevPsi` 📖	CompOp	—
`I₁` 📖	CompOp	3 math math: `I1Bound`, `I9I1`, `SmoothedChebyshevPull1`
`I₂` 📖	CompOp	3 math math: `I2Bound`, `I8I2`, `SmoothedChebyshevPull1`
`I₃` 📖	CompOp	3 math math: `SmoothedChebyshevPull2`, `I7I3`, `I3Bound`
`I₃₇` 📖	CompOp	2 math math: `SmoothedChebyshevPull2`, `SmoothedChebyshevPull1`
`I₄` 📖	CompOp	3 math math: `I4Bound`, `I6I4`, `SmoothedChebyshevPull2`
`I₅` 📖	CompOp	2 math math: `SmoothedChebyshevPull2`, `I5Bound`
`I₆` 📖	CompOp	3 math math: `I6I4`, `SmoothedChebyshevPull2`, `I6Bound`
`I₇` 📖	CompOp	3 math math: `I7Bound`, `SmoothedChebyshevPull2`, `I7I3`
`I₈` 📖	CompOp	3 math math: `I8Bound`, `I8I2`, `SmoothedChebyshevPull1`
`I₉` 📖	CompOp	3 math math: `I9Bound`, `I9I1`, `SmoothedChebyshevPull1`
`LogDerivZetaHasBound` 📖	MathDef	1 math math: `LogDerivZetaBoundedAndHolo`
`LogDerivZetaIsHoloSmall` 📖	MathDef	—
`SmoothedChebyshev` 📖	CompOp	4 math math: `SmoothedChebyshevPull3`, `SmoothedChebyshevClose`, `SmoothedChebyshevDirichlet`, `SmoothedChebyshevPull1`
`SmoothedChebyshevIntegrand` 📖	CompOp	3 math math: `I1NewIntegrandBound`, `smoothedChebyshevIntegrand_conj`, `SmoothedChebyshevPull1_aux_integrable`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`BddAboveOnRect` 📖	—	`HolomorphicOn`	—	—	—
`I1Bound` 📖	mathematical	—	`I₁`	—	`MellinOfSmooth1b` `triv_bound_zeta` `logt_gt_one` `SmoothedChebyshevPull1_aux_integrable` `poisson_kernel_integrable` `integral_evaluation`
`I2Bound` 📖	mathematical	`LogDerivZetaHasBound`	`I₂`	—	`MellinOfSmooth1b` `IBound_aux1` `logt_gt_one` `mul_le_mul₃` `one_add_inv_log`
`I3Bound` 📖	mathematical	`LogDerivZetaHasBound`	`I₃`	—	`MellinOfSmooth1b` `log_pow_over_xsq_integral_bounded` `logt_gt_one`
`I4Bound` 📖	mathematical	`LogDerivZetaIsHoloSmall`	`I₄`	—	`MellinOfSmooth1b`
`I5Bound` 📖	mathematical	`LogDerivZetaIsHoloSmall`	`I₅`	—	`MellinOfSmooth1b`
`I6Bound` 📖	mathematical	`LogDerivZetaIsHoloSmall`	`I₆`	—	`I4Bound` `I6I4`
`I6I4` 📖	mathematical	—	`I₆` `I₄`	—	`intervalIntegral_conj` `smoothedChebyshevIntegrand_conj`
`I7Bound` 📖	mathematical	`LogDerivZetaHasBound`	`I₇`	—	`I3Bound` `I7I3`
`I7I3` 📖	mathematical	—	`I₇` `I₃`	—	`intervalIntegral_conj` `smoothedChebyshevIntegrand_conj`
`I8Bound` 📖	mathematical	`LogDerivZetaHasBound`	`I₈`	—	`I2Bound` `I8I2`
`I8I2` 📖	mathematical	—	`I₈` `I₂`	—	`intervalIntegral_conj` `smoothedChebyshevIntegrand_conj`
`I9Bound` 📖	mathematical	—	`I₉`	—	`I1Bound` `I9I1`
`I9I1` 📖	mathematical	—	`I₉` `I₁`	—	`smoothedChebyshevIntegrand_conj`
`IBound_aux1` 📖	—	—	—	—	—
`LogDerivZetaBoundedAndHolo` 📖	mathematical	—	`LogDerivZetaHasBound` `HolomorphicOn`	—	`LogDerivZetaBndUnif` `LogDerivZetaHolcLargeT`
`LogDerivativeDirichlet` 📖	—	—	—	—	—
`MediumPNT` 📖	—	—	—	—	`SmoothExistence` `SmoothedChebyshevClose` `MellinOfSmooth1cExplicit` `LogDerivZetaBoundedAndHolo` `LogDerivZetaHolcSmallT` `I1Bound` `I2Bound` `I3Bound` `I5Bound` `I7Bound` `I8Bound` `I9Bound` `I4Bound` `I6Bound` `x_ε_to_inf` `logt_gt_one` `Smooth1MellinDifferentiable` `SmoothedChebyshevPull1` `SmoothedChebyshevPull2`
`MellinOfSmooth1cExplicit` 📖	mathematical	—	`Smooth1`	—	`MellinOfSmooth1c`
`SmoothedChebyshevClose` 📖	mathematical	—	`SmoothedChebyshev`	—	`Smooth1Properties_above` `Smooth1LeOne` `Smooth1Nonneg` `SmoothedChebyshevDirichlet` `SmoothedChebyshevClose_aux`
`SmoothedChebyshevClose_aux` 📖	—	—	—	—	`Chebyshev.psi_eq_sum_range`
`SmoothedChebyshevDirichlet` 📖	mathematical	—	`SmoothedChebyshev` `Smooth1`	—	`logt_gt_one` `LogDerivativeDirichlet` `SmoothedChebyshevDirichlet_aux_tsum_integral` `Smooth1MellinConvergent` `SmoothedChebyshevDirichlet_aux_integrable` `Smooth1ContinuousAt`
`SmoothedChebyshevDirichlet_aux_integrable` 📖	mathematical	—	`Smooth1`	—	`MellinOfSmooth1b` `Smooth1MellinDifferentiable`
`SmoothedChebyshevDirichlet_aux_tsum_integral` 📖	mathematical	—	`Smooth1`	—	`Smooth1MellinDifferentiable` `SmoothedChebyshevDirichlet_aux_integrable`
`SmoothedChebyshevPull1` 📖	mathematical	`HolomorphicOn`	`SmoothedChebyshev` `I₁` `I₂` `I₃₇` `I₈` `I₉` `Smooth1`	—	`logt_gt_one` `verticalIntegral_split_three` `SmoothedChebyshevPull1_aux_integrable` `rectangle_mem_nhds_iff` `ResidueTheoremOnRectangleWithSimplePole'` `Smooth1MellinDifferentiable` `riemannZetaLogDerivResidueBigO` `ResidueMult`
`SmoothedChebyshevPull1_aux_integrable` 📖	mathematical	—	`SmoothedChebyshevIntegrand`	—	`dlog_riemannZeta_bdd_on_vertical_lines` `SmoothedChebyshevDirichlet_aux_integrable` `differentiableAt_deriv_riemannZeta` `realDiff_of_complexDiff`
`SmoothedChebyshevPull2` 📖	mathematical	`HolomorphicOn` `SmoothedChebyshevIntegrand`	`I₃₇` `I₃` `I₄` `I₅` `I₆` `I₇`	—	`interval_membership` `HolomorphicOn.vanishesOnRectangle` `verticalIntegral_split_three_finite'` `SmoothedChebyshevPull2_aux1` `Smooth1MellinDifferentiable` `realDiff_of_complexDiff`
`SmoothedChebyshevPull2_aux1` 📖	—	`HolomorphicOn`	—	—	—
`ZetaBoxEval` 📖	—	—	—	—	`MellinOfSmooth1c`
`ae_volume_of_contains_compl_singleton_zero` 📖	—	—	—	—	—
`dlog_riemannZeta_bdd_on_vertical_lines` 📖	—	—	—	—	`dlog_riemannZeta_bdd_on_vertical_lines_explicit`
`dlog_riemannZeta_bdd_on_vertical_lines_explicit` 📖	—	—	—	—	`dlog_riemannZeta_bdd_on_vertical_lines_generalized`
`integral_evaluation` 📖	—	—	—	—	`ae_volume_of_contains_compl_singleton_zero`
`interval_membership` 📖	—	—	—	—	—
`log_pow_over_xsq_integral_bounded` 📖	—	—	—	—	`logt_gt_one`
`one_add_inv_log` 📖	—	—	—	—	`logt_gt_one`
`poisson_kernel_integrable` 📖	—	—	—	—	—
`realDiff_of_complexDiff` 📖	—	—	—	—	—
`smoothedChebyshevIntegrand_conj` 📖	mathematical	—	`SmoothedChebyshevIntegrand`	—	`deriv_riemannZeta_conj` `riemannZeta_conj`
`verticalIntegral_split_three_finite` 📖	mathematical	—	`VIntegral`	—	—
`verticalIntegral_split_three_finite'` 📖	mathematical	—	`VIntegral`	—	`verticalIntegral_split_three_finite`
`x_ε_to_inf` 📖	—	—	—	—	—

---

← Back to Index