OAI/NumberTheory/DirichletL/Moments/DivisorBoundary.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.CenteredMomentDivisorBoundary.frozenSlots line 12
  2. def OAI.SevenEighths.CenteredMomentDivisorBoundary.extractedProduct line 15
  3. theorem OAI.SevenEighths.CenteredMomentDivisorBoundary.divisor_dvd_extractedProduct line 19
  4. theorem OAI.SevenEighths.CenteredMomentDivisorBoundary.extractedProduct_ne_zero line 39
  5. theorem OAI.SevenEighths.CenteredMomentDivisorBoundary.actual_divisor_norm_boundary line 46
  6. theorem OAI.SevenEighths.CenteredMomentDivisorBoundary.actual_divisor_log_boundary line 57
  7. def OAI.SevenEighths.CenteredMomentDivisorBoundary.formalReduction line 79
  8. def OAI.SevenEighths.CenteredMomentDivisorBoundary.frozenRatio line 84
  9. theorem OAI.SevenEighths.CenteredMomentDivisorBoundary.formal_reduction_add_ratio line 88
  10. theorem OAI.SevenEighths.CenteredMomentDivisorBoundary.actual_formal_boundary line 103
  11. theorem OAI.SevenEighths.CenteredMomentDivisorBoundary.divisor_dyad_card line 113
  12. theorem OAI.SevenEighths.CenteredMomentDivisorBoundary.paired_raw_divisor_bound line 120