OAI/NumberTheory/DirichletL/CubicSieve/KernelEnergy.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FirstPassCubeLabels.actualFirstKernel line 84
  2. def OAI.FirstPassCubeLabels.firstColumnEnergy line 97
  3. theorem OAI.FirstPassCubeLabels.firstColumnEnergy_nonneg line 108
  4. theorem OAI.FirstPassCubeLabels.actual_first_kernel_energy_bound line 120
  5. theorem OAI.FirstPassCubeLabels.row_union line 177
  6. theorem OAI.FirstPassCubeLabels.mask_union line 183
  7. theorem OAI.FirstPassCubeLabels.row_four_star line 188
  8. def OAI.FirstPassCubeLabels.beforeDilationLabel line 201
  9. def OAI.FirstPassCubeLabels.afterDilationLabel line 209
  10. theorem OAI.FirstPassCubeLabels.beforeDilationLabel_union line 214
  11. theorem OAI.FirstPassCubeLabels.beforeDilationLabel_norm_le_one line 224
  12. theorem OAI.FirstPassCubeLabels.beforeDilationLabel_star_row line 237
  13. theorem OAI.FirstPassCubeLabels.rayIdealRow_eq_supportRow line 257
  14. def OAI.FirstPassCubeLabels.dilatedRayColumn line 269
  15. theorem OAI.FirstPassCubeLabels.rayIdealRow_beforeDilation line 277
  16. def OAI.FirstPassCubeLabels.originalLabelColumn line 310
  17. def OAI.FirstPassCubeLabels.cubeCoreCoefficient line 319
  18. theorem OAI.FirstPassCubeLabels.cubeLogCoefficient_originalLabel line 335
  19. theorem OAI.FirstPassCubeLabels.rayIdealRow_cube_labels line 352
  20. theorem OAI.FirstPassCubeLabels.first_cube_energy_small_power line 375
  21. theorem OAI.FirstPassCubeLabels.normalized_originalLabelColumn line 412
  22. theorem OAI.FirstPassCubeLabels.firstColumnEnergy_original_labels line 422
  23. def OAI.FirstPassCubeLabels.firstDivisorWeight line 459
  24. theorem OAI.FirstPassCubeLabels.retained_first_kernel_energy_bound line 464
  25. theorem OAI.FirstPassCubeLabels.blockRow_norm_le_one line 554
  26. theorem OAI.FirstPassCubeLabels.cubeBaseFactor_norm_le_one line 566
  27. theorem OAI.FirstPassCubeLabels.rayPairWeight_norm_le line 582
  28. def OAI.FirstPassCubeLabels.firstLogDensity line 603
  29. theorem OAI.FirstPassCubeLabels.firstLogDensity_nonneg line 605
  30. theorem OAI.FirstPassCubeLabels.firstLogDensity_integrable line 609
  31. theorem OAI.FirstPassCubeLabels.firstLogDensity_moment_integrable line 617
  32. theorem OAI.FirstPassCubeLabels.two_variable_radial_envelope line 625
  33. theorem OAI.FirstPassCubeLabels.actualFirstKernel_eq_separated line 655
  34. theorem OAI.FirstPassCubeLabels.actual_first_kernel_energy_envelope line 706