OAI/Combinatorics/MatchingCount/Graphs/RowPeak.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MatchingFPRAS.RealStage.scalingTrace_invariant line 13
  2. theorem OAI.MatchingFPRAS.RealStage.one_pass_scaling line 51
  3. def OAI.MatchingFPRAS.RealStage.rowPeak line 72
  4. def OAI.MatchingFPRAS.RealStage.scaledHoleMatrix line 75
  5. def OAI.MatchingFPRAS.RealStage.BalancedRows line 78
  6. theorem OAI.MatchingFPRAS.RealStage.one_pass_restores_balance line 84
  7. def OAI.MatchingFPRAS.RealStage.sigma line 127
  8. def OAI.MatchingFPRAS.RealStage.ratioEstimate line 129
  9. def OAI.MatchingFPRAS.RealStage.upperEstimate line 131
  10. lemma OAI.MatchingFPRAS.RealStage.sigma_nonneg line 136
  11. lemma OAI.MatchingFPRAS.RealStage.sigma_small line 139
  12. lemma OAI.MatchingFPRAS.RealStage.sigma_times_D line 146
  13. lemma OAI.MatchingFPRAS.RealStage.sigma_relative line 153
  14. lemma OAI.MatchingFPRAS.RealStage.ratio_error line 159
  15. lemma OAI.MatchingFPRAS.RealStage.upper_error line 192
  16. theorem OAI.MatchingFPRAS.RealStage.successful_stage_estimates line 245
  17. def OAI.MatchingFPRAS.Enlargement.pairEdge line 280
  18. lemma OAI.MatchingFPRAS.Enlargement.pairEdge_swap line 284
  19. lemma OAI.MatchingFPRAS.Enlargement.pairEdge_holes line 289
  20. def OAI.MatchingFPRAS.Enlargement.probeMatrix line 295
  21. lemma OAI.MatchingFPRAS.Enlargement.probeMatrix_off line 299
  22. lemma OAI.MatchingFPRAS.Enlargement.probeMatrix_symm line 303
  23. def OAI.MatchingFPRAS.Enlargement.estimateMatrix line 308
  24. lemma OAI.MatchingFPRAS.Enlargement.estimateMatrix_symm line 312
  25. lemma OAI.MatchingFPRAS.Enlargement.rowMax_cooling_lower line 316
  26. def OAI.MatchingFPRAS.Enlargement.meanA line 333
  27. def OAI.MatchingFPRAS.Enlargement.meanD line 336
  28. def OAI.MatchingFPRAS.Enlargement.meanProbe line 339
  29. lemma OAI.MatchingFPRAS.Enlargement.rowPeak_holeMatrix line 349
  30. structure OAI.MatchingFPRAS.Enlargement.StageData line 353
  31. structure OAI.MatchingFPRAS.Enlargement.EmpiricalData line 372
  32. lemma OAI.MatchingFPRAS.Enlargement.StageData.cooling line 381
  33. lemma OAI.MatchingFPRAS.Enlargement.StageData.mean_bounds line 387
  34. lemma OAI.MatchingFPRAS.Enlargement.StageData.hole_upper line 399
  35. theorem OAI.MatchingFPRAS.Enlargement.actual_stage_statistics line 406
  36. theorem OAI.MatchingFPRAS.Enlargement.actual_successful_stage line 430