OAI/NumberTheory/Jacobsthal/Sieve/LinearSieveFunctions.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.NumberTheoryLean.LinearSieveFunctions.plus line 15
  2. theorem OAI.Erdos970.NumberTheoryLean.LinearSieveFunctions.plus_continuous line 17
  3. theorem OAI.Erdos970.NumberTheoryLean.LinearSieveFunctions.plus_initial line 19
  4. def OAI.Erdos970.NumberTheoryLean.LinearSieveFunctions.f line 21
  5. def OAI.Erdos970.NumberTheoryLean.LinearSieveFunctions.F line 24
  6. def OAI.Erdos970.NumberTheoryLean.LinearSieveFunctions.startingExtension line 27
  7. theorem OAI.Erdos970.NumberTheoryLean.LinearSieveFunctions.f_initial line 29
  8. theorem OAI.Erdos970.NumberTheoryLean.LinearSieveFunctions.f_eq_difference line 31
  9. theorem OAI.Erdos970.NumberTheoryLean.LinearSieveFunctions.plus_add_rho_initial line 38
  10. theorem OAI.Erdos970.NumberTheoryLean.LinearSieveFunctions.mass_f line 45
  11. theorem OAI.Erdos970.NumberTheoryLean.LinearSieveFunctions.mass_F line 50
  12. theorem OAI.Erdos970.NumberTheoryLean.LinearSieveFunctions.F_initial line 55
  13. theorem OAI.Erdos970.NumberTheoryLean.LinearSieveFunctions.f_continuousAt_of_ne_zero line 60
  14. theorem OAI.Erdos970.NumberTheoryLean.LinearSieveFunctions.f_continuous line 68
  15. theorem OAI.Erdos970.NumberTheoryLean.LinearSieveFunctions.F_continuousAt line 79
  16. theorem OAI.Erdos970.NumberTheoryLean.LinearSieveFunctions.gap_identity line 85
  17. theorem OAI.Erdos970.NumberTheoryLean.LinearSieveFunctions.mass_f_hasDerivAt line 93
  18. theorem OAI.Erdos970.NumberTheoryLean.LinearSieveFunctions.mass_F_hasDerivAt line 110
  19. theorem OAI.Erdos970.NumberTheoryLean.LinearSieveFunctions.F_continuousOn line 127
  20. theorem OAI.Erdos970.NumberTheoryLean.LinearSieveFunctions.mass_F_initial line 131
  21. theorem OAI.Erdos970.NumberTheoryLean.LinearSieveFunctions.mass_f_integral line 135
  22. theorem OAI.Erdos970.NumberTheoryLean.LinearSieveFunctions.mass_F_integral line 149
  23. theorem OAI.Erdos970.NumberTheoryLean.LinearSieveFunctions.f_first_formula line 162
  24. theorem OAI.Erdos970.NumberTheoryLean.LinearSieveFunctions.startingExtension_eq_f line 183
  25. theorem OAI.Erdos970.NumberTheoryLean.LinearSieveFunctions.gap_pos line 186