OAI/Combinatorics/PerfectMatching/ObjectivePenalty.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BinaryMatching.Algorithm.foldl_max_le line 11
  2. lemma OAI.BinaryMatching.Algorithm.le_foldl_max line 18
  3. lemma OAI.BinaryMatching.Algorithm.mem_le_foldl_max line 23
  4. lemma OAI.BinaryMatching.Algorithm.record_log_le_B line 31
  5. lemma OAI.BinaryMatching.Algorithm.multiplicity_log_le_B line 34
  6. lemma OAI.BinaryMatching.Algorithm.B_le_L line 40
  7. lemma OAI.BinaryMatching.Algorithm.beta_bound line 47
  8. lemma OAI.BinaryMatching.Algorithm.piece_slope_bound line 54
  9. lemma OAI.BinaryMatching.Algorithm.piece_supergradient line 62
  10. lemma OAI.BinaryMatching.Algorithm.selectedPiece_supergradient line 71
  11. lemma OAI.BinaryMatching.Algorithm.psiReal_abs_sub line 78
  12. def OAI.BinaryMatching.Algorithm.objective line 93
  13. def OAI.BinaryMatching.Algorithm.penalized line 96
  14. lemma OAI.BinaryMatching.Algorithm.objective_lipschitz line 99
  15. lemma OAI.BinaryMatching.Algorithm.exact_penalty line 114
  16. lemma OAI.BinaryMatching.Algorithm.penalized_feasible line 133
  17. lemma OAI.BinaryMatching.Algorithm.trialValue_cast line 137
  18. lemma OAI.BinaryMatching.Algorithm.trialValue_correct line 142
  19. lemma OAI.BinaryMatching.Algorithm.gradient_supergradient line 149
  20. lemma OAI.BinaryMatching.Algorithm.gradient_bound line 175
  21. lemma OAI.BinaryMatching.Algorithm.gradient_square_bound line 192