Contracts.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Source-facing accounting lemmas. In particular, the thinning assertion is proved on each fixed outside-test fiber, not only after averaging those bits.

theorem OAI.MatroidProphet.AccountingContracts.thinning_final_fixed_outside line 15

Source documentation

Fixing all test memberships outside the focal group leaves its Bernoulli rank lower bound intact. This is the finite conditional law in lem:all-orders.

theorem thinning_final_fixed_outside
    (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
…

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

theorem OAI.MatroidProphet.AccountingContracts.nominal_rank_le_final_add_cost line 62

Source documentation

The manuscript's real-valued one-budget rank loss, before test thinning. The bound is valid for the entire finite parity window, including empty layers.

theorem nominal_rank_le_final_add_cost
    (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 ε : ℝ) ≤
      (finalRankStatistic M hE κ D C T h (h+1+later) U O Set.univ ε : ℝ) +
      (C h).ncard + ∑ j ∈ range later,
        ((C (h+1+j)).ncard + (D (h+1+j)).ncard / (κ : ℝ)) := by
…

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

theorem OAI.MatroidProphet.AccountingContracts.all_orders line 97

Source documentation

Both source clauses of the order-uniform rank bound: deterministic domination for every order, and test thinning on every fixed outside-group fiber.

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.AccountingContracts.rank_cost line 124

Source documentation

The source telescoping rank-cost assertion for an actual listed group. All later expansions use one cost over the whole auxiliary path.

theorem 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 : ℝ) ≤
      (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 univ h)
        ((d.H ∪ d.D ∪ d.C : Finset (Fin n)) : Set (Fin n)) Set.univ
        (boolParity d.odd) : ℝ) + (groupMask M d w d.C h).ncard +
      ∑ j ∈ 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) := by
…

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