PeriodicEnlargement.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem310.Auxiliary.closure_periodic line 12

Source documentation

Periodicity is preserved under topological closure.

theorem closure_periodic (B : Set ℝ)
    (hB : ∀ x : ℝ, x + 1 ∈ B ↔ x ∈ B) :
    ∀ x : ℝ, x + 1 ∈ closure B ↔ x ∈ closure B := by
…

theorem OAI.Problem310.Auxiliary.exists_open_periodic_enlargement line 26

Source documentation

A periodic set whose closure adds no density has arbitrarily economical open periodic enlargements. Finite unions of grid cells satisfy the closure hypothesis.

theorem exists_open_periodic_enlargement (B : Set ℝ)
    (hBp : ∀ x : ℝ, x + 1 ∈ B ↔ x ∈ B)
    (hBm : volume (closure B ∩ Icc (0 : ℝ) 1) = volume (B ∩ Icc (0 : ℝ) 1))
    (ε : ℝ) (hε : 0 < ε) :
    ∃ V : Set ℝ, IsOpen V ∧
      (∀ x : ℝ, x + 1 ∈ V ↔ x ∈ V) ∧ B ⊆ V ∧
      volume (V ∩ Icc (0 : ℝ) 1) ≤
        volume (B ∩ Icc (0 : ℝ) 1) + ENNReal.ofReal ε := by
…

theorem OAI.Problem310.Auxiliary.density_closure_eq_of_null_frontier line 39

Source documentation

Null frontier is a simple sufficient condition for the closure-density hypothesis.

theorem density_closure_eq_of_null_frontier (B : Set ℝ)
    (hB : volume (frontier B) = 0) :
    volume (closure B ∩ Icc (0 : ℝ) 1) = volume (B ∩ Icc (0 : ℝ) 1) := by
…

theorem OAI.Problem310.Auxiliary.exceptionalCenters_antitone line 46
Source documentation
Enlarging the test set can only remove exceptional centers.
```
theorem exceptionalCenters_antitone {B V : Set ℝ} (hBV : B ⊆ V)
    (N : Set ℕ) (a : ℕ → ℝ) :
    exceptionalCenters V N a ⊆ exceptionalCenters B N a := by
…
```
Mentions: OAI.Problem310.Auxiliary.exceptionalCenters