Independent.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Source-exact accounting contracts

The conditioning in lem:all-orders fixes every test bit outside the focal listed group. Averaging only the remaining group's bits is stronger than merely averaging all test bits. We make that finite conditional expectation explicit below, without conditioning on any arrival order.

theorem OAI.MatroidProphet.AccountingIndependent.thinning_finalRankStatistic_conditioned line 24

Source documentation

The manuscript's test-thinning inequality for each fixed outside-mask realization. A is exactly the fixed positive test set outside G h; only B ⊆ G h is averaged. In particular, no selected arrival order is conditioned on, and the competition set may depend on all outside bits.

theorem thinning_finalRankStatistic_conditioned
    (M : Matroid α) (hE : M.E = Set.univ)
    (κ : ℕ) (D C : ℕ → Set α) (G : ℕ → Finset α)
    (hG : Pairwise (fun i j => Disjoint (G i) (G j)))
    (h final : ℕ) (O : Set α) (ε : Fin 2) (t : ℝ)
    (ht0 : 0 ≤ t) (ht1 : t ≤ 1)
    (A : Finset α) (hA : Disjoint A (G h)) :
    t * (finalRankStatistic M hE κ D C
      (fun j => (A : Set α) ∩ (G j : Set α)) h final (G h) O Set.univ ε : ℝ) ≤
    bitsExpectation (fun _ : α => t) (G h) (fun B =>
      (finalRankStatistic M hE κ D C
        (fun j => ((A ∪ B : Finset α) : Set α) ∩ (G j : Set α))
…

Mentions: OAI.MatroidProphet.finalRankStatistic, OAI.MatroidProphet.bitsExpectation

theorem OAI.MatroidProphet.AccountingIndependent.rank_cost_real line 74

Source documentation

The unscaled real-valued form of lem:rank-cost. There is a single sum of later-group costs for the entire parity timeline, not one cost per layer. The density contribution is real division, never truncated division.

theorem rank_cost_real
    (M : Matroid α) (hE : M.E = Set.univ)
    (κ : ℕ) (hκ : 0 < κ) (D C T : ℕ → Set α) (h later : ℕ)
    (U O : Set α) (ε : Fin 2) :
    (nominalRankStatistic M hE κ D C T h U O ε : ℝ) -
      ((C h).ncard + ∑ j ∈ Finset.range later,
        ((C (h+1+j)).ncard + (D (h+1+j)).ncard / (κ : ℝ))) ≤
    (finalRankStatistic M hE κ D C T h (h+1+later) U O Set.univ ε : ℝ) := by
…

Mentions: OAI.MatroidProphet.nominalRankStatistic, OAI.MatroidProphet.finalRankStatistic

theorem OAI.MatroidProphet.AccountingIndependent.all_orders line 111

Source documentation

Both assertions of source lem:all-orders, instantiated to the actual listed groups. The second assertion is the finite conditional law obtained by fixing all of H,D,C, parity, and every test bit outside the listed group.

theorem all_orders {n : ℕ} (M : Matroid (Fin n)) (hE : M.E = Set.univ)
    (d : MainMasks n) (w : Fin n → Option ℤ) (h : ℕ) :
    (∀ π : ArrivalOrder n, listedLambda M hE d w h ≤
      ((selection M hE d w π).filter (fun e =>
        ∃ i, w e = some i ∧ h ≤ (groups M d w).idxOf i)).card) ∧
    (∀ A : Finset (Fin n), Disjoint A (pathGroups M d w h) →
      thinningRate * (finalRankStatistic M hE (2^100)
        (groupMask M d w d.D) (groupMask M d w d.C)
        (fun j => (A : Set (Fin n)) ∩ (pathGroups M d w j : Set (Fin n)))
        h (groups M d w).length (pathGroups M d w h)
        ((d.H ∪ d.D ∪ d.C : Finset (Fin n)) : Set (Fin n)) Set.univ
        (boolParity d.odd) : ℝ) ≤
…

Mentions: OAI.MatroidProphet.MainMasks, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.thinningRate, OAI.MatroidProphet.finalRankStatistic, OAI.MatroidProphet.boolParity

theorem OAI.MatroidProphet.AccountingIndependent.listed_rank_cost line 139

Source documentation

Source lem:rank-cost for the concrete listed group and final guarded path, with the displayed real-valued cost and without any probabilistic or independence assumption on its common generators.

theorem listed_rank_cost {n : ℕ} (M : Matroid (Fin n)) (hE : M.E = Set.univ)
    (d : MainMasks n) (w : Fin n → Option ℤ) (h : ℕ)
    (hh : h < (groups M d w).length) :
    (listedZ M hE d w h : ℝ) -
      ((groupMask M d w d.C h).ncard +
        ∑ j ∈ Finset.range ((groups M d w).length - (h+1)),
          ((groupMask M d w d.C (h+1+j)).ncard +
            (groupMask M d w d.D (h+1+j)).ncard / densityThreshold)) ≤
    (finalRankStatistic M hE (2^100)
      (groupMask M d w d.D) (groupMask M d w d.C) (groupMask M d w d.T)
      h (groups M d w).length (groupMask M d w Finset.univ h)
      ((d.H ∪ d.D ∪ d.C : Finset (Fin n)) : Set (Fin n)) Set.univ
…

Mentions: OAI.MatroidProphet.MainMasks, OAI.MatroidProphet.densityThreshold, OAI.MatroidProphet.finalRankStatistic