ExceptionalCenters.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem310.Auxiliary.exceptionalCenters line 14
Source documentation
Centers at which some normalized scale avoids all the selected tests.
```
def exceptionalCenters (B : Set ℝ) (N : Set ℕ) (a : ℕ → ℝ) : Set ℝ :=
…
```
theorem OAI.Problem310.Auxiliary.isClosed_exceptionalCenters line 18
Source documentation
Compactness of the normalized scale interval makes the exceptional centers closed.
```
theorem isClosed_exceptionalCenters (B : Set ℝ) (hB : IsOpen B)
    (N : Set ℕ) (a : ℕ → ℝ) : IsClosed (exceptionalCenters B N a) := by
…
```
Mentions: OAI.Problem310.Auxiliary.exceptionalCenters

theorem OAI.Problem310.Auxiliary.exceptionalCenters_periodic line 43

Source documentation

Periodicity passes from the selected set to its exceptional centers.

theorem exceptionalCenters_periodic (B : Set ℝ)
    (hB : ∀ x : ℝ, x + 1 ∈ B ↔ x ∈ B) (N : Set ℕ) (a : ℕ → ℝ) :
    ∀ x : ℝ, x + 1 ∈ exceptionalCenters B N a ↔
      x ∈ exceptionalCenters B N a := by
…

Mentions: OAI.Problem310.Auxiliary.exceptionalCenters

theorem OAI.Problem310.Auxiliary.exists_tail_mem_of_tendsto line 60

Source documentation

An open neighborhood of a limit point meets every tail of a converging sequence.

theorem exists_tail_mem_of_tendsto (a : ℕ → ℝ) (ha : Tendsto a atTop (𝓝 0))
    (V : Set ℝ) (hV : IsOpen V) (x : ℝ) (hx : x ∈ V) (t : ℝ) :
    ∃ n : ℕ, 1 ≤ n ∧ x + t * a n ∈ V := by
…

theorem OAI.Problem310.Auxiliary.exceptionalCenters_repair line 70

Source documentation

Open-neighborhood repair turns tests away from exceptional centers into hits everywhere.

theorem exceptionalCenters_repair (B V : Set ℝ) (N : Set ℕ) (a : ℕ → ℝ)
    (ha : Tendsto a atTop (𝓝 0)) (hN : ∀ n ∈ N, 1 ≤ n)
    (hV : IsOpen V) (hcover : exceptionalCenters B N a ⊆ V) :
    ∀ x t : ℝ, t ∈ Icc (1 : ℝ) 2 →
      ∃ n : ℕ, 1 ≤ n ∧ x + t * a n ∈ B ∪ V := by
…

Mentions: OAI.Problem310.Auxiliary.exceptionalCenters

theorem OAI.Problem310.Auxiliary.thickening_periodic line 88

Source documentation

Thickening preserves one-periodicity.

theorem thickening_periodic (R : Set ℝ)
    (hR : ∀ x : ℝ, x + 1 ∈ R ↔ x ∈ R) (ε : ℝ) :
    ∀ x : ℝ, x + 1 ∈ thickening ε R ↔ x ∈ thickening ε R := by
…

theorem OAI.Problem310.Auxiliary.exists_open_periodic_superset line 105

Source documentation

A closed periodic set admits an open periodic neighborhood with arbitrarily small increase of its measure in one period.

theorem exists_open_periodic_superset (R : Set ℝ) (hRc : IsClosed R)
    (hRp : ∀ x : ℝ, x + 1 ∈ R ↔ x ∈ R) (ε : ℝ) (hε : 0 < ε) :
    ∃ V : Set ℝ, IsOpen V ∧
      (∀ x : ℝ, x + 1 ∈ V ↔ x ∈ V) ∧ R ⊆ V ∧
      volume (V ∩ Icc (0 : ℝ) 1) ≤
        volume (R ∩ Icc (0 : ℝ) 1) + ENNReal.ofReal ε := by
…

theorem OAI.Problem310.Auxiliary.repair_open_periodic_hitting line 136

Source documentation

Deterministic completion of the probabilistic construction: once the density of an open test set plus its exceptional centers is small, a genuinely hitting open periodic set is available at arbitrarily small additional density cost.

theorem repair_open_periodic_hitting
    (B : Set ℝ) (hBo : IsOpen B)
    (hBp : ∀ x : ℝ, x + 1 ∈ B ↔ x ∈ B)
    (N : Set ℕ) (hN : ∀ n ∈ N, 1 ≤ n)
    (a : ℕ → ℝ) (ha : Tendsto a atTop (𝓝 0))
    (c : ENNReal)
    (hbound : volume (B ∩ Icc (0 : ℝ) 1) +
      volume (exceptionalCenters B N a ∩ Icc (0 : ℝ) 1) ≤ c)
    (ε : ℝ) (hε : 0 < ε) :
    ∃ H : Set ℝ, IsOpen H ∧
      (∀ x : ℝ, x + 1 ∈ H ↔ x ∈ H) ∧
      volume (H ∩ Icc (0 : ℝ) 1) ≤ c + ENNReal.ofReal ε ∧
…

Mentions: OAI.Problem310.Auxiliary.exceptionalCenters

theorem OAI.Problem310.Auxiliary.dyadic_tendsto_zero line 170
Source documentation
The dyadic sequence converges to zero.
```
theorem dyadic_tendsto_zero :
    Tendsto (fun n : ℕ => (2 : ℝ)⁻¹ ^ n) atTop (𝓝 0) := by
…
```
theorem OAI.Problem310.Auxiliary.periodic_hitting_of_small_exceptional line 174