OAI/Combinatorics/EditApproximation/Refinement/PhysicalInputGuard.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.physicalLargeInputWithWork_value line 14

   Source documentation

   Prefix rejection precedes arithmetic involving the accuracy word.

    theorem physicalLargeInputWithWork_value (N : ℕ) (epsilon : BinaryFraction) :
       (physicalLargeInputWithWork N epsilon).1 = decide (physicalLargeInput N epsilon) := by
   …

   Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.physicalLargeInputWithWork, OAI.EditApproximation.physicalLargeInput

2. theorem OAI.EditApproximation.physicalLargeInputWithWork_cost line 39