OAI/Computability/PerfectCompleteness/Construction/SourceQuestionOrderLemmas.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.SourceQuestionOrder.questionToTuple line 26
  2. def OAI.PerfectCompleteness.SourceQuestionOrder.tupleToQuestion line 31
  3. theorem OAI.PerfectCompleteness.SourceQuestionOrder.tupleToQuestion_questionToTuple line 35
  4. theorem OAI.PerfectCompleteness.SourceQuestionOrder.questionToTuple_tupleToQuestion line 41
  5. def OAI.PerfectCompleteness.SourceQuestionOrder.questionTupleEquiv line 47
  6. def OAI.PerfectCompleteness.SourceQuestionOrder.sourceOrder line 55
  7. theorem OAI.PerfectCompleteness.SourceQuestionOrder.sourceOrder_length line 60
  8. theorem OAI.PerfectCompleteness.SourceQuestionOrder.sourceOrder_nodup line 65
  9. theorem OAI.PerfectCompleteness.SourceQuestionOrder.mem_sourceOrder line 72
  10. theorem OAI.PerfectCompleteness.SourceQuestionOrder.sourceOrder_toFinset line 82
  11. theorem OAI.PerfectCompleteness.SourceQuestionOrder.sum_map_sourceOrder line 88
  12. def OAI.PerfectCompleteness.SourceQuestionOrder.numberedClauseIDs line 93
  13. theorem OAI.PerfectCompleteness.SourceQuestionOrder.numberedClauseIDs_length line 96
  14. theorem OAI.PerfectCompleteness.SourceQuestionOrder.numberedClauseIDs_tupleToQuestion line 101
  15. theorem OAI.PerfectCompleteness.SourceQuestionOrder.outputBlock_all_eq_sourceOrder line 107
  16. theorem OAI.PerfectCompleteness.SourceQuestionOrder.output_eq_sourceOrder line 116
  17. def OAI.PerfectCompleteness.SourceQuestionOrder.sourceOutputsInTime line 121
  18. def OAI.PerfectCompleteness.TreeCardinality.domainBound line 149
  19. def OAI.PerfectCompleteness.TreeCardinality.functionBound line 152
  20. theorem OAI.PerfectCompleteness.TreeCardinality.domain_card_le line 155
  21. theorem OAI.PerfectCompleteness.TreeCardinality.subspace_card_le line 166
  22. theorem OAI.PerfectCompleteness.TreeCardinality.H_card_le line 177
  23. theorem OAI.PerfectCompleteness.TreeCardinality.square_card_le line 182
  24. def OAI.PerfectCompleteness.TreeCardinality.arraysBound line 187
  25. theorem OAI.PerfectCompleteness.TreeCardinality.arrays_card_le line 191
  26. theorem OAI.PerfectCompleteness.TreeCardinality.source_questions_card line 203
  27. theorem OAI.PerfectCompleteness.TreeCardinality.source_base_card line 209
  28. abbrev OAI.PerfectCompleteness.ChildBlockCardinality.Raw line 228
  29. instance OAI.PerfectCompleteness.ChildBlockCardinality.rawFintype line 232
  30. instance OAI.PerfectCompleteness.ChildBlockCardinality.rawNonempty line 236
  31. def OAI.PerfectCompleteness.ChildBlockCardinality.bound line 240
  32. theorem OAI.PerfectCompleteness.ChildBlockCardinality.card_le line 244
  33. theorem OAI.PerfectCompleteness.ChildBlockCardinality.fintype_card_le line 252
  34. theorem OAI.PerfectCompleteness.ChildBlockCardinality.bound_pos line 257
  35. def OAI.PerfectCompleteness.ChildBlockCardinality.density line 262
  36. theorem OAI.PerfectCompleteness.ChildBlockCardinality.weight_eq line 267
  37. theorem OAI.PerfectCompleteness.ChildBlockCardinality.mean_one line 273
  38. theorem OAI.PerfectCompleteness.ChildBlockCardinality.density_le line 279
  39. theorem OAI.PerfectCompleteness.ChildBlockCardinality.second_moment_le line 286
  40. def OAI.PerfectCompleteness.ChildBlockMixture.component line 310
  41. def OAI.PerfectCompleteness.ChildBlockMixture.reference line 314
  42. def OAI.PerfectCompleteness.ChildBlockMixture.special line 317
  43. def OAI.PerfectCompleteness.ChildBlockMixture.mixture line 321
  44. theorem OAI.PerfectCompleteness.ChildBlockMixture.component_weight line 326
  45. theorem OAI.PerfectCompleteness.ChildBlockMixture.special_weight line 339
  46. theorem OAI.PerfectCompleteness.ChildBlockMixture.observed_variation line 348
  47. theorem OAI.PerfectCompleteness.ChildBlockMixture.actual_observed_variation line 366
  48. theorem OAI.PerfectCompleteness.ChildBlockMixture.conditional_actual_observed_variation line 392
  49. def OAI.PerfectCompleteness.ChildBlockContinuation.continuedSpecial line 431
  50. theorem OAI.PerfectCompleteness.ChildBlockContinuation.continuedSpecial_eq_product line 438
  51. theorem OAI.PerfectCompleteness.ChildBlockContinuation.continuedSpecial_weight line 452
  52. theorem OAI.PerfectCompleteness.ChildBlockContinuation.average_special line 462
  53. theorem OAI.PerfectCompleteness.ChildBlockContinuation.hidden_average line 482
  54. theorem OAI.PerfectCompleteness.ChildBlockContinuation.uniform_average line 488