OAI/NumberTheory/DirichletL/CubicSieve/LogSeparation.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CanonicalCubeSeparation.cube_log_bin line 83
  2. lemma OAI.CanonicalCubeSeparation.cube_log_argument line 92
  3. lemma OAI.CanonicalCubeSeparation.cube_half_normalization line 104
  4. lemma OAI.CanonicalCubeSeparation.cube_half_normalization_complex line 119
  5. theorem OAI.CanonicalCubeSeparation.reopening_norm_separation line 125
  6. lemma OAI.CanonicalCubeSeparation.completed_cube_half_weight line 140
  7. lemma OAI.CanonicalCubeSeparation.completed_cube_half_weight_complex line 147
  8. theorem OAI.CanonicalCubeSeparation.completed_cube_norm_separation line 152
  9. def OAI.CanonicalCubeSeparation.separatedCubeCoefficient line 165
  10. lemma OAI.CanonicalCubeSeparation.separatedCubeCoefficient_bound line 168
  11. theorem OAI.CanonicalCubeSeparation.reopening_finite_sum_integrable line 177
  12. theorem OAI.CanonicalCubeSeparation.reopening_finite_sum line 199
  13. theorem OAI.CanonicalRowCompletion.rowTwist_primary_zero_of_mask line 263
  14. theorem OAI.CanonicalRowCompletion.cubeWeight_zero_of_prime_mask line 280
  15. theorem OAI.CanonicalRowCompletion.summand_cube_support line 285
  16. theorem OAI.CanonicalRowCompletion.large_cube_sum_comm line 307
  17. theorem OAI.CanonicalRowCompletion.large_cube_sum_finite line 324
  18. theorem OAI.CanonicalRowCompletion.inner_completed_sum line 346
  19. theorem OAI.CanonicalRowCompletion.outsideCanonicalRow_reopened line 369
  20. theorem OAI.CanonicalRowCompletion.outsideCanonicalRow_reopened_exponents line 399
  21. theorem OAI.CanonicalRowCompletion.cubeWeight_norm_le line 422
  22. def OAI.CanonicalRowCompletion.cubePhase line 435
  23. theorem OAI.CanonicalRowCompletion.cubePhase_norm_le line 438
  24. theorem OAI.CanonicalRowCompletion.cube_weight_scale line 449
  25. def OAI.CanonicalRowCompletion.reopenedCubeCoefficient line 468
  26. theorem OAI.CanonicalRowCompletion.reopenedCubeCoefficient_small_power line 471
  27. theorem OAI.CanonicalRowCompletion.reopenedCubeCoefficient_support line 483
  28. def OAI.SecondPassArithmetic.childLabelRotation line 495
  29. theorem OAI.SecondPassArithmetic.childLabelRotation_injective line 498
  30. theorem OAI.SecondPassArithmetic.childLabelRotation_norm line 510
  31. theorem OAI.SecondPassArithmetic.childLabelRotation_ne_zero line 516
  32. theorem OAI.SecondPassArithmetic.fixedChildRow_label_mul line 527
  33. theorem OAI.SecondPassArithmetic.idealChildRow_eq_rotated line 537
  34. def OAI.SecondPassArithmetic.canonicalSmoothedEnergy line 545
  35. theorem OAI.SecondPassArithmetic.canonicalSmoothedEnergy_nonneg line 550
  36. theorem OAI.SecondPassArithmetic.canonicalSmoothedEnergy_zero_correction line 562
  37. theorem OAI.SecondPassArithmetic.idealChildRow_energy_le_canonical line 572
  38. def OAI.SecondPassArithmetic.canonicalLogEnergy line 611
  39. def OAI.SecondPassArithmetic.orientedLogProfile line 617
  40. theorem OAI.SecondPassArithmetic.fixedSecondTest_zero_profile line 620