TableLaw.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Precommitted finite conditional-randomness tables

The secretary construction draws all conditional random choices before the random arrival permutation. A table indexed by every possible branch/prefix pair does this without concealing later randomness. Its law is the ordinary finite product measure Measure.pi κ. Evaluating the table after an independent prefix experiment has exactly the corresponding conditional law.

These lemmas concern only this sampling construction, not the source theorem's competitive guarantee. In particular an application must separately prove the prefix law and the concrete source conditional-kernel laws.

theorem OAI.MatroidProphet.Secretary.integral_precommittedTable line 32

Source documentation

All conditional samples can be drawn initially and independently. Evaluating one coordinate after an independent finite experiment has the prescribed law.

theorem integral_precommittedTable
    (κ : ι → Measure α) [∀ i, IsProbabilityMeasure (κ i)]
    (μ : Measure Ω) [IsFiniteMeasure μ] (index : Ω → ι) (f : ι → α → ℝ) :
    (∫ z : Ω × (ι → α), f (index z.1) (z.2 (index z.1))
      ∂μ.prod (Measure.pi κ)) =
      ∫ ω, ∫ r, f (index ω) r ∂κ (index ω) ∂μ := by
…

theorem OAI.MatroidProphet.Secretary.integral_precommittedTable_eq_sum line 47

Source documentation

The same identity with the independent experiment explicitly summed. It retains the complete table, including all coordinates unused in this run.

theorem integral_precommittedTable_eq_sum
    (κ : ι → Measure α) [∀ i, IsProbabilityMeasure (κ i)]
    (μ : Measure Ω) [IsFiniteMeasure μ] (index : Ω → ι) (f : ι → α → ℝ) :
    (∫ z : Ω × (ι → α), f (index z.1) (z.2 (index z.1))
      ∂μ.prod (Measure.pi κ)) =
      ∑ ω, μ.real {ω} * (∫ r, f (index ω) r ∂κ (index ω)) := by
…