OAI/Probability/MatroidSecretary/Pivots/SupportedTransactions.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Removing impossible invalid query branches

A no-repeat procedure need only satisfy that property along its possible transcripts. Truncating at an attempted repeated/unavailable query produces a globally fresh finite tree and does not change any lawful execution. Together with support-sensitive certificate soundness, this includes deterministic bit coordinates without imposing conditions on impossible transcripts.

  1. def OAI.MatroidProphet.MarkedQueryProgram.prune line 23

    Source documentation

    Stop at an attempted repeated or otherwise unavailable coordinate.

    def prune : MarkedQueryProgram α → Finset α → MarkedQueryProgram α
  | .stop, _ => .stop
  | .query e no yes, V => if e ∈ V then
      .query e (no.prune (V.erase e)) (yes.prune (V.erase e)) else .stop
  | .finish success rest, V => .finish success (rest.prune V)

    Mentions: OAI.MatroidProphet.MarkedQueryProgram

  2. lemma OAI.MatroidProphet.MarkedQueryProgram.prune_fresh line 29
  3. lemma OAI.MatroidProphet.MarkedQueryProgram.run_prune_eq line 40
  4. lemma OAI.MatroidProphet.MarkedQueryProgram.soundAt_prune line 56
  5. lemma OAI.MatroidProphet.MarkedQueryProgram.bitsExpectation_prune_eq line 73
  6. theorem OAI.MatroidProphet.MarkedQueryProgram.disjoint_query_certificates_supported line 90

    Source documentation

    The certificate budget requires no-repeat and soundness only on possible executions. No conditions are placed on zero-probability bit vectors.

    theorem disjoint_query_certificates_supported [Fintype α]
    (cert : Finset α → Prop) [DecidablePred cert] (hcert : Monotone cert)
    (q : α → ℝ) (hq0 : ∀ e, 0 ≤ q e) (hq1 : ∀ e, q e ≤ 1)
    (hδ : 0 < bitsFailure cert q univ ∅)
    (prog : MarkedQueryProgram α)
    (fresh : ∀ S, 0 < bitsWeight q univ S → prog.FreshAt S univ)
    (sound : ∀ S, 0 < bitsWeight q univ S → prog.SoundAt cert S ∅) :
    bitsExpectation q univ prog.run ≤ Real.log (1 / bitsFailure cert q univ ∅) := by
…

    Mentions: OAI.MatroidProphet.bitsFailure, OAI.MatroidProphet.MarkedQueryProgram, OAI.MatroidProphet.bitsWeight, OAI.MatroidProphet.bitsExpectation