OAI/Probability/GammaPassage/HighDensityOriented.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarFPP.badContourEvent line 12

   Also declared: OAI/Probability/FirstPassage/HighDensityOriented.lean:11 (same declaration text).

2. theorem OAI.PlanarFPP.no_infinite_path_subset_contours line 16

   Also declared: OAI/Probability/FirstPassage/HighDensityOriented.lean:15 (same declaration text).

3. theorem OAI.PlanarFPP.bad_contours_fixed_length line 28

   Also declared: OAI/Probability/FirstPassage/HighDensityOriented.lean:27 (same declaration text).

4. theorem OAI.PlanarFPP.no_infinite_path_probability line 53

   Also declared: OAI/Probability/FirstPassage/HighDensityOriented.lean:52 (same declaration text).

5. theorem OAI.PlanarFPP.high_density_oriented_paths line 70

   Also declared: OAI/Probability/FirstPassage/HighDensityOriented.lean:69 (same declaration text).

6. theorem OAI.PlanarFPP.high_density_oriented_paths_real_bound line 85

   Source documentation

   A threshold depending only on k, with real-valued probabilities.

   Also declared: OAI/Probability/FirstPassage/HighDensityOriented.lean:83 (same declaration text).

   theorem high_density_oriented_paths_real_bound (k : ℕ) (G : Vertex → Set Ω)
       (hG : ∀ v, MeasurableSet (G v)) (hi : SeparatedGoodIndependent P G k)
       (hb : ∀ v, P.real (G v)ᶜ ≤ (1/1024 : ℝ)^(8*(2*k+1)^2)) :
       0 < P.real {ω | infiniteOrientedPath (fun v => ω ∈ G v) 0} := by
   …

   Mentions: OAI.PlanarFPP.Vertex, OAI.PlanarFPP.SeparatedGoodIndependent, OAI.PlanarFPP.infiniteOrientedPath

7. theorem OAI.PlanarFPP.high_density_oriented_paths_real line 99

   Source documentation

   Source cr:oriented-paths on an arbitrary probability space.

   Also declared: OAI/Probability/FirstPassage/HighDensityOriented.lean:96 (same declaration text).

   theorem high_density_oriented_paths_real (k : ℕ) :
       ∃ ζ : ℝ, 0 < ζ ∧ ∀ G : Vertex → Set Ω,
         (∀ v, MeasurableSet (G v)) → SeparatedGoodIndependent P G k →
         (∀ v, P.real (G v)ᶜ ≤ ζ) →
         0 < P.real {ω | infiniteOrientedPath (fun v => ω ∈ G v) 0} :=
   …

   Mentions: OAI.PlanarFPP.Vertex, OAI.PlanarFPP.SeparatedGoodIndependent, OAI.PlanarFPP.infiniteOrientedPath

8. theorem OAI.PlanarFPP.high_density_oriented_paths_uniform line 109

   Source documentation

   The same positive threshold works for every probability space and field; the existential is outside both quantifiers, exactly as in the source.

   Also declared: OAI/Probability/FirstPassage/HighDensityOriented.lean:104 (same declaration text).

   theorem high_density_oriented_paths_uniform (k : ℕ) :
       ∃ ζ : ℝ, 0 < ζ ∧ ∀ (Ω' : Type*) [MeasurableSpace Ω']
         (P' : Measure Ω') [IsProbabilityMeasure P'] (G : Vertex → Set Ω'),
         (∀ v, MeasurableSet (G v)) → SeparatedGoodIndependent P' G k →
         (∀ v, P'.real (G v)ᶜ ≤ ζ) →
         0 < P'.real {ω | infiniteOrientedPath (fun v => ω ∈ G v) 0} := by
   …

   Mentions: OAI.PlanarFPP.Vertex, OAI.PlanarFPP.SeparatedGoodIndependent, OAI.PlanarFPP.infiniteOrientedPath