OAI/NumberTheory/Ostmann/ZeroDensity/DensityHybridIntegral.lean
4 declarations, 0 contain sorry, 0 declared as axioms
Integrated short-window sieve for complex Dirichlet polynomials
- theorem
OAI.Ostmann.density_finite_localized_integrableline 13 - theorem
OAI.Ostmann.density_window_energy_integralline 23 - theorem
OAI.Ostmann.density_integrated_localized_sieveline 37 - theorem
OAI.Ostmann.density_hybrid_windowline 60