OAI/Probability/SLE/Stochastic/BrownianGerm.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The Brownian germ zero-one argument needed for positive canonical mass before every positive time.

  1. lemma OAI.SLEExactGauge.brownian_germ_fdd_law line 17
  2. lemma OAI.SLEExactGauge.brownian_germ_path_law line 50
  3. theorem OAI.SLEExactGauge.brownian_germ_zero_one line 74

    Source documentation

    An event observable along times decreasing to zero has probability zero or one. Only the continuous based Brownian path is needed.

    theorem brownian_germ_zero_one
    (hB : IsBrownianReal B P) (hm : ∀ t, Measurable (B t))
    (hc : ∀ ω, Continuous (fun t => B t ω)) (h0 : ∀ ω, B 0 ω=0)
    (ε : ℕ → ℝ≥0) (hε : Tendsto ε atTop (𝓝 0))
    (E : Set Ω)
    (hE : ∀ n, MeasurableSet[Filtration.natural B (fun t => (hm t).stronglyMeasurable) (ε n)] E) :
    P E=0 ∨ P E=1 := by
…