OAI/Combinatorics/EditApproximation/Binary/BitQuery.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Adaptive queries whose answers are stored binary fractions. Local Boolean computations appear as explicit charged steps. The simulation relation below preserves the ordered requests as well as the final value; it does not gather a rational query's keys in advance.

  1. def OAI.EditApproximation.BitQuery.keys line 21
  2. theorem OAI.EditApproximation.BitQuery.value_bind line 30
  3. theorem OAI.EditApproximation.BitQuery.keys_bind line 38
  4. theorem OAI.EditApproximation.BitQuery.work_bind line 46
  5. inductive OAI.EditApproximation.BitQuery.Refines line 60

    Source documentation

    Branches of the reference query are selected only by the values of answers actually read. The relation can therefore be composed stage by stage.

    inductive Refines {ι β : Type*} (relation : β → ℚ → Prop) :
    BitQuery ι β → FiniteQuery ι → Prop where
…

    Mentions: OAI.EditApproximation.BitQuery, OAI.EditApproximation.FiniteQuery

  6. theorem OAI.EditApproximation.BitQuery.Refines.value_keys line 70
  7. theorem OAI.EditApproximation.BitQuery.Refines.read_work_le line 81
  8. theorem OAI.EditApproximation.BitQuery.Refines.bind line 90
  9. theorem OAI.EditApproximation.BitQuery.Refines.collect line 102
  10. theorem OAI.EditApproximation.BitQuery.value_collect line 121
  11. theorem OAI.EditApproximation.BitQuery.work_collect line 130