OAI/Computability/MinUncut/Estimates/CoefficientMoments.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncut.Outer.coefficientVectors line 15
  2. lemma OAI.MinUncut.Outer.coefficientVectors_surjective line 21
  3. def OAI.MinUncut.Outer.Active line 25
  4. def OAI.MinUncut.Outer.hintRate line 28
  5. lemma OAI.MinUncut.Outer.active_power_product line 30
  6. lemma OAI.MinUncut.Outer.zero_vector_expect line 42
  7. lemma OAI.MinUncut.Outer.active_power_expect line 54
  8. lemma OAI.MinUncut.Outer.coefficient_active_expect line 71
  9. lemma OAI.MinUncut.Outer.hintRate_nonnegative line 80
  10. lemma OAI.MinUncut.Outer.hintRate_lt_one line 89