OAI/Computability/MinUncut/Search/RationalBasics.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncut.Inner.rationalSigma line 12
  2. def OAI.MinUncut.Inner.rationalEta line 13
  3. def OAI.MinUncut.Inner.rationalR line 14
  4. def OAI.MinUncut.Inner.rationalT line 15
  5. lemma OAI.MinUncut.Inner.ceil_rat_real line 17
  6. lemma OAI.MinUncut.Inner.rationalSigma_cast line 22
  7. lemma OAI.MinUncut.Inner.rationalEta_cast line 24
  8. lemma OAI.MinUncut.Inner.rationalR_eq line 26
  9. lemma OAI.MinUncut.Inner.rationalT_eq line 28
  10. lemma OAI.MinUncut.Inner.rho_even line 33
  11. lemma OAI.MinUncut.Inner.cutoff_tail line 39
  12. lemma OAI.MinUncut.Inner.exists_finite_cutoff line 54
  13. lemma OAI.MinUncut.Inner.pairClass_card_le line 70
  14. lemma OAI.MinUncut.Inner.row_card line 74
  15. lemma OAI.MinUncut.Outer.edgeMean_abs_difference line 92
  16. def OAI.MinUncut.Outer.ProofFamily.finiteErrors line 105
  17. def OAI.MinUncut.Outer.ProofFamily.finiteCost line 116
  18. def OAI.MinUncut.Outer.budgetWeight line 120
  19. lemma OAI.MinUncut.Outer.rational_source_bounds line 123
  20. lemma OAI.MinUncut.Outer.ProofFamily.finiteErrors_difference line 135
  21. lemma OAI.MinUncut.Outer.ProofFamily.finiteCost_difference line 157