OAI/Combinatorics/ContingencyTables/Sampling/PhysicalEventBounds.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.PhysicalEventBounds.event line 14
2. lemma OAI.ContingencyTables.PhysicalEventBounds.event_nonneg line 16
3. lemma OAI.ContingencyTables.PhysicalEventBounds.event_le_one line 18
4. lemma OAI.ContingencyTables.PhysicalEventBounds.mean_mono line 21
5. lemma OAI.ContingencyTables.PhysicalEventBounds.average_mono line 28
6. theorem OAI.ContingencyTables.PhysicalEventBounds.stopped_event_bounds line 34

   Source documentation

   Only successful endpoints need be halted; the failure endpoint can be live.

   theorem stopped_event_bounds (M : PhysicalPost.Table Γ Q) (out : Option A → Cfg Γ Q)
       (c : Cfg Γ Q) (p : Experiment (Option A)) (hp : Implements M out c p)
       (hhalt : ∀ a,(out (some a)).state=none) (P : Cfg Γ Q → Prop)
       (n : ℕ) (hn : p.cost≤n) :
       p.mean (fun o => o.elim 0 (fun a => event P (out (some a))))≤
           (experiment M n c).mean (event P) ∧
         (experiment M n c).mean (event P)≤
           p.mean (fun o => o.elim 0 (fun a => event P (out (some a))))+
             p.mean (fun o => if o=none then 1 else 0) := by
   …

   Mentions: OAI.ContingencyTables.PhysicalEventBounds.event

7. lemma OAI.ContingencyTables.PhysicalEventBounds.terminal_event_monotone line 70
8. theorem OAI.ContingencyTables.PhysicalEventBounds.absent_event_bound line 87

   Source documentation

   A terminal event absent at every successful endpoint is bounded by prefix failure even at times earlier than the stopping-prefix budget.

   theorem absent_event_bound (M : PhysicalPost.Table Γ Q) (out : Option A → Cfg Γ Q)
       (c : Cfg Γ Q) (p : Experiment (Option A)) (hp : Implements M out c p)
       (hhalt : ∀ a,(out (some a)).state=none) (P : Cfg Γ Q → Prop)
       (hP : ∀ d,P d → d.state=none) (habsent : ∀ a,¬P (out (some a))) (n : ℕ) :
       (experiment M n c).mean (event P)≤p.mean (fun o => if o=none then 1 else 0) := by
   …

   Mentions: OAI.ContingencyTables.PhysicalEventBounds.event

9. lemma OAI.ContingencyTables.PhysicalEventBounds.tendsto_of_prefix_bounds line 105

   Source documentation

   Prefix accuracy transfers to physical time without assuming a uniform bound on the number of steps in the prefix.

   lemma tendsto_of_prefix_bounds (f a b : ℕ → ℝ) (L : ℝ)
       (ha : Filter.Tendsto a Filter.atTop (nhds L))
       (hb : Filter.Tendsto b Filter.atTop (nhds 0))
       (h : ∀ N,∃ S,∀ t,S≤t → a N≤f t ∧ f t≤a N+b N) :
       Filter.Tendsto f Filter.atTop (nhds L) := by
   …

10. lemma OAI.ContingencyTables.PhysicalEventBounds.mean_one_sub line 125
11. lemma OAI.ContingencyTables.PhysicalEventBounds.run_halted_iff line 132