OAI/Combinatorics/UniformKServer/EpochAlphaStatic.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Parameter changes inside one actual held-vector epoch: sparse coordinates when the held side reference is unchanged, side mass otherwise.

  1. theorem OAI.UniformKServer.EpochAlphaStatic.dominant_base line 17
  2. theorem OAI.UniformKServer.EpochAlphaStatic.config_regular line 22
  3. theorem OAI.UniformKServer.EpochAlphaStatic.config_marked line 28
  4. theorem OAI.UniformKServer.EpochAlphaStatic.config_singleton line 35
  5. theorem OAI.UniformKServer.EpochAlphaStatic.singleton_zero line 42
  6. theorem OAI.UniformKServer.EpochAlphaStatic.nonempty_of_input line 47
  7. theorem OAI.UniformKServer.EpochAlphaStatic.marked_bound line 57
  8. theorem OAI.UniformKServer.EpochAlphaStatic.same_epoch line 83