OAI/Combinatorics/EditApproximation/Queries/QueryRestrictionCost.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EditApproximation.BitQuery.restrictedOracle line 8

   Source documentation

   A failed domain test supplies the same zero word to the adaptive continuation.

   def restrictedOracle {ι : Type*} (P : ι → Prop) (test : ι → Bool × ℕ)
       (htest : ∀ key, (test key).1 = true ↔ P key)
       (oracle : {key // P key} → BinaryFraction) (key : ι) : BinaryFraction :=
   …

   Mentions: OAI.EditApproximation.BinaryFraction

2. def OAI.EditApproximation.BitQuery.restrictedReadWork line 13
3. theorem OAI.EditApproximation.BitQuery.restrictWithWork_work line 18
4. theorem OAI.EditApproximation.BitQuery.restrictWithWork_value line 34
5. theorem OAI.EditApproximation.BitQuery.restrictedOracle_width line 47
6. theorem OAI.EditApproximation.queryPhysicalBoundedWithWork_cost line 61