OAI/Combinatorics/UniformKServer/StarLocalCharges.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Pointwise charges which enter the actual finite-law star ledger. In particular marking-side changes and deficit changes are not assumed free.

  1. def OAI.UniformKServer.StarLocalCharges.wholesaleMass line 18
  2. def OAI.UniformKServer.StarLocalCharges.coreChanges line 21
  3. def OAI.UniformKServer.StarLocalCharges.endpoints line 23
  4. theorem OAI.UniformKServer.StarLocalCharges.wholesale_nonneg line 26
  5. theorem OAI.UniformKServer.StarLocalCharges.core_nonneg line 32
  6. theorem OAI.UniformKServer.StarLocalCharges.endpoints_nonneg line 35
  7. theorem OAI.UniformKServer.StarLocalCharges.wholesale_path line 38
  8. theorem OAI.UniformKServer.StarLocalCharges.alpha_changes line 50
  9. theorem OAI.UniformKServer.StarLocalCharges.side_flag_formula line 61
  10. theorem OAI.UniformKServer.StarLocalCharges.side_changes_same line 77
  11. theorem OAI.UniformKServer.StarLocalCharges.side_changes_size line 101
  12. theorem OAI.UniformKServer.StarLocalCharges.side_changes line 127
  13. theorem OAI.UniformKServer.StarLocalCharges.coarse_flex_bound line 138
  14. theorem OAI.UniformKServer.StarLocalCharges.deficit_bound line 148
  15. theorem OAI.UniformKServer.StarLocalCharges.deficit_same line 157
  16. theorem OAI.UniformKServer.StarLocalCharges.deficit_step line 174