StrongPNT

📁 Source: PrimeNumberTheoremAnd/StrongPNT.lean

Statistics

Metric	Count
Definitions `DeltaT`, `E`, `F`, `I1New`, `I2New`, `I3New`, `I4New`, `I5New`, `PathIntegral`	9
Theorems `BorelCaratheodoryDeriv`, `DeltaRange`, `EinIoo`, `FLogTtoDeltaT`, `Fequ`, `I1NewBound`, `I1NewIntegrandBound`, `I2NewBound`, `I3NewBound`, `I4NewBound`, `I5NewBound`, `IntegralLogSqOverTSqBound`, `LogDerivZetaBdd_of_Re_ge_three_halves`, `LogDerivZetaBoundForI1`, `LogDerivZetaLogSquaredBoundSmallt`, `LogDerivZetaUniformLogSquaredBound`, `LogDerivZetaUniformLogSquaredBoundStrip`, `LogDerivZetaUniformLogSquaredBoundStripSpec`, `LogOfAnalyticFunction`, `NormXPowS`, `SmoothedChebyshevPull3`, `ZeroInequality`, `ZeroInequalitySpecialized`, `cauchy_formula_deriv`	24
Total	33
⚠️ With sorry `DeltaRange`, `I2NewBound`, `I3NewBound`, `LogDerivZetaLogSquaredBoundSmallt`, `LogDerivZetaUniformLogSquaredBoundStrip`, `LogOfAnalyticFunction`, `ZeroInequality`	7

(root)

Definitions

Name	Category	Theorems
`DeltaT` 📖	CompOp	2 math math: `FLogTtoDeltaT`, `DeltaRange`
`E` 📖	CompOp	3 math math: `ZeroInequalitySpecialized`, `EinIoo`, `Fequ`
`F` 📖	CompOp	5 math math: `I3NewBound`, `I4NewBound`, `I2NewBound`, `FLogTtoDeltaT`, `Fequ`
`I1New` 📖	CompOp	2 math math: `SmoothedChebyshevPull3`, `I1NewBound`
`I2New` 📖	CompOp	2 math math: `SmoothedChebyshevPull3`, `I2NewBound`
`I3New` 📖	CompOp	2 math math: `I3NewBound`, `SmoothedChebyshevPull3`
`I4New` 📖	CompOp	2 math math: `SmoothedChebyshevPull3`, `I4NewBound`
`I5New` 📖	CompOp	2 math math: `SmoothedChebyshevPull3`, `I5NewBound`
`PathIntegral` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`BorelCaratheodoryDeriv` 📖	—	—	—	—	`DerivativeBound`
`DeltaRange` 📖 ⚠️	mathematical	—	`DeltaT`	—	—
`EinIoo` 📖	mathematical	—	`E`	—	`ZeroInequality`
`FLogTtoDeltaT` 📖	mathematical	—	`DeltaT` `F`	—	`Fequ`
`Fequ` 📖	mathematical	—	`F` `E`	—	`LogDerivZetaUniformLogSquaredBoundStrip`
`I1NewBound` 📖	mathematical	—	`I1New`	—	`I1NewIntegrandBound` `IntegralLogSqOverTSqBound`
`I1NewIntegrandBound` 📖	mathematical	—	`SmoothedChebyshevIntegrand`	—	`LogDerivZetaBoundForI1` `MellinOfSmooth1b`
`I2NewBound` 📖 ⚠️	mathematical	—	`I2New` `F`	—	—
`I3NewBound` 📖 ⚠️	mathematical	—	`I3New` `F`	—	—
`I4NewBound` 📖	mathematical	—	`I4New` `F`	—	`I2NewBound` `intervalIntegral_conj` `smoothedChebyshevIntegrand_conj`
`I5NewBound` 📖	mathematical	—	`I5New`	—	`I1NewBound` `smoothedChebyshevIntegrand_conj`
`IntegralLogSqOverTSqBound` 📖	—	—	—	—	—
`LogDerivZetaBdd_of_Re_ge_three_halves` 📖	—	—	—	—	`LogDerivativeDirichlet`
`LogDerivZetaBoundForI1` 📖	—	—	—	—	`LogDerivZetaUniformLogSquaredBound` `EinIoo` `Fequ`
`LogDerivZetaLogSquaredBoundSmallt` 📖 ⚠️	—	—	—	—	—
`LogDerivZetaUniformLogSquaredBound` 📖	—	—	—	—	`LogDerivZetaUniformLogSquaredBoundStripSpec` `LogDerivZetaBdd_of_Re_ge_three_halves`
`LogDerivZetaUniformLogSquaredBoundStrip` 📖 ⚠️	—	—	—	—	—
`LogDerivZetaUniformLogSquaredBoundStripSpec` 📖	—	—	—	—	`LogDerivZetaUniformLogSquaredBoundStrip`
`LogOfAnalyticFunction` 📖 ⚠️	—	—	—	—	—
`NormXPowS` 📖	—	—	—	—	—
`SmoothedChebyshevPull3` 📖	mathematical	`HolomorphicOn`	`SmoothedChebyshev` `I1New` `I2New` `I3New` `I4New` `I5New` `Smooth1`	—	`logt_gt_one` `verticalIntegral_split_three` `SmoothedChebyshevPull1_aux_integrable` `rectangle_mem_nhds_iff` `ResidueTheoremOnRectangleWithSimplePole'` `Smooth1MellinDifferentiable` `riemannZetaLogDerivResidueBigO` `ResidueMult`
`ZeroInequality` 📖 ⚠️	—	—	—	—	—
`ZeroInequalitySpecialized` 📖	mathematical	—	`E`	—	`ZeroInequality`
`cauchy_formula_deriv` 📖	—	—	—	—	—

---

← Back to Index