OAI/Combinatorics/BalancedRyser/Candidates/CandidateGlobalLineModel.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Balanced.CandidateGlobalLine.lineModel line 17
  2. def OAI.Balanced.CandidateGlobalLine.oldLineTest line 19
  3. theorem OAI.Balanced.CandidateGlobalLine.allExposed_overlapCount_eq line 22
  4. theorem OAI.Balanced.CandidateGlobalLine.lineModel_fixed_count_le line 41
  5. theorem OAI.Balanced.CandidateGlobalLine.lineModel_fixed_allExposed line 49
  6. theorem OAI.Balanced.CandidateGlobalLine.lineModel_fixed_allExposed_le line 70
  7. theorem OAI.Balanced.CandidateGlobalLine.lineModel_fixed_overlap_le line 78
  8. theorem OAI.Balanced.CandidateGlobalLine.lineGate_depends line 91
  9. abbrev OAI.Balanced.CandidateGlobalLine.gatedLineModel line 96
  10. theorem OAI.Balanced.CandidateGlobalLine.gatedLineModel_count line 100
  11. theorem OAI.Balanced.CandidateGlobalLine.gatedLineModel_measure line 109
  12. theorem OAI.Balanced.CandidateGlobalLine.gatedLineModel_fixedExpectation line 112
  13. theorem OAI.Balanced.CandidateGlobalLine.gatedLineModel_initial_mean_le line 117
  14. theorem OAI.Balanced.CandidateGlobalLine.gatedLineModel_centered_moment_le line 128
  15. def OAI.Balanced.CandidateGlobalLine.globalLineMomentConstant line 152
  16. theorem OAI.Balanced.CandidateGlobalLine.globalLineMomentConstant_nonneg line 156
  17. theorem OAI.Balanced.CandidateGlobalLine.gatedLineModel_centered_moment_bound line 160