OAI/NumberTheory/DirichletL/CubicSieve/CubeBlocks.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SecondPassArithmetic.globalFirstCoreRows_integrated_transfer line 84
  2. structure OAI.SecondPassArithmetic.GlobalCubeBlock line 170
  3. def OAI.SecondPassArithmetic.GlobalCubeBlock.withCommon line 177
  4. def OAI.SecondPassArithmetic.GlobalFirstData.block line 183
  5. theorem OAI.SecondPassArithmetic.GlobalFirstData.block_withCommon line 184
  6. theorem OAI.SecondPassArithmetic.GlobalFirstData.withCommon_block line 185
  7. def OAI.SecondPassArithmetic.globalCubePool line 190
  8. def OAI.SecondPassArithmetic.globalFirstFamilySet line 192
  9. theorem OAI.SecondPassArithmetic.sum_globalFirstFamilySet line 195
  10. theorem OAI.SecondPassArithmetic.mem_globalFirstFamilySet line 213
  11. def OAI.SecondPassArithmetic.globalCubeColumnScale line 223
  12. def OAI.SecondPassArithmetic.globalCubeCoefficient line 226
  13. theorem OAI.SecondPassArithmetic.globalFirstCoefficient_block line 230
  14. def OAI.SecondPassArithmetic.globalCubeInputFamilyEnergy line 236
  15. def OAI.SecondPassArithmetic.globalFirstFamilyWeight line 244
  16. theorem OAI.SecondPassArithmetic.globalFirstFiniteEnergy_integral_sum line 250
  17. theorem OAI.SecondPassArithmetic.globalCubeInputFamilyEnergy_eq_integrated_rows line 267
  18. theorem OAI.SecondPassArithmetic.globalChild_large_radial_bound line 302
  19. def OAI.InitialMeanSquare.conjugateMonoid line 368
  20. def OAI.InitialMeanSquare.mobiusRow line 377
  21. lemma OAI.InitialMeanSquare.star_mobiusRow line 381
  22. lemma OAI.InitialMeanSquare.mobiusRow_norm line 397
  23. theorem OAI.InitialMeanSquare.mobiusRow_smoothed_source line 406
  24. theorem OAI.InitialMeanSquare.mobiusRow_finite_source line 421
  25. def OAI.CompletedGauss.PowerfulIdeal line 451
  26. theorem OAI.CompletedGauss.powerful_squarefree_dvd_squarePart line 454
  27. theorem OAI.CompletedGauss.powerful_exists_square_cube line 473
  28. def OAI.CompletedGauss.powerfulBase line 487
  29. theorem OAI.CompletedGauss.powerfulBase_spec line 490
  30. theorem OAI.CompletedGauss.powerfulBase_injective_on_fiber line 495
  31. theorem OAI.CompletedGauss.powerfulBase_norm_bound line 500
  32. theorem OAI.CompletedGauss.powerful_fiber_count line 537
  33. theorem OAI.CompletedGauss.powerful_ideal_count_log line 566
  34. theorem OAI.CompletedGauss.powerful_ideal_count line 588