OAI/Combinatorics/BalancedRyser/Local/LocalKernel.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.Local.KernelBridge.encodeTuple line 16
  2. def OAI.Balanced.Local.KernelBridge.encodeChoice line 17
  3. theorem OAI.Balanced.Local.KernelBridge.decode_encode_tuple line 19
  4. theorem OAI.Balanced.Local.KernelBridge.decode_encode_choice line 22
  5. theorem OAI.Balanced.Local.KernelBridge.encode_decode_tuple line 25
  6. theorem OAI.Balanced.Local.KernelBridge.encode_decode_choice line 28
  7. def OAI.Balanced.Local.KernelBridge.canonicalRetention line 33
  8. theorem OAI.Balanced.Local.KernelBridge.retained_tuple_injective line 65
  9. theorem OAI.Balanced.Local.KernelBridge.offsetProbability_eq_card line 85
  10. theorem OAI.Balanced.Local.KernelBridge.offsetProbability_eq_canonical line 91
  11. theorem OAI.Balanced.Local.KernelBridge.offsetProbability_nonneg line 106
  12. theorem OAI.Balanced.Local.KernelBridge.offsetProbability_le_one line 112
  13. theorem OAI.Balanced.Local.KernelBridge.offsetProbability_mono line 120
  14. theorem OAI.Balanced.Local.KernelBridge.selectedProbability_nonneg line 131
  15. theorem OAI.Balanced.Local.KernelBridge.selectedProbability_le_of_fixed_offset line 144
  16. theorem OAI.Balanced.Local.KernelBridge.selectedProbability_le_one line 156
  17. theorem OAI.Balanced.Local.KernelBridge.selectedProbability_mono line 170
  18. theorem OAI.Balanced.Local.KernelBridge.selected_prescription_and_offset_le line 187
  19. theorem OAI.Balanced.Local.KernelBridge.selected_prescription_le line 227