OAI/Computability/MatchingCount/ScaledBounds.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BinaryMatching.Algorithm.int_two_abs line 10
  2. lemma OAI.BinaryMatching.Algorithm.beta_abs_nat line 12
  3. lemma OAI.BinaryMatching.Algorithm.indexed_slope_abs line 18
  4. lemma OAI.BinaryMatching.Algorithm.pieceNumerator_abs line 27
  5. lemma OAI.BinaryMatching.Algorithm.integralRow_mem line 42
  6. lemma OAI.BinaryMatching.Algorithm.integral_row_coeff line 48
  7. lemma OAI.BinaryMatching.Algorithm.integral_row_constant line 57
  8. lemma OAI.BinaryMatching.Algorithm.rowNumerator_abs line 63
  9. lemma OAI.BinaryMatching.Algorithm.scaledPsi_abs line 77
  10. lemma OAI.BinaryMatching.Algorithm.scaledSlope_abs line 81
  11. def OAI.BinaryMatching.Algorithm.operandBound line 84
  12. lemma OAI.BinaryMatching.Algorithm.integralValue_abs line 87
  13. lemma OAI.BinaryMatching.Algorithm.integralGradient_abs line 116
  14. lemma OAI.BinaryMatching.Algorithm.integralIterate_abs line 128
  15. lemma OAI.BinaryMatching.Algorithm.integralBest_abs line 136
  16. lemma OAI.BinaryMatching.Algorithm.operandBound_polynomial line 157