OAI/Combinatorics/UniformKServer/AlphaFiniteLedger.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The actual alpha trajectory has an all-step finite-law movement ledger. Filtering coefficients are the primitives' proved affine coefficients and are measured before refresh tests. Parameter jumps remain their exact signed values for the subsequent sparse-charge estimate.

  1. def OAI.UniformKServer.AlphaFiniteLedger.potential line 20
  2. def OAI.UniformKServer.AlphaFiniteLedger.movement line 23
  3. def OAI.UniformKServer.AlphaFiniteLedger.jump line 26
  4. def OAI.UniformKServer.AlphaFiniteLedger.coefficient line 30
  5. theorem OAI.UniformKServer.AlphaFiniteLedger.coefficient_bound line 34
  6. theorem OAI.UniformKServer.AlphaFiniteLedger.coefficient_measurable line 42
  7. theorem OAI.UniformKServer.AlphaFiniteLedger.frozen_change line 51
  8. theorem OAI.UniformKServer.AlphaFiniteLedger.step_bound line 75
  9. theorem OAI.UniformKServer.AlphaFiniteLedger.budget line 108