OAI/MathematicalPhysics/NavierStokes/Material/Encoding.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Alternating.Memory.fraction line 8
  2. def OAI.Alternating.Memory.AllowedDigits line 12
  3. def OAI.Alternating.Memory.tailBound line 15
  4. theorem OAI.Alternating.Memory.fraction_nil line 17
  5. theorem OAI.Alternating.Memory.fraction_cons line 19
  6. theorem OAI.Alternating.Memory.fraction_nonneg line 22
  7. theorem OAI.Alternating.Memory.tailBound_nonneg line 27
  8. theorem OAI.Alternating.Memory.tailBound_lt_one line 32
  9. theorem OAI.Alternating.Memory.fraction_le_tailBound line 37
  10. theorem OAI.Alternating.Memory.fraction_lt_one line 55
  11. theorem OAI.Alternating.Memory.fraction_mem_digit_interval line 59
  12. theorem OAI.Alternating.Memory.fraction_append line 67
  13. theorem OAI.Alternating.Memory.fraction_replicate_zero line 75
  14. def OAI.Alternating.Memory.pad line 81
  15. theorem OAI.Alternating.Memory.pad_length line 84
  16. theorem OAI.Alternating.Memory.fraction_pad line 87
  17. theorem OAI.Alternating.Memory.allowedDigits_pad line 90
  18. theorem OAI.Alternating.Memory.fraction_denominator line 98
  19. theorem OAI.Alternating.Memory.fraction_padded_denominator line 111
  20. structure OAI.Alternating.Memory.Block line 115
  21. def OAI.Alternating.Memory.Block.digits line 125
  22. def OAI.Alternating.Memory.Block.code line 128
  23. def OAI.Alternating.Memory.Block.leftCode line 129
  24. def OAI.Alternating.Memory.Block.rightCode line 130
  25. theorem OAI.Alternating.Memory.Block.digits_length line 132
  26. theorem OAI.Alternating.Memory.Block.digits_allowed line 136
  27. theorem OAI.Alternating.Memory.Block.code_formula line 145
  28. theorem OAI.Alternating.Memory.Block.code_nonneg line 150
  29. theorem OAI.Alternating.Memory.Block.code_le line 153
  30. theorem OAI.Alternating.Memory.Block.code_denominator line 156
  31. theorem OAI.Alternating.Memory.Block.left_denominator line 160
  32. theorem OAI.Alternating.Memory.Block.right_denominator line 164
  33. theorem OAI.Alternating.Memory.Block.tail_mem line 168
  34. theorem OAI.Alternating.Memory.Block.right_mem line 182