CountableInteriorIntervals.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The deterministic countable certificates for the retained middle-strip intervals. An actual open interior visit contains a nondegenerate rational time interval, whose image lies in one fixed countable compact exhaustion.

theorem OAI.SLEExactGauge.exists_countable_compact_exhaustion_open line 16
theorem OAI.SLEExactGauge.exists_rational_interval_in_open_visit line 35

theorem OAI.SLEExactGauge.rational_interval_compact_certificate line 54

Source documentation

One countable compact family captures every open visit, at rational times strictly between the entry and the later crossing.

theorem rational_interval_compact_certificate
    (O : Set ℂ) (hO : IsOpen O) :
    ∃ K : ℕ → Set ℂ, (∀ n, IsCompact (K n)) ∧ (∀ n, K n ⊆ O) ∧
      ∀ (f : ℝ → ℂ), Continuous f → ∀ a b : ℝ,
        (∃ u ∈ Ioo a b, f u ∈ O) →
        ∃ (s t : ℚ) (n : ℕ), a < (s : ℝ) ∧ (s : ℝ) < t ∧
          (t : ℝ) < b ∧ f '' Icc (s : ℝ) t ⊆ K n := by
…

theorem OAI.SLEExactGauge.isClosed_interval_compact_certificate line 73
theorem OAI.SLEExactGauge.measurableSet_interval_compact_certificate line 84