OAI/NumberTheory/DirichletL/CubicSieve/FrequencyBlocks.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SecondPassArithmetic.inputConjugateRow_smoothed_frequency_blocks line 89
  2. theorem OAI.SecondPassArithmetic.firstCoreInputRow_finite_le_frequency_blocks line 121
  3. lemma OAI.SecondPassArithmetic.finiteSquarefreeRow_zero_of_nonempty line 164
  4. theorem OAI.SecondPassArithmetic.inputConjugateRow_zero line 171
  5. theorem OAI.SecondPassArithmetic.firstCoreInputRow_zero line 184
  6. def OAI.SecondPassArithmetic.nonzeroRowMajorantSum line 196
  7. lemma OAI.SecondPassArithmetic.nonzeroRowMajorant_summable line 200
  8. theorem OAI.SecondPassArithmetic.nonzeroRowMajorantSum_eq_sub line 208
  9. theorem OAI.SecondPassArithmetic.finite_nonzero_row_energy_le_majorant line 219
  10. theorem OAI.SecondPassArithmetic.inputConjugateRow_nonzero_correction line 250
  11. theorem OAI.SecondPassArithmetic.firstCoreInputRow_nonzero_correction line 257
  12. theorem OAI.SecondPassArithmetic.firstCoreInputRow_finite_le_corrected_source line 268
  13. lemma OAI.SecondPassArithmetic.firstCoreTest_empty_mass line 295
  14. theorem OAI.SecondPassArithmetic.firstCoreInputRow_integrated_le_corrected_source line 302
  15. lemma OAI.SecondPassArithmetic.span_dvd_of_element_dvd line 357
  16. lemma OAI.SecondPassArithmetic.primeProduct_add line 366
  17. lemma OAI.SecondPassArithmetic.aLabel_dvd_primeProduct line 371
  18. theorem OAI.SecondPassArithmetic.cubeRadical_dvd_jLabel_b0 line 382
  19. def OAI.SecondPassArithmetic.actualSecondTuple line 398
  20. def OAI.SecondPassArithmetic.actualSecondLabel line 410
  21. def OAI.SecondPassArithmetic.actualSecondRow line 414
  22. theorem OAI.SecondPassArithmetic.actualSecondTuple_valid line 419
  23. theorem OAI.SecondPassArithmetic.actualSecondTuple_newLabel line 462
  24. theorem OAI.SecondPassArithmetic.actualSecondTuple_newRow line 468
  25. theorem OAI.SecondPassArithmetic.actualSecondLabel_span line 474
  26. structure OAI.SecondPassArithmetic.SecondSupportData line 490
  27. instance OAI.SecondPassArithmetic.(instance at line 498) line 498
  28. def OAI.SecondPassArithmetic.secondSupportTuple line 503
  29. def OAI.SecondPassArithmetic.secondSupportLabel line 507
  30. def OAI.SecondPassArithmetic.secondSupportNewLabel line 513
  31. def OAI.SecondPassArithmetic.secondSupportRow line 517
  32. theorem OAI.SecondPassArithmetic.secondSupportTuple_newLabel line 521
  33. theorem OAI.SecondPassArithmetic.secondSupportTuple_newRow line 527
  34. theorem OAI.SecondPassArithmetic.secondSupportLabel_span line 532
  35. theorem OAI.SecondPassArithmetic.secondSupportTuple_injective line 537
  36. theorem OAI.SecondPassArithmetic.secondSupportTuple_valid line 555
  37. theorem OAI.SecondPassArithmetic.sector_b0_ne_bot line 567
  38. def OAI.SecondPassArithmetic.secondSectorZ line 573
  39. def OAI.SecondPassArithmetic.secondSectorUd line 576
  40. def OAI.SecondPassArithmetic.secondSectorUe line 579
  41. def OAI.SecondPassArithmetic.secondSectorUv line 582
  42. def OAI.SecondPassArithmetic.secondSectorKap line 585
  43. def OAI.SecondPassArithmetic.actualSecondSectorSource line 602
  44. theorem OAI.SecondPassArithmetic.actual_second_sector_uniform_transfer line 614