OAI/NumberTheory/DirichletL/CubicSieve/ReopeningSeparation.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SecondPassArithmetic.normPhase line 84
  2. theorem OAI.SecondPassArithmetic.normPhase_zero line 96
  3. theorem OAI.SecondPassArithmetic.normPhase_of_ne_zero line 98
  4. theorem OAI.SecondPassArithmetic.normPhase_norm line 101
  5. theorem OAI.SecondPassArithmetic.normPhase_norm_le_one line 104
  6. theorem OAI.SecondPassArithmetic.normPhase_add line 109
  7. theorem OAI.SecondPassArithmetic.normPhase_star line 115
  8. def OAI.SecondPassArithmetic.normHeightTwist line 120
  9. theorem OAI.SecondPassArithmetic.normHeightTwist_norm_le line 122
  10. theorem OAI.SecondPassArithmetic.normHeightTwist_twice line 127
  11. theorem OAI.SecondPassArithmetic.normHeightTwist_mul line 131
  12. theorem OAI.SecondPassArithmetic.logPhase_columnLog line 140
  13. theorem OAI.SecondPassArithmetic.canonicalSourceCoefficient_frequencyTwist line 152
  14. theorem OAI.SecondPassArithmetic.fixedChildRow_frequencyTwist line 162
  15. theorem OAI.SecondPassArithmetic.fixedChildRow_frequencyTwist_norm line 175
  16. def OAI.SecondPassArithmetic.secondSignedHeight line 192
  17. theorem OAI.SecondPassArithmetic.fixedSecondTest_normPhase line 199
  18. theorem OAI.SecondPassArithmetic.fixedChildRow_secondTest_normPhase line 216
  19. theorem OAI.SecondPassIntegration.childEnergy_normHeight line 240
  20. theorem OAI.SecondPassIntegration.childEnergy_previousNormHeight line 250
  21. theorem OAI.SecondPassArithmetic.firstCoreTwist_normHeight line 266
  22. theorem OAI.SecondPassArithmetic.secondRayMinus_normHeight line 273
  23. theorem OAI.SecondPassArithmetic.secondRayPlus_normHeight line 278
  24. theorem OAI.SecondPassIntegration.sqrt_height_weight line 288
  25. theorem OAI.SecondPassIntegration.densityChildEnergy_normHeight_polynomial line 298
  26. theorem OAI.SecondPassArithmetic.reopenedCanonicalRow_frequencyTwist line 355
  27. theorem OAI.SecondPassArithmetic.reopenedCanonicalRow_frequencyTwist_norm line 371
  28. theorem OAI.SecondPassArithmetic.reopenedSource_frequencyTwist line 381
  29. theorem OAI.SecondPassArithmetic.reopenedCanonicalRow_twoPassage_uniform_height line 407
  30. def OAI.CanonicalCubeSeparation.columnWindowRadius line 476
  31. lemma OAI.CanonicalCubeSeparation.columnWindowRadius_nonneg line 478
  32. def OAI.CanonicalCubeSeparation.sourceLogProfile line 482
  33. lemma OAI.CanonicalCubeSeparation.sourceLogProfile_apply line 494
  34. def OAI.CanonicalCubeSeparation.reopeningCoefficient line 498
  35. def OAI.CanonicalCubeSeparation.cubeFrequencyFactor line 502
  36. lemma OAI.CanonicalCubeSeparation.cubeFrequencyFactor_norm line 505
  37. lemma OAI.CanonicalCubeSeparation.cubeFrequencyFactor_bound line 510
  38. lemma OAI.CanonicalCubeSeparation.active_column_window line 515
  39. lemma OAI.CanonicalCubeSeparation.reopening_integrable line 529
  40. theorem OAI.CanonicalCubeSeparation.reopening_separation_with_window line 545
  41. theorem OAI.CanonicalCubeSeparation.exists_reopening_separation line 573