OAI/NumberTheory/PrimeGaps/ProfileVariance.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LargePrimeGaps.centered_profile_integral line 13
  2. theorem OAI.LargePrimeGaps.coordinateSum_variance line 23
  3. theorem OAI.LargePrimeGaps.scaledProfileDensity_continuous line 56
  4. theorem OAI.LargePrimeGaps.scaledProfileDensity_compact line 61
  5. theorem OAI.LargePrimeGaps.scaledProfileDensity_variance line 69
  6. theorem OAI.LargePrimeGaps.concentrated_cutoff_mass line 87
  7. theorem OAI.LargePrimeGaps.cutoff_mass_le_one line 133
  8. def OAI.LargePrimeGaps.simplexCutoff line 151
  9. theorem OAI.LargePrimeGaps.simplexCutoff_smooth line 154
  10. theorem OAI.LargePrimeGaps.simplexCutoff_nonneg line 159
  11. theorem OAI.LargePrimeGaps.simplexCutoff_le_one line 162
  12. theorem OAI.LargePrimeGaps.simplexCutoff_eq_one line 165
  13. theorem OAI.LargePrimeGaps.simplexCutoff_eq_zero line 171
  14. def OAI.LargePrimeGaps.cutoffDeletion line 177
  15. theorem OAI.LargePrimeGaps.cutoffDeletion_continuous line 180
  16. theorem OAI.LargePrimeGaps.cutoffDeletion_integrable line 191
  17. theorem OAI.LargePrimeGaps.cutoffDeletion_nonneg line 196
  18. theorem OAI.LargePrimeGaps.cutoffDeletion_le_mass line 200
  19. theorem OAI.LargePrimeGaps.cutoffDeletion_eq_mass line 209
  20. def OAI.LargePrimeGaps.cancellationBracket line 222
  21. theorem OAI.LargePrimeGaps.cancellationBracket_continuous line 225
  22. theorem OAI.LargePrimeGaps.cancellationBracket_abs_le_one line 230
  23. theorem OAI.LargePrimeGaps.cancellationBracket_flat line 254
  24. theorem OAI.LargePrimeGaps.concentrated_function_sq line 265
  25. theorem OAI.LargePrimeGaps.profile_first_moment_nonneg line 313
  26. theorem OAI.LargePrimeGaps.scaled_level_moment_bound line 321
  27. theorem OAI.LargePrimeGaps.scaled_level_variance_bound line 329
  28. theorem OAI.LargePrimeGaps.scaled_cutoff_mass_bounds line 342
  29. theorem OAI.LargePrimeGaps.one_sub_sqrt_level_sq line 373
  30. theorem OAI.LargePrimeGaps.scaled_cancellation_integral_bound line 389
  31. def OAI.LargePrimeGaps.alpha line 429
  32. theorem OAI.LargePrimeGaps.alpha_pos line 431
  33. theorem OAI.LargePrimeGaps.alpha_succ line 434
  34. theorem OAI.LargePrimeGaps.sqrt_alpha_succ_ratio line 441
  35. theorem OAI.LargePrimeGaps.productProfile_snoc line 464
  36. theorem OAI.LargePrimeGaps.coordinateSum_snoc line 471
  37. def OAI.LargePrimeGaps.levelFunction line 477
  38. def OAI.LargePrimeGaps.deleteCoordinate line 482
  39. theorem OAI.LargePrimeGaps.levelFunction_delete line 485