OAI/NumberTheory/DirichletL/Endpoint.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.Endpoint.denominator line 14
  2. def OAI.SevenEighths.Endpoint.primeWeight line 16
  3. def OAI.SevenEighths.Endpoint.balanceDenominator line 18
  4. def OAI.SevenEighths.Endpoint.certificateWeight line 21
  5. def OAI.SevenEighths.Endpoint.balancedCutoff line 23
  6. def OAI.SevenEighths.Endpoint.balancedRowCount line 26
  7. def OAI.SevenEighths.Endpoint.balancedExponent line 29
  8. theorem OAI.SevenEighths.Endpoint.denominator_bounds line 33
  9. theorem OAI.SevenEighths.Endpoint.primeWeight_bounds line 38
  10. theorem OAI.SevenEighths.Endpoint.balanceDenominator_bounds line 45
  11. theorem OAI.SevenEighths.Endpoint.endpoint_identity line 58
  12. theorem OAI.SevenEighths.Endpoint.balanced_endpoint_margin line 68
  13. theorem OAI.SevenEighths.Endpoint.balanced_endpoint_strict line 102