OAI/Combinatorics/UniformKServer/AlphaPrepared.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Common-core prepared states can be evaluated in either parameter domain. The zero-weight case is proved separately; there is no hidden division by a small core mass.

  1. theorem OAI.UniformKServer.AlphaPrepared.zero_of_sum line 18
  2. theorem OAI.UniformKServer.AlphaPrepared.prepared_state line 24
  3. theorem OAI.UniformKServer.AlphaPrepared.bound line 45
  4. theorem OAI.UniformKServer.AlphaPrepared.jump line 58