GlobalFromPeriodic.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem310Support.compact_complement_volume line 13

Source documentation

A small open deletion from the unit interval leaves a compact set whose volume is strictly greater than the requested threshold.

theorem compact_complement_volume {C : Set ℝ} (hC : IsOpen C)
    {η : ℝ} (hη : 0 < η) (hη1 : η < 1)
    (hsmall : volume (C ∩ Icc (0 : ℝ) 1) ≤ ENNReal.ofReal (η / 2)) :
    IsCompact (Icc (0 : ℝ) 1 \ C) ∧
      ENNReal.ofReal (1 - η) < volume (Icc (0 : ℝ) 1 \ C) := by
…

theorem OAI.Problem310Support.positive_scale_normalization line 38
Source documentation
Every positive scale can be moved into [1,2] by a natural power of two followed by passage to a dyadic tail.
```
theorem positive_scale_normalization {s : ℝ} (hs : 0 < s) :
    ∃ j m : ℕ, (s * (2 : ℝ) ^ j * ((2 : ℝ)⁻¹ ^ m)) ∈ Icc (1 : ℝ) 2 := by
…
```
def OAI.Problem310Support.signedDyadicUnion line 54
Source documentation
The paired pullbacks used to cover all signed scales.
```
def signedDyadicUnion (H : ℕ → Set ℝ) : Set ℝ :=
…
```
theorem OAI.Problem310Support.signedDyadicUnion_open line 58
theorem OAI.Problem310Support.signedDyadicUnion_neg line 65

theorem OAI.Problem310Support.signedDyadicUnion_hits line 78

Source documentation

The full signed-scale hitting property is a purely algebraic consequence of a normalized hitting set at every dyadic magnification.

theorem signedDyadicUnion_hits {H : ℕ → Set ℝ}
    (hH : ∀ j (x t : ℝ), t ∈ Icc (1 : ℝ) 2 →
      ∃ n : ℕ, 1 ≤ n ∧ x + t * ((2 : ℝ)⁻¹ ^ n) ∈ H j) :
    ∀ x s : ℝ, s ≠ 0 → ∃ n : ℕ, 1 ≤ n ∧
      x + s * ((2 : ℝ)⁻¹ ^ n) ∈ signedDyadicUnion H := by
…

Mentions: OAI.Problem310Support.signedDyadicUnion

theorem OAI.Problem310Support.signedDyadicUnion_volume_le line 107
Source documentation
The cost of pairing and summing the dyadic pullbacks is at most twice the sum of the original period densities.
```
theorem signedDyadicUnion_volume_le {H : ℕ → Set ℝ}
    (hH : ∀ j, ∀ x : ℝ, x + 1 ∈ H j ↔ x ∈ H j) :
    volume (signedDyadicUnion H ∩ Icc (0 : ℝ) 1) ≤
      ∑' j : ℕ, 2 * volume (H j ∩ Icc (0 : ℝ) 1) := by
…
```
Mentions: OAI.Problem310Support.signedDyadicUnion
theorem OAI.Problem310Support.dyadic_density_budget line 120

theorem OAI.Problem310Support.avoidance_of_periodic_hitting line 150

Source documentation

The global compact avoidance theorem follows from the periodic hitting lemma. All measure estimates, signed scales, and strict volume loss are included in this implication.

theorem avoidance_of_periodic_hitting
    (hperiodic : ∀ p : ℝ, 0 < p → p < 1 → ∃ H : Set ℝ,
      IsOpen H ∧ (∀ x : ℝ, x + 1 ∈ H ↔ x ∈ H) ∧
      volume (H ∩ Icc (0 : ℝ) 1) ≤ ENNReal.ofReal (6 * p) ∧
      ∀ x t : ℝ, t ∈ Icc (1 : ℝ) 2 → ∃ n : ℕ, 1 ≤ n ∧
        x + t * ((2 : ℝ)⁻¹ ^ n) ∈ H) :
    ∀ η : ℝ, 0 < η → η < 1 → ∃ E : Set ℝ,
      E ⊆ Icc (0 : ℝ) 1 ∧ IsCompact E ∧
      volume E > ENNReal.ofReal (1 - η) ∧
      ∀ x s : ℝ, s ≠ 0 → ∃ n : ℕ, 1 ≤ n ∧
        x + s * ((2 : ℝ)⁻¹ ^ n) ∉ E := by
…