OAI/NumberTheory/DirichletL/CubicSieve/QuantitativePassage.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SecondPassArithmetic.globalTwoPassage_quantitative line 81
  2. def OAI.SecondPassArithmetic.canonicalCubeFirstBlock line 164
  3. theorem OAI.SecondPassArithmetic.canonicalCubeFirstBlock_input_transfer line 181
  4. theorem OAI.SecondPassArithmetic.canonicalTwoPassage_quantitative line 308
  5. theorem OAI.CompletedGauss.completed_branch_count_small_power line 386
  6. theorem OAI.CompletedGauss.sum_completedRowFibers line 420
  7. theorem OAI.CompletedGauss.rowMaskPart_image_card line 431
  8. theorem OAI.CompletedGauss.completed_outer_row_sum_bound line 438
  9. theorem OAI.CompletedGauss.completed_outer_row_small_power line 467
  10. def OAI.CompletedDyadic.kernelTerm line 485
  11. theorem OAI.CompletedDyadic.pow_rpow_comm line 487
  12. theorem OAI.CompletedDyadic.kernelTerm_nonneg line 492
  13. theorem OAI.CompletedDyadic.kernelTerm_le_head line 496
  14. theorem OAI.CompletedDyadic.kernelTerm_le_tail line 502
  15. theorem OAI.CompletedDyadic.ratio_lt_one line 516
  16. theorem OAI.CompletedDyadic.kernel_summable line 519
  17. theorem OAI.CompletedDyadic.kernel_sum_cutoff line 524
  18. theorem OAI.CompletedDyadic.kernel_sum_bound line 548