OAI/Combinatorics/BalancedRyser/Results.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.prime_stability line 348
  2. theorem OAI.Balanced.selection line 350
  3. theorem OAI.Balanced.candidate_graph line 352
  4. theorem OAI.Balanced.deletion_domination line 354
  5. theorem OAI.Balanced.pencil_reuse line 357
  6. theorem OAI.Balanced.pencil_small_reuse line 359
  7. theorem OAI.Balanced.pencil_two_reuses line 362
  8. theorem OAI.Balanced.pattern_moments line 365
  9. theorem OAI.Balanced.deterministic_reduction line 367
  10. theorem OAI.Balanced.independent_trial_jumps line 370
  11. theorem OAI.Balanced.bounded_drift_concentration line 373
  12. theorem OAI.Balanced.affine_second_moment line 376
  13. theorem OAI.Balanced.tail_conditioning line 379
  14. theorem OAI.Balanced.profile_counting line 392
  15. theorem OAI.Balanced.robust_deletion line 394
  16. theorem OAI.Balanced.core_pencil line 397
  17. theorem OAI.Balanced.pencil_local line 400
  18. theorem OAI.Balanced.main_result line 402

    Distinct definitions of this name: ComparatorChallenges/BalancedRyser.lean:39 (same statement text; different proof or body). Qualify references as OAI.Balanced.main_result@path.