FixedOutsideThinning.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Source accounting contracts

The finite-fiber expectation below expresses conditioning on all test coordinates outside the focal group. In contrast to an expectation over the entire test mask, it retains the conditional quantifier in lem:all-orders (accounting.tex).

theorem OAI.MatroidProphet.fixed_outside_thinning_rank line 21

Source documentation

Fix every test bit outside G, and average only the fresh bits inside G. The contracted base may depend arbitrarily on the fixed outside mask.

theorem fixed_outside_thinning_rank
    (M : Matroid α) (hE : M.E = Set.univ) (t : ℝ) (ht0 : 0 ≤ t) (ht1 : t ≤ 1)
    (G A : Finset α) (hAG : Disjoint A G) (S : Set α) (hS : S ⊆ (G : Set α))
    (P : Finset α → Set α)
    (hP : ∀ B : Finset α, B ⊆ G → P (A ∪ B) = P A) :
    t * (conditionalRank M S (P A) : ℝ) ≤
      bitsExpectation (fun _ => t) G
        (fun B => (conditionalRank M (S ∩ ((A ∪ B : Finset α) : Set α))
          (P (A ∪ B)) : ℝ)) := by
…

Mentions: OAI.MatroidProphet.conditionalRank, OAI.MatroidProphet.bitsExpectation

theorem OAI.MatroidProphet.fixed_outside_finalRankStatistic line 49

Source documentation

The source's test-thinning inequality conditional on the complete outside configuration, not on an arrival order and not merely after averaging it away.

theorem fixed_outside_finalRankStatistic
    (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 α)) h final
        (G h) O ((A ∪ B : Finset α) : Set α) ε : ℝ)) := by
…

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