CertificateAuxSeed.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Disjoint-query certificates with an independent auxiliary seed

The source lemma lem:transactions permits an arbitrary independent auxiliary seed. After fixing that seed the procedure is a fresh finite query tree. The product-bit expectation below is then averaged over the seed law. In particular the program may depend on the seed, but the Bernoulli parameters do not.

No integrability assumption on the count is needed: nonnegativity and the pointwise logarithmic budget prove its integrability. The measurable-count hypothesis expresses measurability of the seed-dependent procedure.

lemma OAI.MatroidProphet.QueryProgram.run_nonneg line 26
lemma OAI.MatroidProphet.QueryProgram.run_le_card_add line 43
Source documentation
With no empty certificate, each successful transaction consumes at least one new positive query. The extra unit allows a nonempty transaction already in progress. This bound is independent of the number of transaction boundaries.
```
lemma QueryProgram.run_le_card_add (cert : Finset α → Prop) [DecidablePred cert]
    (hempty : ¬ cert ∅) (prog : QueryProgram α) (S V I : Finset α)
    (fresh : prog.Fresh V) :
    prog.run cert S I ≤ (V.card : ℝ) + if I.Nonempty then 1 else 0 := by
…
```
Mentions: OAI.MatroidProphet.QueryProgram
lemma OAI.MatroidProphet.QueryProgram.run_le_card line 79

theorem OAI.MatroidProphet.disjoint_query_certificates_auxiliary line 87

Source documentation

Averaging the actual product-bit count over any independent auxiliary seed preserves the source logarithmic certificate budget. This also proves that the averaged random variable is integrable.

theorem disjoint_query_certificates_auxiliary [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 ∅)
    {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ]
    (prog : Ω → QueryProgram α) (fresh : ∀ ω, (prog ω).Fresh univ)
    (meas : ∀ S, Measurable (fun ω => (prog ω).run cert S ∅)) :
    Integrable (fun ω => bitsExpectation q univ
      (fun S => (prog ω).run cert S ∅)) μ ∧
    (∫ ω, bitsExpectation q univ (fun S => (prog ω).run cert S ∅) ∂μ) ≤
      Real.log (1 / bitsFailure cert q univ ∅) := by
…

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