OAI/NumberTheory/DirichletL/CubicSieve/CanonicalLogEnergy.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SecondPassIntegration.childEnergy_le_canonicalSmoothed line 85
  2. theorem OAI.SecondPassIntegration.childEnergy_le_canonicalLogEnergy line 98
  3. theorem OAI.SecondPassIntegration.childEnergy_le_canonicalLogEnergy_actual_labels line 113
  4. theorem OAI.CanonicalRowCompletion.fixedChildRow_coefficient_expansion line 144
  5. theorem OAI.CanonicalRowCompletion.reopenedCanonicalRow_integrand line 156
  6. theorem OAI.CanonicalRowCompletion.canonical_bin_separation line 172
  7. theorem OAI.CanonicalRowCompletion.cube_coefficient_restore line 225
  8. theorem OAI.CanonicalRowCompletion.cubeIdeal_row line 234
  9. def OAI.CanonicalRowCompletion.outsideCanonicalBin line 248
  10. theorem OAI.CanonicalRowCompletion.outsideCanonicalBin_separated line 259
  11. theorem OAI.CanonicalRowCompletion.fixedChildRow_zero_of_subunit line 317
  12. theorem OAI.CanonicalRowCompletion.outsideCanonicalRow_zero_of_subunit line 335
  13. def OAI.CanonicalRowCompletion.activeCubeExponents line 348
  14. theorem OAI.CanonicalRowCompletion.outsideCanonicalBin_eq_active line 354
  15. theorem OAI.CanonicalRowCompletion.outsideCanonicalRow_reopened_active line 377
  16. theorem OAI.CanonicalRowCompletion.activeCubeExponents_norm_bound line 391
  17. def OAI.CanonicalRowCompletion.cubeLogIndex line 412
  18. def OAI.CanonicalRowCompletion.cubeLogRange line 416
  19. def OAI.CanonicalRowCompletion.activeCubeLogBin line 419
  20. theorem OAI.CanonicalRowCompletion.activeCubeLogIndex_mem line 423
  21. theorem OAI.CanonicalRowCompletion.activeCubeLogBin_norms line 432
  22. theorem OAI.CanonicalRowCompletion.cubeLogRange_card line 444
  23. theorem OAI.CanonicalRowCompletion.sum_activeCubeLogBins line 448
  24. theorem OAI.CanonicalRowCompletion.outsideCanonicalBin_log_bins line 457
  25. theorem OAI.CanonicalRowCompletion.outsideCanonicalRow_reopened_binned line 467
  26. theorem OAI.SecondPassArithmetic.nonzeroRowMajorantSum_exact_disk line 487
  27. def OAI.SecondPassArithmetic.canonicalTerminalConstant line 507
  28. theorem OAI.SecondPassArithmetic.canonicalTerminalConstant_nonneg line 510
  29. theorem OAI.SecondPassArithmetic.fixedDepthRank_zero_iff line 514
  30. theorem OAI.SecondPassArithmetic.smallColumn_row_le_label line 527
  31. theorem OAI.SecondPassArithmetic.canonicalSmoothedEnergy_uniform_row_bound line 540
  32. theorem OAI.SecondPassArithmetic.canonicalLogEnergy_subunit line 574
  33. theorem OAI.SecondPassArithmetic.canonicalLogEnergy_terminal line 593