OAI/Combinatorics/UniformKServer/SwitchFinite.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Literal causal hysteresis under finite observation laws. The old-rule potential is filtered on every step, before the wholesale/reset decision.

  1. structure OAI.UniformKServer.SwitchFinite.Data line 19
  2. def OAI.UniformKServer.SwitchFinite.mass line 27
  3. def OAI.UniformKServer.SwitchFinite.oldMass line 29
  4. def OAI.UniformKServer.SwitchFinite.rule line 31
  5. def OAI.UniformKServer.SwitchFinite.potential line 36
  6. def OAI.UniformKServer.SwitchFinite.charge line 39
  7. def OAI.UniformKServer.SwitchFinite.wholesale line 42
  8. def OAI.UniformKServer.SwitchFinite.indicator line 45
  9. def OAI.UniformKServer.SwitchFinite.coefficient line 47
  10. theorem OAI.UniformKServer.SwitchFinite.mass_nonneg line 50
  11. theorem OAI.UniformKServer.SwitchFinite.oldMass_nonneg line 53
  12. theorem OAI.UniformKServer.SwitchFinite.rule_valid line 56
  13. theorem OAI.UniformKServer.SwitchFinite.mass_measurable line 60
  14. theorem OAI.UniformKServer.SwitchFinite.rule_measurable line 65
  15. theorem OAI.UniformKServer.SwitchFinite.coefficient_bound line 73
  16. theorem OAI.UniformKServer.SwitchFinite.coefficient_measurable line 80
  17. theorem OAI.UniformKServer.SwitchFinite.flags_error line 89
  18. theorem OAI.UniformKServer.SwitchFinite.affine line 97
  19. theorem OAI.UniformKServer.SwitchFinite.frozen_change line 102