OAI/Computability/MinUncut/Estimates/WeightedTestLaw.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MinUncut.Outer.LocalSample line 15
  2. def OAI.MinUncut.Outer.noiseWeight line 18
  3. def OAI.MinUncut.Outer.localWeight line 23
  4. lemma OAI.MinUncut.Outer.sum_invcard_mul line 28
  5. lemma OAI.MinUncut.Outer.localWeight_nonneg line 32
  6. lemma OAI.MinUncut.Outer.localWeight_sum line 46
  7. lemma OAI.MinUncut.Outer.noiseWeight_cast line 64
  8. lemma OAI.MinUncut.Outer.localTest_mean line 69
  9. instance OAI.MinUncut.Outer.localSampleFintype line 102
  10. abbrev OAI.MinUncut.Outer.OuterSample line 107
  11. def OAI.MinUncut.Outer.sampleFirst line 110
  12. def OAI.MinUncut.Outer.sampleHidden line 112
  13. abbrev OAI.MinUncut.Outer.sampleSecond line 114
  14. abbrev OAI.MinUncut.Outer.Elementary line 117
  15. instance OAI.MinUncut.Outer.elementaryFintype line 120
  16. def OAI.MinUncut.Outer.elementaryWeight line 125
  17. def OAI.MinUncut.Outer.elementaryQuery line 129
  18. lemma OAI.MinUncut.Outer.elementaryWeight_nonneg line 134
  19. lemma OAI.MinUncut.Outer.expect_prod_type line 140
  20. lemma OAI.MinUncut.Outer.outer_weight_sum line 146
  21. lemma OAI.MinUncut.Outer.elementary_weighted_sum line 153