OAI/Computability/MinUncut/Estimates/IndexedLists.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MinUncut.Outer.IndexedLists line 12
  2. def OAI.MinUncut.Outer.IndexedLists.numbered line 18
  3. def OAI.MinUncut.Outer.IndexedLists.matches line 22
  4. lemma OAI.MinUncut.Outer.IndexedLists.numbered_matches line 28
  5. theorem OAI.MinUncut.Outer.IndexedLists.shared_soundness line 36
  6. def OAI.MinUncut.Outer.tupleProductEquiv line 56
  7. lemma OAI.MinUncut.Outer.expect_split_tuple line 62
  8. lemma OAI.MinUncut.Outer.hiddenSet_card line 72
  9. lemma OAI.MinUncut.Outer.IndexedLists.shared_soundness_split line 75
  10. def OAI.MinUncut.Outer.backgroundMean line 91
  11. lemma OAI.MinUncut.Outer.IndexedLists.full_soundness line 98
  12. abbrev OAI.MinUncut.Outer.BackgroundStatistic line 123
  13. lemma OAI.MinUncut.Outer.backgroundMean_mono line 128
  14. lemma OAI.MinUncut.Outer.backgroundMean_add line 140
  15. lemma OAI.MinUncut.Outer.backgroundMean_mul line 147
  16. lemma OAI.MinUncut.Outer.backgroundMean_const line 153