OAI/NumberTheory/Ostmann/ZeroDensity/DensitySquareConjugation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Conjugating the actual smoothed square

  1. theorem OAI.Ostmann.density_nat_cpow_conj line 12
  2. theorem OAI.Ostmann.densityCompletedSquare_inverse_conj line 19
  3. theorem OAI.Ostmann.densitySquareNormalizer_inverse_conj line 25
  4. theorem OAI.Ostmann.densitySquareContour_inverse_conj line 31
  5. theorem OAI.Ostmann.densitySquareIntegral_inverse_conj line 38
  6. theorem OAI.Ostmann.densitySmoothedSquare_inverse_conj line 52
  7. theorem OAI.Ostmann.density_L_fourth_single_bound line 57