PeriodicEnvelope.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem310.Aux.integerPeriodize line 11
Source documentation
Integer-periodization of a subset of the line.
```
def integerPeriodize (U : Set ℝ) : Set ℝ :=
…
```
theorem OAI.Problem310.Aux.isOpen_integerPeriodize line 14
theorem OAI.Problem310.Aux.integerPeriodize_onePeriodic line 18
theorem OAI.Problem310.Aux.volume_integerPeriodize_le line 36
Source documentation
Periodization cannot increase the measure within a fundamental interval beyond the measure of the original subset.
```
theorem volume_integerPeriodize_le (U : Set ℝ) (hU : MeasurableSet U) :
    volume (integerPeriodize U ∩ Icc (0 : ℝ) 1) ≤ volume U := by
…
```
Mentions: OAI.Problem310.Aux.integerPeriodize

theorem OAI.Problem310.Aux.exists_open_periodic_envelope line 78

Source documentation

An arbitrarily small open periodic enlargement of a periodic set.

theorem exists_open_periodic_envelope (R : Set ℝ)
    (hR : ∀ x : ℝ, x + 1 ∈ R ↔ x ∈ R) (ε : ENNReal) (hε : ε ≠ 0) :
    ∃ V : Set ℝ, R ⊆ V ∧ IsOpen V ∧
      (∀ x : ℝ, x + 1 ∈ V ↔ x ∈ V) ∧
      volume (V ∩ Icc (0 : ℝ) 1) ≤ volume (R ∩ Icc (0 : ℝ) 1) + ε := by
…