OAI/Combinatorics/BalancedRyser/Candidates/CandidateGlobalLineTail.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.CandidateGlobalLine.gatedLineModel_conditional_upper_tail line 16
  2. theorem OAI.Balanced.CandidateGlobalLine.gatedLineModel_upper_tail line 32
  3. def OAI.Balanced.CandidateGlobalLine.globalLineCount line 45
  4. theorem OAI.Balanced.CandidateGlobalLine.globalLineCount_eq_successfulTest line 48
  5. theorem OAI.Balanced.CandidateGlobalLine.gatedLineModel_count_eq line 59
  6. theorem OAI.Balanced.CandidateGlobalLine.globalLineCount_upper_tail line 65
  7. theorem OAI.Balanced.CandidateGlobalLine.globalLineCount_any_upper_tail line 82
  8. theorem OAI.Balanced.CandidateGlobalLine.globalLineCount_all_tendsto_one line 114
  9. theorem OAI.Balanced.CandidateGlobalLine.globalLineCount_all_probability_tendsto_one line 154
  10. theorem OAI.Balanced.CandidateGlobalLine.successfulTest_globalLine_all_probability_tendsto_one line 169