OAI/Computability/StarHeight/ShiftTable.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GeneralizedStarHeight.FiniteProduct.DependsOn line 16
  2. lemma OAI.GeneralizedStarHeight.FiniteProduct.DependsOn.mono line 19
  3. def OAI.GeneralizedStarHeight.FiniteProduct.splice line 24
  4. lemma OAI.GeneralizedStarHeight.FiniteProduct.splice_eqOn_left line 28
  5. lemma OAI.GeneralizedStarHeight.FiniteProduct.splice_eqOn_right line 34
  6. lemma OAI.GeneralizedStarHeight.FiniteProduct.splice_splice line 41
  7. def OAI.GeneralizedStarHeight.FiniteProduct.cylinderEquiv line 47
  8. lemma OAI.GeneralizedStarHeight.FiniteProduct.independent_of_disjoint_support line 67
  9. lemma OAI.GeneralizedStarHeight.FiniteProduct.DependsOn.compl line 83
  10. lemma OAI.GeneralizedStarHeight.FiniteProduct.DependsOn.inter line 88
  11. lemma OAI.GeneralizedStarHeight.FiniteProduct.probability_inter line 94
  12. def OAI.GeneralizedStarHeight.FiniteProduct.agreementEquiv line 102
  13. lemma OAI.GeneralizedStarHeight.FiniteProduct.probability_agreement line 123
  14. lemma OAI.GeneralizedStarHeight.FiniteProduct.agreement_dependsOn line 145
  15. def OAI.GeneralizedStarHeight.FiniteProduct.allEvents line 151
  16. def OAI.GeneralizedStarHeight.FiniteProduct.supportUnion line 154
  17. lemma OAI.GeneralizedStarHeight.FiniteProduct.allEvents_dependsOn line 157
  18. lemma OAI.GeneralizedStarHeight.FiniteProduct.probability_allEvents line 167
  19. def OAI.GeneralizedStarHeight.FiniteProduct.centeredEquiv line 193
  20. def OAI.GeneralizedStarHeight.FiniteProduct.translationEquiv line 203
  21. def OAI.GeneralizedStarHeight.ShiftCombinatorics.offLine line 221
  22. lemma OAI.GeneralizedStarHeight.ShiftCombinatorics.update_ne_center line 224
  23. lemma OAI.GeneralizedStarHeight.ShiftCombinatorics.offLine_pairwise line 229
  24. lemma OAI.GeneralizedStarHeight.ShiftCombinatorics.card_offLine line 238
  25. lemma OAI.GeneralizedStarHeight.ShiftCombinatorics.centered_line_iff line 250
  26. def OAI.GeneralizedStarHeight.ShiftCombinatorics.starSupport line 266
  27. def OAI.GeneralizedStarHeight.ShiftCombinatorics.badEvent line 269
  28. lemma OAI.GeneralizedStarHeight.ShiftCombinatorics.badEvent_dependsOn line 274
  29. lemma OAI.GeneralizedStarHeight.ShiftCombinatorics.probability_badEvent line 286
  30. abbrev OAI.GeneralizedStarHeight.ShiftCombinatorics.CenterCode line 312
  31. def OAI.GeneralizedStarHeight.ShiftCombinatorics.centerOfCode line 314
  32. def OAI.GeneralizedStarHeight.ShiftCombinatorics.nearCenters line 319
  33. lemma OAI.GeneralizedStarHeight.ShiftCombinatorics.mem_nearCenters line 323
  34. lemma OAI.GeneralizedStarHeight.ShiftCombinatorics.card_nearCenters line 328
  35. lemma OAI.GeneralizedStarHeight.ShiftCombinatorics.restore_center line 339
  36. lemma OAI.GeneralizedStarHeight.ShiftCombinatorics.mem_nearCenters_of_shared line 344
  37. def OAI.GeneralizedStarHeight.ShiftTableProperty line 369
  38. theorem OAI.GeneralizedStarHeight.exists_shift_table_length line 374
  39. theorem OAI.GeneralizedStarHeight.shift_table_at_length line 396
  40. theorem OAI.GeneralizedStarHeight.exists_shift_table line 453