OAI/Probability/SLE/Gauge/CoverEvents.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SLEExactGauge.isClosed_compact_time_hit line 17
2. lemma OAI.SLEExactGauge.measurableSet_whole_time_hit line 32
3. lemma OAI.SLEExactGauge.measurableSet_trace_hits_closed line 47
4. lemma OAI.SLEExactGauge.measurableSet_sausage_candidate line 53
5. lemma OAI.SLEExactGauge.measurableSet_visited_without_candidate line 61

   Source documentation

   Both visit and no-candidate information is terminal information. The finite change of law is applied later only to an adapted containing event.

   lemma measurableSet_visited_without_candidate
       {Ω ι : Type*} [MeasurableSpace Ω]
       (f : Ω → C(ℝ≥0, ℂ)) (hf : Measurable f)
       (κ v : ℝ) (I : Finset ι) (D : ι → Set ℂ) (b : ι → ℝ)
       {Q : Set ℂ} (hQ : IsClosed Q) :
       MeasurableSet {ω | (∃ u : ℝ≥0, f ω u ∈ Q) ∧
         ∀ i ∈ I, wholeSausageCharge κ (f ω) v (D i) < ENNReal.ofReal (b i)} := by
   …

   Mentions: OAI.SLEExactGauge.wholeSausageCharge