OAI/Probability/CriticalZ3/Extension.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MeasureTheory.finite_measureReal_mono_ae line 14
2. theorem OAI.CriticalZ3.LatticeGraph.entrant_exterior line 23
3. theorem OAI.CriticalZ3.LatticeGraph.entrant_node line 27
4. theorem OAI.CriticalZ3.LatticeGraph.fixed_large_entrants_failure line 31

   Source documentation

   Actual separated seed trials under an arbitrary fixed outside pattern.

   theorem fixed_large_entrants_failure (p : m.Bit → Set.Icc (0 : ℝ) 1)
       (q : Set.Icc (0 : ℝ) 1) (hq : 0 < (q : ℝ))
       (C : Box) (r K : ℕ) (hK : 0 < K)
       (hw : ∀ i, C.lower i+r ≤ C.upper i-r) (hC : G.ContainsBox (C.expand 1))
       (o : G.Node) (T : Set Vertex) (ξ : m.Config)
       (hp : ∀ e ∈ (C.expand 1).bits m, p e = q) {γ τ : ℝ} (hτ : 0 < τ)
       (hqual : ∀ y, C.Exterior y → (ProductCylinder.law p).real
         (allValue ((C.seedBox r y).bits m) true ∩
           {ω | conditionalProbability p (C.bits m)
             {ω | G.Meets m ω (G.relayNode C r hw (hC.mono G (fun _ => C.contains_expand 1)) y) T} ω ≤ 1-τ})
           ≤ (q : ℝ)^Box.seedCard m r*γ/τ)
       (hlarge : K*(8*r+5)^3 ≤ (G.entrants m C ξ o).card) :
   …

   Mentions: OAI.CriticalZ3.Box, OAI.CriticalZ3.Vertex, OAI.CriticalZ3.LatticeGraph.bits, OAI.ProductCylinder.law, OAI.CriticalZ3.Box.seedCard

5. theorem OAI.CriticalZ3.LatticeGraph.measurableSet_large_entrants line 106
6. theorem OAI.CriticalZ3.LatticeGraph.large_entrants_failure line 114

   Source documentation

   Integrating the exact separated-trial estimate, including histories with fewer than L entries.

   theorem large_entrants_failure (p : m.Bit → Set.Icc (0 : ℝ) 1)
       (q : Set.Icc (0 : ℝ) 1) (hq : 0 < (q : ℝ))
       (C : Box) (r K : ℕ) (hK : 0 < K)
       (hw : ∀ i, C.lower i+r ≤ C.upper i-r) (hC : G.ContainsBox (C.expand 1))
       (o : G.Node) (T : Set Vertex)
       (hp : ∀ e ∈ (C.expand 1).bits m, p e = q) {γ τ : ℝ} (hγ : 0 ≤ γ) (hτ : 0 < τ)
       (hqual : ∀ y, C.Exterior y → (ProductCylinder.law p).real
         (allValue ((C.seedBox r y).bits m) true ∩
           {ω | conditionalProbability p (C.bits m)
             {ω | G.Meets m ω (G.relayNode C r hw (hC.mono G (fun _ => C.contains_expand 1)) y) T} ω ≤ 1-τ})
           ≤ (q : ℝ)^Box.seedCard m r*γ/τ) :
       (ProductCylinder.law p).real
   …

   Mentions: OAI.CriticalZ3.Box, OAI.CriticalZ3.Vertex, OAI.CriticalZ3.LatticeGraph.bits, OAI.ProductCylinder.law, OAI.CriticalZ3.Box.seedCard

7. theorem OAI.CriticalZ3.Box.entryBit_internal_expand line 158
8. theorem OAI.CriticalZ3.LatticeGraph.extension_bound line 171

   Source documentation

   The shell + separated-seed + interior-quality extension, with all probability terms explicit. The input seed events are the exact cube-restricted events.

   theorem extension_bound (p : m.Bit → Set.Icc (0 : ℝ) 1)
       (q : Set.Icc (0 : ℝ) 1) (hq : 0 < (q : ℝ)) {p₀ : ℝ} (hqp : (q : ℝ) ≤ p₀) (hp₀ : p₀ < 1)
       (B : Box) (r K R : ℕ) (hK : 0 < K) (hrR : r < R)
       (hG : G.ContainsBox (B.expand R)) (o : G.Node) (T : Set Vertex)
       (ho : ¬(B.expand R).Contains o.1)
       (hp : ∀ e ∈ (B.expand R).bits m, p e = q)
       {γ τ : ℝ} (hγ : 0 ≤ γ) (hτ : 0 < τ)
       (hreach : ∀ c, (B.expand R).Contains c → ∃ ℓ : ℕ,
         r ≤ ℓ ∧ G.ContainsBox (Box.cube c ℓ) ∧
         1-γ ≤ (ProductCylinder.law p).real (m.SeedReaches c r ℓ T)) :
       (ProductCylinder.law p).real
         {ω | G.Meets m ω o {x | B.Contains x} ∧ ¬G.Meets m ω o T} ≤
   …

   Mentions: OAI.CriticalZ3.Box, OAI.CriticalZ3.Vertex, OAI.CriticalZ3.LatticeGraph.bits, OAI.CriticalZ3.Box.cube, OAI.ProductCylinder.law