OAI/Probability/CriticalZ3/AdaptiveReveals.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.AdaptiveReveals.Scheme line 16
2. def OAI.AdaptiveReveals.Scheme.weight line 28
3. def OAI.AdaptiveReveals.Scheme.badMass line 32
4. theorem OAI.AdaptiveReveals.Scheme.weight_nonneg line 36
5. theorem OAI.AdaptiveReveals.Scheme.weight_sum line 39
6. def OAI.AdaptiveReveals.Scheme.hit line 45

   Source documentation

   Every target must first be tested by the time limit, and its first test must have declared it bad. Removing it prevents multiple visits from ever being counted as distinct successes in this estimate.

   noncomputable def hit : ℕ → S → Finset V → Set (E → Bool)
     | 0, _, U => if U = ∅ then Set.univ else ∅
     | n+1, s, U => match P.vertex s with
       | none => if U = ∅ then Set.univ else ∅
       | some v => {ω | (v ∈ U → P.bad s ((P.reveal s).restrict ω) = true) ∧
           ω ∈ hit n (P.child s ((P.reveal s).restrict ω)) (U.erase v)}

7. theorem OAI.AdaptiveReveals.Scheme.measurableSet_hit line 52
8. theorem OAI.AdaptiveReveals.Scheme.hit_empty line 69
9. theorem OAI.AdaptiveReveals.Scheme.hit_bound line 78

   Source documentation

   The only probabilistic hypotheses are the local bad probability and the exact next-history product law. Invalid zero-mass histories need no promise.

   theorem hit_bound (I : S → Prop) (f : ℝ) (hf : 0 ≤ f)
       (hbad : ∀ s, I s → P.badMass s ≤ f)
       (hchild : ∀ s, I s → ∀ a, 0 < P.weight s a → I (P.child s a))
       (n : ℕ) (s : S) (hs : I s) (U : Finset V) :
       (ProductCylinder.law (P.parameter s)).real (P.hit n s U) ≤ f^U.card := by
   …

   Mentions: OAI.ProductCylinder.law

10. theorem OAI.AdaptiveReveals.Scheme.badMass_eq_probability line 138
11. theorem OAI.AdaptiveReveals.Scheme.hit_subset_succ line 154
12. theorem OAI.AdaptiveReveals.Scheme.hit_monotone line 170
13. theorem OAI.AdaptiveReveals.Scheme.everHit_bound line 174

    Source documentation

    Uniform control survives an unbounded possible processing time.

    theorem everHit_bound (I : S → Prop) (f : ℝ) (hf : 0 ≤ f)
        (hbad : ∀ s, I s → P.badMass s ≤ f)
        (hchild : ∀ s, I s → ∀ a, 0 < P.weight s a → I (P.child s a))
        (s : S) (hs : I s) (U : Finset V) :
        (ProductCylinder.law (P.parameter s)).real (⋃ n, P.hit n s U) ≤ f^U.card := by
    …

    Mentions: OAI.ProductCylinder.law

14. theorem OAI.InfiniteConditioning.fixedParameter_merge line 193
15. structure OAI.InfiniteConditioning.History line 200
16. def OAI.InfiniteConditioning.History.parameter line 205
17. def OAI.InfiniteConditioning.History.observe line 207
18. def OAI.InfiniteConditioning.History.freeze line 209
19. theorem OAI.InfiniteConditioning.History.parameter_observe line 212
20. theorem OAI.InfiniteConditioning.History.freeze_determined line 217
21. theorem OAI.InfiniteConditioning.History.observe_outcome line 230
22. theorem OAI.InfiniteConditioning.History.ae_freeze line 242
23. theorem OAI.InfiniteConditioning.History.probability_freeze line 247