OAI/NumberTheory/DirichletL/CubicSieve/SquarefreeTransfer.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SecondPassArithmetic.secondSquarefreeLogNormalizedEnergy line 87
  2. lemma OAI.SecondPassArithmetic.secondSquarefreeLogNormalizedEnergy_nonneg line 95
  3. lemma OAI.SecondPassArithmetic.secondSquarefreeLogNormalizedEnergy_empty line 112
  4. theorem OAI.SecondPassArithmetic.secondSquarefreeLog_normalized_cost line 121
  5. def OAI.SecondPassArithmetic.firstCoreSquarefreeBudget line 155
  6. theorem OAI.SecondPassArithmetic.firstInputFamilyEnergy_squarefree_transfer line 191
  7. structure OAI.SecondPassArithmetic.SquarefreeBudgetData line 260
  8. def OAI.SecondPassArithmetic.firstSquarefreeFamilyBudget line 271
  9. theorem OAI.SecondPassArithmetic.first_passage_squarefree_child_transfer line 285
  10. theorem OAI.FirstPassCubeLabels.actual_first_kernel_full_uniform_envelope line 385
  11. theorem OAI.FirstPassCubeLabels.first_passage_full_uniform_transfer line 442
  12. theorem OAI.SecondPassArithmetic.first_passage_full_uniform_input_family line 550