OAI/Combinatorics/EditApproximation/Probability/RejectionSelectedLaw.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The independent failure-count/accepted-value representation is exactly the law of the literal rejection executions, including discarded trials.

  1. def OAI.EditApproximation.rejectionRuntimeToExecution line 16
  2. def OAI.EditApproximation.rejectionExecutionToRuntime line 19
  3. theorem OAI.EditApproximation.rejectionRuntimeToExecution_law line 22
  4. theorem OAI.EditApproximation.rejectionRuntime_roundtrip line 54
  5. theorem OAI.EditApproximation.rejectionExecution_roundtrip line 58
  6. theorem OAI.EditApproximation.rejectionRequestedBits_expected_le line 66

    Source documentation

    Only distinct requested coordinates are sampled. The bound includes all failed rejection trials, even when the query depends on accepted values.

     theorem rejectionRequestedBits_expected_le [DecidableEq ι]
    (program : FiniteQuery ι) (budget : ℕ)
    (hbudget : ∀ accepted : ∀ i, Fin (range i),
      program.cost (fun i => (accepted i).val) (fun i => rejectionBitCount (range i)) ≤ budget) :
    (∫ execution, rejectionSelectedBits range
        (fun i accepted => i ∈ program.keys (fun j => (accepted j).val)) execution
      ∂rejectionRuntimeArrayLaw range) ≤ 2 * (budget : ℝ) := by
…

    Mentions: OAI.EditApproximation.FiniteQuery, OAI.EditApproximation.rejectionBitCount, OAI.EditApproximation.rejectionSelectedBits, OAI.EditApproximation.rejectionRuntimeArrayLaw