OAI/NumberTheory/DirichletL/MeanSquare/ThetaDensity.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InitialMeanSquare.HasInitialCanonicalDensityAtRadius.nonzero_source_bound line 86
  2. theorem OAI.InitialMeanSquare.outside_mean_square_of_canonical_density_at_radius line 192
  3. theorem OAI.InitialMeanSquare.outside_mean_square_of_theta_models line 269
  4. lemma OAI.CubicEisenstein.cuspBarrierField_local_model line 293
  5. lemma OAI.CubicEisenstein.cuspBarrierProfile_log_derivative_bound line 324
  6. lemma OAI.CubicEisenstein.cuspBarrierField_scaled_deriv_bound line 349
  7. lemma OAI.CubicEisenstein.kernelBarrier_scaled_fderiv_bound line 389
  8. lemma OAI.CubicEisenstein.kernelBarrier_scaled_real_fderiv_bound line 409
  9. lemma OAI.CubicEisenstein.kernelExhaustionProfile_euler_bounded line 424
  10. lemma OAI.CubicEisenstein.kernelExhaustionCutoff_scaled_fderiv_bound line 439
  11. lemma OAI.CubicEisenstein.kernelExhaustionCutoff_fderiv_eventually_zero line 467
  12. lemma OAI.CubicEisenstein.kernelExhaustionCutoff_energy_density_bound line 480
  13. def OAI.SixthPowerAverage.totientDensity line 502
  14. theorem OAI.SixthPowerAverage.idealSupport_card line 505
  15. theorem OAI.SixthPowerAverage.idealSupport_density line 510
  16. theorem OAI.SixthPowerAverage.idealSexticRow_sixth_mask line 516
  17. theorem OAI.SixthPowerAverage.idealSexticRow_sixth_radial_summable line 525
  18. theorem OAI.SixthPowerAverage.idealSexticRow_sixth_average line 542
  19. theorem OAI.SixthPowerAverage.idealRowSum_sixth_average line 554
  20. theorem OAI.SixthPowerAverage.sixth_average_remainder_bound line 590
  21. theorem OAI.SixthPowerAverage.sixth_power_fiber_card line 611
  22. theorem OAI.SixthPowerAverage.sixth_power_average_cauchy line 622