OAI/MathematicalPhysics/NavierStokes/BalancedTransport/BoxCoding.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BalancedTransport.Coding.disjoint_of_first_difference line 10
  2. def OAI.BalancedTransport.Recorder.Instruction.sourcePrefixes line 28
  3. def OAI.BalancedTransport.Recorder.Instruction.targetPrefixes line 31
  4. theorem OAI.BalancedTransport.Recorder.Instruction.balanced_determinant line 34
  5. theorem OAI.BalancedTransport.Recorder.Row.determinant_one line 47
  6. theorem OAI.BalancedTransport.residual_zero_pressure_solution line 53
  7. theorem OAI.BalancedTransport.Coding.first_difference line 74
  8. theorem OAI.BalancedTransport.Coding.incompatible_intervals_disjoint line 95
  9. theorem OAI.BalancedTransport.Coding.comparable_of_intersection line 105
  10. theorem OAI.BalancedTransport.Coding.common_extensions line 123
  11. def OAI.BalancedTransport.Coding.oddDigit line 132
  12. theorem OAI.BalancedTransport.Coding.oddDigit_pos line 135
  13. theorem OAI.BalancedTransport.Coding.oddDigit_upper line 139
  14. theorem OAI.BalancedTransport.Coding.oddDigit_gap line 144
  15. def OAI.BalancedTransport.Coding.box line 163
  16. def OAI.BalancedTransport.Coding.boxMap line 166
  17. theorem OAI.BalancedTransport.Coding.boxMap_image line 170
  18. theorem OAI.BalancedTransport.Coding.boxMap_sub line 195
  19. def OAI.BalancedTransport.Coding.codedPoint line 202
  20. theorem OAI.BalancedTransport.Coding.codedPoint_mem_box line 205
  21. theorem OAI.BalancedTransport.Coding.boxMap_codedPoint line 213
  22. def OAI.BalancedTransport.Coding.origin line 222
  23. theorem OAI.BalancedTransport.Coding.control_eq_of_box_intersection line 224
  24. theorem OAI.BalancedTransport.Coding.box_compact line 238
  25. def OAI.BalancedTransport.Recorder.placement line 257
  26. theorem OAI.BalancedTransport.Recorder.placement_halt line 260
  27. theorem OAI.BalancedTransport.Recorder.placement_positive line 263
  28. theorem OAI.BalancedTransport.Recorder.placement_injective line 266
  29. def OAI.BalancedTransport.Recorder.Instruction.sourceBox line 276
  30. def OAI.BalancedTransport.Recorder.Instruction.targetBox line 280
  31. theorem OAI.BalancedTransport.Recorder.source_boxes_disjoint line 284
  32. theorem OAI.BalancedTransport.Recorder.target_boxes_disjoint line 312
  33. def OAI.BalancedTransport.Recorder.base line 347
  34. def OAI.BalancedTransport.Recorder.digit line 350
  35. theorem OAI.BalancedTransport.Recorder.base_pos line 353
  36. theorem OAI.BalancedTransport.Recorder.digit_pos line 355
  37. theorem OAI.BalancedTransport.Recorder.digit_upper line 358
  38. theorem OAI.BalancedTransport.Recorder.digit_gap line 361