OAI/Combinatorics/BalancedRyser/Local/AlignedStateTransition.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.AlignedListProbability.installCurrentTupleOffsets line 13
  2. theorem OAI.Balanced.AlignedListProbability.installCurrentTupleOffsets_generator line 18
  3. theorem OAI.Balanced.AlignedListProbability.installCurrentTupleOffsets_outside line 26
  4. theorem OAI.Balanced.AlignedListProbability.installCurrentTupleOffsets_agree_old line 37
  5. def OAI.Balanced.AlignedListProbability.generateCurrentState line 50
  6. theorem OAI.Balanced.AlignedListProbability.generateCurrentState_agree_old line 57
  7. theorem OAI.Balanced.AlignedListProbability.generateCurrentState_aligned line 68
  8. theorem OAI.Balanced.AlignedListProbability.installCurrentTupleOffsets_reconstruct line 84
  9. theorem OAI.Balanced.AlignedListProbability.conditionedOffsetProbability_congr_on line 99
  10. theorem OAI.Balanced.AlignedListProbability.current_state_generated_probability line 111
  11. theorem OAI.Balanced.AlignedListProbability.generateCurrentState_freePoint line 128
  12. theorem OAI.Balanced.AlignedListProbability.generateCurrentState_old_left line 143
  13. theorem OAI.Balanced.AlignedListProbability.generateCurrentState_old_right line 164
  14. theorem OAI.Balanced.AlignedListProbability.generateCurrentState_listAligned line 185
  15. theorem OAI.Balanced.AlignedListProbability.full_aligned_state_generated_probability line 205