OAI/Computability/MinUncut/Estimates/Bridge.lean

GitHub source file

81 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncut.SourceBridge.boolField line 15
  2. def OAI.MinUncut.SourceBridge.fieldBool line 17
  3. lemma OAI.MinUncut.SourceBridge.boolField_fieldBool line 19
  4. lemma OAI.MinUncut.SourceBridge.fieldBool_boolField line 22
  5. def OAI.MinUncut.SourceBridge.equation line 25
  6. lemma OAI.MinUncut.SourceBridge.satisfied_equation line 28
  7. def OAI.MinUncut.SourceBridge.equations line 34
  8. instance OAI.MinUncut.SourceBridge.entriesNonempty line 37
  9. lemma OAI.MinUncut.SourceBridge.sum_list_count line 40
  10. lemma OAI.MinUncut.SourceBridge.sum_satisfied line 51
  11. lemma OAI.MinUncut.SourceBridge.fraction_eq line 58
  12. lemma OAI.MinUncut.SourceBridge.fraction_eq_assignment line 65
  13. lemma OAI.MinUncut.SourceBridge.source_sound line 70
  14. lemma OAI.MinUncut.SourceBridge.source_complete line 82
  15. lemma OAI.MinUncut.Costed.SourceWords.flatMap_word line 101
  16. lemma OAI.MinUncut.Costed.SourceWords.input_word line 117
  17. lemma OAI.MinUncut.Costed.SourceWords.input_name line 125
  18. lemma OAI.MinUncut.Costed.SourceWords.input_rhs line 131
  19. def OAI.MinUncut.Outer.LocalTemplate.width line 148
  20. abbrev OAI.MinUncut.Outer.LocalTemplate.Alphabet line 149
  21. lemma OAI.MinUncut.Outer.LocalTemplate.slot_width line 151
  22. def OAI.MinUncut.Outer.LocalTemplate.alphabetEquiv line 155
  23. def OAI.MinUncut.Outer.LocalTemplate.formsPull line 168
  24. lemma OAI.MinUncut.Outer.LocalTemplate.formsPull_apply line 171
  25. def OAI.MinUncut.Outer.LocalTemplate.facesPull line 174
  26. lemma OAI.MinUncut.Outer.LocalTemplate.facesPull_eq line 177
  27. lemma OAI.MinUncut.Outer.LocalTemplate.facesPull_label line 183
  28. def OAI.MinUncut.Outer.LocalTemplate.samplePull line 190
  29. lemma OAI.MinUncut.Outer.LocalTemplate.noiseWeight_pull line 194
  30. lemma OAI.MinUncut.Outer.LocalTemplate.localWeight_pull line 204
  31. def OAI.MinUncut.Outer.LocalTemplate.localSampleEquiv line 213
  32. lemma OAI.MinUncut.Outer.LocalTemplate.localSample_weight line 217
  33. def OAI.MinUncut.Outer.SampleEnumeration.testQuery line 231
  34. lemma OAI.MinUncut.Outer.SampleEnumeration.testQuery_eq line 245
  35. def OAI.MinUncut.Outer.SampleEnumeration.hidden line 256
  36. lemma OAI.MinUncut.Outer.SampleEnumeration.hidden_eq line 259
  37. def OAI.MinUncut.Outer.SampleEnumeration.rawQuery line 263
  38. def OAI.MinUncut.Outer.SampleEnumeration.query line 270
  39. lemma OAI.MinUncut.Outer.SampleEnumeration.query_eq line 275
  40. def OAI.MinUncut.Outer.SampleEnumeration.demand line 290
  41. lemma OAI.MinUncut.Outer.SampleEnumeration.demand_eq line 294
  42. def OAI.MinUncut.Outer.LocalTemplate.projectSlot line 308
  43. def OAI.MinUncut.Outer.LocalTemplate.project line 312
  44. def OAI.MinUncut.Outer.LocalTemplate.decode line 315
  45. def OAI.MinUncut.Outer.LocalTemplate.originTable line 318
  46. lemma OAI.MinUncut.Outer.LocalTemplate.slotCount_width line 320
  47. lemma OAI.MinUncut.Outer.LocalTemplate.slotProjection_cast line 323
  48. lemma OAI.MinUncut.Outer.LocalTemplate.alphabetEquiv_projection line 328
  49. lemma OAI.MinUncut.Outer.LocalTemplate.alphabetEquiv_zero line 334
  50. lemma OAI.MinUncut.Outer.LocalTemplate.decodeSlot line 339
  51. lemma OAI.MinUncut.Outer.LocalTemplate.alphabetEquiv_decode line 348
  52. lemma OAI.MinUncut.Outer.LocalTemplate.extend_second_rep line 354
  53. lemma OAI.MinUncut.Outer.LocalTemplate.extend_first_rep line 365
  54. lemma OAI.MinUncut.Outer.LocalTemplate.first_base line 381
  55. lemma OAI.MinUncut.Outer.LocalTemplate.second_base line 387
  56. abbrev OAI.MinUncut.Outer.LocalTemplate.Index line 397
  57. instance OAI.MinUncut.Outer.LocalTemplate.indexFintype line 400
  58. def OAI.MinUncut.Outer.LocalTemplate.occurrence line 402
  59. def OAI.MinUncut.Outer.LocalTemplate.weight line 416
  60. def OAI.MinUncut.Outer.LocalTemplate.repetitions line 419
  61. lemma OAI.MinUncut.Outer.LocalTemplate.occurrence_weight line 422
  62. lemma OAI.MinUncut.Outer.LocalTemplate.weight_nonneg line 431
  63. lemma OAI.MinUncut.Outer.LocalTemplate.weight_den line 436
  64. lemma OAI.MinUncut.Outer.LocalTemplate.occurrence_multiplicity line 443
  65. structure OAI.MinUncut.Outer.LocalTemplate.Query line 464
  66. def OAI.MinUncut.Outer.LocalTemplate.query line 469
  67. def OAI.MinUncut.Outer.LocalTemplate.Query.realize line 477
  68. lemma OAI.MinUncut.Outer.LocalTemplate.query_realize line 489
  69. structure OAI.MinUncut.Outer.LocalTemplate.Signature line 499
  70. def OAI.MinUncut.Outer.LocalTemplate.signature line 503
  71. def OAI.MinUncut.Outer.LocalTemplate.Signature.Valid line 506
  72. def OAI.MinUncut.Outer.LocalTemplate.Signature.origin line 509
  73. lemma OAI.MinUncut.Outer.LocalTemplate.signature_valid line 512
  74. lemma OAI.MinUncut.Outer.LocalTemplate.signature_origin line 516
  75. def OAI.MinUncut.Outer.LocalTemplate.Query.leftBase line 520
  76. def OAI.MinUncut.Outer.LocalTemplate.Query.leftTable line 523
  77. def OAI.MinUncut.Outer.LocalTemplate.Query.rightTable line 528
  78. def OAI.MinUncut.Outer.LocalTemplate.Query.localSign line 531
  79. lemma OAI.MinUncut.Outer.LocalTemplate.Query.left_extended line 534
  80. lemma OAI.MinUncut.Outer.LocalTemplate.Query.right_extended line 548
  81. lemma OAI.MinUncut.Outer.LocalTemplate.Query.signed_equal line 555