OAI/Combinatorics/EditApproximation/Binary/BinaryFinalAnswer.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.BinaryFraction.finalAnswerWithWork_value line 15

   Source documentation

   Clamp the final value to the input length and round down by binary division.

   theorem finalAnswerWithWork_value (N : ℕ) (a : BinaryFraction) :
       bitWordValue (finalAnswerWithWork N a).1 = integerAnswer N (a.value : ℝ) := by
   …

   Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.bitWordValue, OAI.EditApproximation.BinaryFraction.finalAnswerWithWork, OAI.EditApproximation.integerAnswer

2. theorem OAI.EditApproximation.BinaryFraction.finalAnswerWithWork_cost line 39