OAI/Computability/PerfectCompleteness/Foundations/HierarchicalFrozenTablesLemmas.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.HierarchicalFrozenTables.LowerNodes line 27
  2. def OAI.PerfectCompleteness.HierarchicalFrozenTables.lowerIndex line 30
  3. def OAI.PerfectCompleteness.HierarchicalFrozenTables.knownSpace line 35
  4. theorem OAI.PerfectCompleteness.HierarchicalFrozenTables.knownSpace_le_rowSpace line 38
  5. def OAI.PerfectCompleteness.HierarchicalFrozenTables.knownRows line 43
  6. def OAI.PerfectCompleteness.HierarchicalFrozenTables.sectionMap line 47
  7. theorem OAI.PerfectCompleteness.HierarchicalFrozenTables.sectionMap_spec line 52
  8. theorem OAI.PerfectCompleteness.HierarchicalFrozenTables.determined line 57
  9. abbrev OAI.PerfectCompleteness.HierarchicalFrozenTables.QuotientMatrix line 63
  10. def OAI.PerfectCompleteness.HierarchicalFrozenTables.table line 69
  11. theorem OAI.PerfectCompleteness.HierarchicalFrozenTables.card_accepted_responses_le_two line 76
  12. abbrev OAI.PerfectCompleteness.HierarchicalUsefulness.Coarse line 114
  13. instance OAI.PerfectCompleteness.HierarchicalUsefulness.coarseFintype line 118
  14. def OAI.PerfectCompleteness.HierarchicalUsefulness.observe line 126
  15. def OAI.PerfectCompleteness.HierarchicalUsefulness.mark line 137
  16. def OAI.PerfectCompleteness.HierarchicalUsefulness.table line 142
  17. theorem OAI.PerfectCompleteness.HierarchicalUsefulness.table_isSome line 148
  18. theorem OAI.PerfectCompleteness.HierarchicalUsefulness.table_defined_at_observation line 156
  19. theorem OAI.PerfectCompleteness.HierarchicalUsefulness.useful_upper_mass line 164
  20. abbrev OAI.PerfectCompleteness.HierarchicalInverseAdvice.Input line 199
  21. theorem OAI.PerfectCompleteness.HierarchicalInverseAdvice.mean_adviceMass_ge line 216
  22. abbrev OAI.PerfectCompleteness.KnownSpaceDimension.GeneratorIndex line 249
  23. def OAI.PerfectCompleteness.KnownSpaceDimension.generator line 251
  24. theorem OAI.PerfectCompleteness.KnownSpaceDimension.generator_range line 255
  25. theorem OAI.PerfectCompleteness.KnownSpaceDimension.quadraticSpan_eq_span_range line 268
  26. theorem OAI.PerfectCompleteness.KnownSpaceDimension.card_generatorIndex line 277
  27. theorem OAI.PerfectCompleteness.KnownSpaceDimension.finiteDimensional_quadraticSpan line 282
  28. theorem OAI.PerfectCompleteness.KnownSpaceDimension.finrank_quadraticSpan_le line 287
  29. theorem OAI.PerfectCompleteness.KnownSpaceDimension.finrank_knownSpace_le line 299
  30. theorem OAI.PerfectCompleteness.KnownSpaceDimension.finrank_knownSpace_comap_le line 316
  31. def OAI.PerfectCompleteness.DescendantSpaces.Path.append line 342
  32. theorem OAI.PerfectCompleteness.DescendantSpaces.Path.append_refl line 346
  33. theorem OAI.PerfectCompleteness.DescendantSpaces.Path.append_step line 348
  34. theorem OAI.PerfectCompleteness.DescendantSpaces.Path.append_refl_right line 351
  35. theorem OAI.PerfectCompleteness.DescendantSpaces.Path.append_assoc line 356
  36. theorem OAI.PerfectCompleteness.DescendantSpaces.Path.slotEmbedding_append line 365
  37. theorem OAI.PerfectCompleteness.DescendantSpaces.Path.family_append line 374
  38. theorem OAI.PerfectCompleteness.DescendantSpaces.Path.restriction_append_heq line 380
  39. def OAI.PerfectCompleteness.DescendantSpaces.Path.appendAssignmentEquiv line 390
  40. theorem OAI.PerfectCompleteness.DescendantSpaces.Path.restriction_append line 396
  41. theorem OAI.PerfectCompleteness.DescendantSpaces.Path.restriction_append_comp line 403
  42. theorem OAI.PerfectCompleteness.PathComposition.append_leafPath line 418
  43. theorem OAI.PerfectCompleteness.PathComposition.exists_leafAtNode line 427
  44. def OAI.PerfectCompleteness.PathComposition.leafAtNode line 442
  45. theorem OAI.PerfectCompleteness.PathComposition.leafAtNode_embedding line 446
  46. theorem OAI.PerfectCompleteness.PathComposition.leafAtNode_unique line 451
  47. theorem OAI.PerfectCompleteness.PathComposition.leafPath_split line 458
  48. def OAI.PerfectCompleteness.GeometricCutSplit.PrefixDepth line 476
  49. instance OAI.PerfectCompleteness.GeometricCutSplit.prefixDepthFintype line 480
  50. abbrev OAI.PerfectCompleteness.GeometricCutSplit.Prefix line 489
  51. def OAI.PerfectCompleteness.GeometricCutSplit.prefixPathDepth line 492
  52. def OAI.PerfectCompleteness.GeometricCutSplit.splitDepth line 497
  53. theorem OAI.PerfectCompleteness.GeometricCutSplit.splitDepth_symm_eq_embedding line 508
  54. def OAI.PerfectCompleteness.GeometricCutSplit.castPath line 521
  55. theorem OAI.PerfectCompleteness.GeometricCutSplit.castPath_embedding line 524
  56. def OAI.PerfectCompleteness.GeometricCutSplit.prefixPath line 533
  57. def OAI.PerfectCompleteness.GeometricCutSplit.joinEquiv line 537
  58. def OAI.PerfectCompleteness.GeometricCutSplit.splitEquiv line 542
  59. theorem OAI.PerfectCompleteness.GeometricCutSplit.joinEquiv_apply line 546
  60. theorem OAI.PerfectCompleteness.GeometricCutSplit.join_split line 555
  61. theorem OAI.PerfectCompleteness.GeometricCutSplit.split_embedding line 559
  62. theorem OAI.PerfectCompleteness.GeometricCutSplit.split_embedding_eq line 565
  63. theorem OAI.PerfectCompleteness.GeometricCutSplit.leafPath_split line 571
  64. theorem OAI.PerfectCompleteness.GeometricCutSplit.prefix_nonempty line 576
  65. def OAI.PerfectCompleteness.GeometricCutSplit.prefixLaw line 583
  66. theorem OAI.PerfectCompleteness.GeometricCutSplit.law_split line 588
  67. theorem OAI.PerfectCompleteness.GeometricCutSplit.expectation_split line 602
  68. theorem OAI.PerfectCompleteness.GeometricCutSplit.probability_split line 614
  69. theorem OAI.PerfectCompleteness.GeometricCutMixture.mixture_split line 642
  70. theorem OAI.PerfectCompleteness.GeometricCutMixture.path_mixture_split line 661