MaskLawAbe.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The source sacrificed-mask law for the secretary transport

The identities below concern the actual complete source seed. They average over the branch coin and all mask coordinates, including unused coordinates. They do not assert a product law conditional on the complete secretary seed.

lemma OAI.MatroidProphet.secretary_main_rate line 17
lemma OAI.MatroidProphet.secretary_main_rate_pos line 22
lemma OAI.MatroidProphet.secretary_main_rate_lt_one line 25

theorem OAI.MatroidProphet.main_sacrificed_mask_expectation line 30

Source documentation

The union of the three sacrificed main-branch masks has precisely the Bernoulli rate stated in the manuscript. The test mask is not sacrificed.

theorem main_sacrificed_mask_expectation {α : Type*} [DecidableEq α]
    (V : Finset α) (f : Finset α → ℝ) :
    bitsExpectation (fun _ => (1 / 2 : ℝ)) V (fun H =>
      bitsExpectation (fun _ => (1 / 4 : ℝ)) V (fun D =>
        bitsExpectation (fun _ => thinningRate) V (fun C => f (H ∪ D ∪ C)))) =
      bitsExpectation (fun _ => (5 / 8 : ℝ) + 3 * ((2 : ℝ) ^ 143)⁻¹) V f := by
…

Mentions: OAI.MatroidProphet.bitsExpectation, OAI.MatroidProphet.thinningRate

lemma OAI.MatroidProphet.completeHiddenRule_mask line 44
Source documentation
The sacrificed mask of the implemented hidden rule, with its branch tag.
```
lemma completeHiddenRule_mask {n : ℕ} (M : Matroid (Fin n))
    (hE : M.E = Set.univ) (r : Seed (mainSeedBits n)) :
    (completeHiddenRule M hE).mask r =
      if mainBranch r then (mainMasks r).H ∪ (mainMasks r).D ∪ (mainMasks r).C
      else (mainMasks r).H := by
…
```
Mentions: OAI.MatroidProphet.Seed, OAI.MatroidProphet.mainSeedBits, OAI.MatroidProphet.completeHiddenRule, OAI.MatroidProphet.mainBranch, OAI.MatroidProphet.mainMasks

theorem OAI.MatroidProphet.source_sacrificed_mask_expectation line 53

Source documentation

Exact joint law of the branch and sacrificed mask. Arbitrary real test functions characterize the full finite joint law, not just its marginals.

theorem source_sacrificed_mask_expectation {n : ℕ} (M : Matroid (Fin n))
    (hE : M.E = Set.univ) (f : Bool → Finset (Fin n) → ℝ) :
    (∫ r, f (mainBranch r) ((completeHiddenRule M hE).mask r) ∂sourceSeedLaw n) =
      (1 / 2 : ℝ) *
        bitsExpectation (fun _ => (1 / 2 : ℝ)) Finset.univ (f false) +
      (1 / 2 : ℝ) *
        bitsExpectation (fun _ => (5 / 8 : ℝ) + 3 * ((2 : ℝ) ^ 143)⁻¹)
          Finset.univ (f true) := by
…

Mentions: OAI.MatroidProphet.mainBranch, OAI.MatroidProphet.completeHiddenRule, OAI.MatroidProphet.sourceSeedLaw, OAI.MatroidProphet.bitsExpectation