TransactionLogResource.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The exact one-query resource identity

This is the displayed eq:log-resource with its conditional product law written as the explicit two-outcome Bernoulli expectation. The finite-tree execution proof justifies applying this identity at every predictably selected fresh query.

theorem OAI.MatroidProphet.transaction_log_resource line 19

Source documentation

The source's expected one-query decrement, exponential expression, and logarithmic bound, for the actual finite-product failure probabilities.

theorem transaction_log_resource
    {α : Type*} [DecidableEq α]
    (cert : Finset α → Prop) [DecidablePred cert] (hcert : Monotone cert)
    (q : α → ℝ) (hq0 : ∀ e, 0 ≤ q e) (hq1 : ∀ e, q e ≤ 1)
    (V I : Finset α) (e : α) (he : e ∈ V)
    (hp : 0 < bitsFailure cert q V ∅) :
    let p := bitsFailure cert q V ∅
…

Mentions: OAI.MatroidProphet.bitsFailure