OAI/Combinatorics/UniformKServer/KeySizePosterior.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The entropy size tracker instantiated by true finite hidden-count data. Its drift estimate is conditional L1 contraction, never event-conditional.

  1. def OAI.UniformKServer.KeySizePosterior.input line 18
  2. theorem OAI.UniformKServer.KeySizePosterior.drift line 47
  3. theorem OAI.UniformKServer.KeySizePosterior.budget line 54