OAI/Analysis/RecorderRadix/Codes.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Infinite radix codes and exact rational values for eventually constant tails.

  1. def OAI.Solenoidal.Radix.code line 10
  2. theorem OAI.Solenoidal.Radix.inv_base_lt_one line 13
  3. theorem OAI.Solenoidal.Radix.summable_majorant line 18
  4. theorem OAI.Solenoidal.Radix.tsum_majorant line 23
  5. theorem OAI.Solenoidal.Radix.summable_code line 33
  6. theorem OAI.Solenoidal.Radix.code_bounds line 44
  7. theorem OAI.Solenoidal.Radix.code_unfold line 58
  8. theorem OAI.Solenoidal.Radix.code_mem_first line 72
  9. theorem OAI.Solenoidal.Radix.pop_code line 77
  10. theorem OAI.Solenoidal.Radix.code_constant line 82
  11. theorem OAI.Solenoidal.Radix.code_eventually_constant line 93
  12. def OAI.Solenoidal.Radix.cons line 106
  13. theorem OAI.Solenoidal.Radix.code_cons line 110
  14. def OAI.Solenoidal.Radix.finiteCode line 113
  15. theorem OAI.Solenoidal.Radix.code_is_finiteCode line 119