OAI/Combinatorics/EditApproximation/Geometry/OnlineLinearBits.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The actual finite optimistic-history sum has polynomial encoding length. Its normalized table entries are bounded by the fixed envelopes.

  1. def OAI.EditApproximation.onlineSummandEncodingBudget line 13
  2. def OAI.EditApproximation.onlineLinearEncodingBudget line 16
  3. theorem OAI.EditApproximation.childGain_encoding line 21
  4. theorem OAI.EditApproximation.childDecrement_encoding line 29
  5. theorem OAI.EditApproximation.childGain_abs_le_one line 40
  6. theorem OAI.EditApproximation.childDecrement_abs_le_one line 46
  7. theorem OAI.EditApproximation.rationalOnlineLinear_encoding line 55
  8. theorem OAI.EditApproximation.rationalOnlineLinear_abs line 107