OAI/NumberTheory/Jacobsthal/Partitions/MeshStationary.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.Erdos970Dependency.MeshStationary.mesh line 14
  2. def OAI.Erdos970.Erdos970Dependency.MeshStationary.point line 15
  3. def OAI.Erdos970.Erdos970Dependency.MeshStationary.weight line 16
  4. theorem OAI.Erdos970.Erdos970Dependency.MeshStationary.mesh_nonneg line 18
  5. theorem OAI.Erdos970.Erdos970Dependency.MeshStationary.mesh_pos line 20
  6. theorem OAI.Erdos970.Erdos970Dependency.MeshStationary.mesh_le_one line 25
  7. theorem OAI.Erdos970.Erdos970Dependency.MeshStationary.mesh_mul line 29
  8. theorem OAI.Erdos970.Erdos970Dependency.MeshStationary.point_ge_one line 33
  9. theorem OAI.Erdos970.Erdos970Dependency.MeshStationary.point_ge_two line 38
  10. theorem OAI.Erdos970.Erdos970Dependency.MeshStationary.point_nonneg line 43
  11. theorem OAI.Erdos970.Erdos970Dependency.MeshStationary.point_succ line 46
  12. theorem OAI.Erdos970.Erdos970Dependency.MeshStationary.weight_nonneg line 51
  13. theorem OAI.Erdos970.Erdos970Dependency.MeshStationary.weight_le_two line 53
  14. theorem OAI.Erdos970.Erdos970Dependency.MeshStationary.weight_cost_le_twenty line 58
  15. theorem OAI.Erdos970.Erdos970Dependency.MeshStationary.reciprocal_drop_le line 63
  16. theorem OAI.Erdos970.Erdos970Dependency.MeshStationary.reciprocal_telescope line 70
  17. theorem OAI.Erdos970.Erdos970Dependency.MeshStationary.even_row_count line 76
  18. theorem OAI.Erdos970.Erdos970Dependency.MeshStationary.row_card line 99
  19. theorem OAI.Erdos970.Erdos970Dependency.MeshStationary.point_last line 103
  20. theorem OAI.Erdos970.Erdos970Dependency.MeshStationary.reciprocal_sum_lower line 109
  21. theorem OAI.Erdos970.Erdos970Dependency.MeshStationary.leading_sum_le line 125
  22. theorem OAI.Erdos970.Erdos970Dependency.MeshStationary.correction_sum_le line 151
  23. theorem OAI.Erdos970.Erdos970Dependency.MeshStationary.full_row_sum_le line 169
  24. theorem OAI.Erdos970.Erdos970Dependency.MeshStationary.odd_row_weighted line 192
  25. theorem OAI.Erdos970.Erdos970Dependency.MeshStationary.even_row_literal line 213
  26. theorem OAI.Erdos970.Erdos970Dependency.MeshStationary.odd_row_literal line 218