OAI/Probability/MatroidSecretary/Residual/ExitContract.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatroidProphet.ExitContract.reverseCost_nonneg line 11
2. lemma OAI.MatroidProphet.ExitContract.transition_cost_le_total line 21
3. lemma OAI.MatroidProphet.ExitContract.exists_exit_transition line 38

   Source documentation

   A finite run starting live and ending absent contains an actual exit step.

   lemma exists_exit_transition (M : Matroid α) (hE : M.E = Set.univ)
       (κ : ℕ) (D : ℕ → Set α) (G : ℕ → Finset α) (n : ℕ)
       (m : ℕ) (k : ℤ) (S : ℕ → Set α) (C : Finset α) (d : α) (h : ℕ)
       (hin : d ∈ S h)
       (hout : d ∉ reverseFinal M hE κ D G n m k S C h) :
       ∃ t ∈ reverseTrace M hE κ D G n m k S C, d ∈ t.before h ∧ d ∉ t.after h := by
   …

   Mentions: OAI.MatroidProphet.reverseFinal, OAI.MatroidProphet.reverseTrace

4. theorem OAI.MatroidProphet.ExitContract.nonloop_exits line 54

   Source documentation

   Every nonloop has an actual exit, for every realization of the original mask.

   theorem nonloop_exits (M : Matroid α) (hE : M.E = Set.univ)
       (κ : ℕ) (D : ℕ → Set α) (G : ℕ → Finset α)
       (hG : Pairwise (fun i j => Disjoint (G i) (G j)))
       (d : α) (hd : d ∉ M.closure ∅) (h : ℕ) (C : Finset α) :
       ∃ t ∈ reverseTrace M hE κ D G h (pathHorizon h + 1) (-1)
           (fun _ => Set.univ) C, d ∈ t.before h ∧ d ∉ t.after h := by
   …

   Mentions: OAI.MatroidProphet.reverseTrace, OAI.MatroidProphet.pathHorizon

5. theorem OAI.MatroidProphet.ExitContract.low_exit_event_lt_half line 66

   Source documentation

   Probability of an actual low-hazard exit in a finite reverse run.

   theorem low_exit_event_lt_half (M : Matroid α) (hE : M.E = Set.univ)
       (κ : ℕ) (D : ℕ → Set α) (G : ℕ → Finset α) (n : ℕ)
       (hG : Pairwise (fun i j => Disjoint (G i) (G j))) (q : α → ℝ)
       (hq0 : ∀ e, 0 ≤ q e) (hq1 : ∀ e, q e ≤ 1)
       (d : α) (h : ℕ) (hh : h ≤ n)
       (m : ℕ) (k : ℤ) (S : ℕ → Set α) (closed : ReverseClosed M hE κ D k S) :
       bitsExpectation q univ (fun C =>
         if ∃ t ∈ reverseTrace M hE κ D G n m k S C,
           d ∈ t.before h ∧ d ∉ t.after h ∧
             reverseHazard M hE κ D G q d h t.time t.before < exitThreshold
         then (1 : ℝ) else 0) < 1 / 2 := by
   …

   Mentions: OAI.MatroidProphet.ReverseClosed, OAI.MatroidProphet.bitsExpectation, OAI.MatroidProphet.reverseTrace, OAI.MatroidProphet.reverseHazard, OAI.MatroidProphet.exitThreshold

6. theorem OAI.MatroidProphet.ExitContract.exit_mass line 110

   Source documentation

   All three conclusions of manuscript lem:exit, on actual nominal paths. The natural reverse index i denotes manuscript time b = -i; its range is precisely activation h ≤ b ≤ 0.

   theorem exit_mass (M : Matroid α) (hE : M.E = Set.univ)
       (κ : ℕ) (D : ℕ → Set α) (G : ℕ → Finset α)
       (hG : Pairwise (fun i j => Disjoint (G i) (G j))) (q : α → ℝ)
       (hq0 : ∀ e, 0 ≤ q e) (hq1 : ∀ e, q e ≤ 1)
       (d : α) (hd : d ∉ M.closure ∅) (h : ℕ) :
       (∀ C : Finset α,
         d ∉ reverseFinal M hE κ D G h (pathHorizon h + 1) (-1)
           (fun _ => Set.univ) C h) ∧
       bitsExpectation q univ (fun C =>
         if ∃ t ∈ reverseTrace M hE κ D G h (pathHorizon h + 1) (-1)
             (fun _ => Set.univ) C,
           d ∈ t.before h ∧ d ∉ t.after h ∧
   …

   Mentions: OAI.MatroidProphet.reverseFinal, OAI.MatroidProphet.pathHorizon, OAI.MatroidProphet.bitsExpectation, OAI.MatroidProphet.reverseTrace

7. theorem OAI.MatroidProphet.ExitContract.exit_mass_actual line 140

   Source documentation

   Source-facing form with existence of the actual exit transition explicit. The final absence clause in exit_mass is strengthened to a witness in the single-mask reverse trace; the probability and square-sum clauses are unchanged.

   theorem exit_mass_actual (M : Matroid α) (hE : M.E = Set.univ)
       (κ : ℕ) (D : ℕ → Set α) (G : ℕ → Finset α)
       (hG : Pairwise (fun i j => Disjoint (G i) (G j))) (q : α → ℝ)
       (hq0 : ∀ e, 0 ≤ q e) (hq1 : ∀ e, q e ≤ 1)
       (d : α) (hd : d ∉ M.closure ∅) (h : ℕ) :
       (∀ C : Finset α,
         ∃ t ∈ reverseTrace M hE κ D G h (pathHorizon h + 1) (-1)
             (fun _ => Set.univ) C, d ∈ t.before h ∧ d ∉ t.after h) ∧
       bitsExpectation q univ (fun C =>
         if ∃ t ∈ reverseTrace M hE κ D G h (pathHorizon h + 1) (-1)
             (fun _ => Set.univ) C,
           d ∈ t.before h ∧ d ∉ t.after h ∧
   …

   Mentions: OAI.MatroidProphet.reverseTrace, OAI.MatroidProphet.pathHorizon, OAI.MatroidProphet.bitsExpectation