RandomizedMarkedTransactions.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The complete disjoint-query certificate contract

This is the independent-auxiliary-seed form of lem:transactions, with explicit success declarations rather than counting every certifying transaction. The inner finite product expectation has the original Bernoulli law for every seed. Soundness is required only on bit vectors with positive product mass; this keeps deterministic Bernoulli coordinates within scope without restricting impossible executions. Integrability follows from the proved logarithmic budget.

lemma OAI.MatroidProphet.MarkedQueryProgram.run_le_card_of_positive_failure line 26

Source documentation

On every sound execution with positive failure probability, successes are bounded by the number of coordinates, even if the chosen finite tree contains arbitrarily many empty or unsuccessful transactions.

lemma run_le_card_of_positive_failure
    {α : Type*} [Fintype α] [DecidableEq α]
    (cert : Finset α → Prop) [DecidablePred cert] (hcert : Monotone cert)
    (q : α → ℝ) (hδ : 0 < bitsFailure cert q univ ∅)
    (prog : MarkedQueryProgram α) (fresh : prog.Fresh univ)
    (S : Finset α) (sound : prog.SoundAt cert S ∅) :
    prog.run S ≤ (Fintype.card α : ℝ) := by
…

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

theorem OAI.MatroidProphet.MarkedQueryProgram.disjoint_query_certificates_auxiliary line 44

Source documentation

Arbitrary independent auxiliary randomization preserves the certificate budget for explicitly declared, sound successes. The source's uniform finite transaction bound is not needed: each seed fixes a finite adaptive tree.

theorem disjoint_query_certificates_auxiliary
    {α : Type*} [Fintype α] [DecidableEq α]
    (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 ∅)
    {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ]
    (prog : Ω → MarkedQueryProgram α)
    (fresh : ∀ ω, (prog ω).Fresh univ)
    (sound : ∀ ω S, 0 < bitsWeight q univ S → (prog ω).SoundAt cert S ∅)
    (meas : ∀ S, Measurable (fun ω => (prog ω).run S)) :
    Integrable (fun ω => bitsExpectation q univ (prog ω).run) μ ∧
    (∫ ω, bitsExpectation q univ (prog ω).run ∂μ) ≤
…

Mentions: OAI.MatroidProphet.bitsFailure, OAI.MatroidProphet.MarkedQueryProgram, OAI.MatroidProphet.MarkedQueryProgram.Fresh, OAI.MatroidProphet.bitsWeight, OAI.MatroidProphet.MarkedQueryProgram.SoundAt, OAI.MatroidProphet.MarkedQueryProgram.run, OAI.MatroidProphet.bitsExpectation