MarkedTransactions.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Explicit success declarations satisfy the disjoint-query certificate bound. The support-sensitive version permits arbitrary behavior on zero-probability bit vectors, including deterministic Bernoulli coordinates.

def OAI.MatroidProphet.MarkedQueryProgram.erase line 19
Source documentation
Forget success declarations, retaining the exact adaptive query tree.
```
def erase : MarkedQueryProgram α → QueryProgram α
  | .stop => .stop
  | .query e no yes => .query e no.erase yes.erase
  | .finish _ rest => .finish rest.erase
```
Mentions: OAI.MatroidProphet.MarkedQueryProgram, OAI.MatroidProphet.QueryProgram
lemma OAI.MatroidProphet.MarkedQueryProgram.erase_fresh line 24
lemma OAI.MatroidProphet.MarkedQueryProgram.run_nonneg line 32
lemma OAI.MatroidProphet.MarkedQueryProgram.run_le_transactionBound line 40
lemma OAI.MatroidProphet.MarkedQueryProgram.run_le_certifying_run line 53

theorem OAI.MatroidProphet.MarkedQueryProgram.disjoint_query_certificates_support line 79

Source documentation

Source lem:transactions for actual selected successes, with full support sensitivity. The tree only needs the soundness law on positive-weight vectors.

theorem disjoint_query_certificates_support [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 : prog.Fresh 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

theorem OAI.MatroidProphet.MarkedQueryProgram.disjoint_query_certificates line 98

Source documentation

The usual everywhere-lawful special case.

theorem disjoint_query_certificates [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 : prog.Fresh univ)
    (sound : ∀ S, prog.SoundAt cert S ∅) :
    bitsExpectation q univ prog.run ≤ Real.log (1 / bitsFailure cert q univ ∅) :=
…

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