MarkedAuxiliaryAE.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Almost-surely lawful auxiliary-seed transaction policies

The independent auxiliary seed may live in an arbitrary probability space. Freshness and certificate soundness are needed only almost surely in that seed, and soundness in the bit vector is needed only on positive-probability vectors. The iterated expectation expresses the independent product experiment; its integrability is proved, not assumed. No uniform bound on the sizes of the seed-indexed finite trees is needed.

theorem OAI.MatroidProphet.MarkedQueryProgram.disjoint_query_certificates_auxiliary_ae line 24

Source documentation

The source logarithmic budget for an arbitrary independent auxiliary seed, including null exceptional seeds and deterministic Bernoulli coordinates.

theorem disjoint_query_certificates_auxiliary_ae
    {α : Type*} [DecidableEq α] [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 : Ω → 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