PeriodizedUniform.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.sourceFract_measurable line 11
theorem OAI.FiniteFactor.fract_unit_interval line 17
Source documentation
Every translated interval of length one maps to the same representative Haar measure under fractional part.
```
theorem fract_unit_interval (a : ℝ) :
    (volume.restrict (Set.Ioc a (a+1))).map Int.fract = unitIntervalMeasure := by
…
```
Mentions: OAI.FiniteFactor.unitIntervalMeasure
theorem OAI.FiniteFactor.fract_integer_interval line 25
theorem OAI.FiniteFactor.fract_interval_domination line 43
Source documentation
Periodizing normalized interval measure has density at most 1+1/length. The bound is expressed as domination of measures on every measurable set.
```
theorem fract_interval_domination (a b : ℝ) (hab : a < b) :
    (cond volume (Set.Ioc a b)).map Int.fract ≤
      ENNReal.ofReal (1+1/(b-a)) • unitIntervalMeasure := by
…
```
Mentions: OAI.FiniteFactor.unitIntervalMeasure
theorem OAI.FiniteFactor.cond_interval_mul_pos line 74
Source documentation
Positive scaling carries normalized interval measure to the normalized scaled interval; this identifies the actual phase law before periodization.
```
theorem cond_interval_mul_pos (a b c : ℝ) (hab : a < b) (hc : 0 < c) :
    (cond volume (Set.Ioc a b)).map (fun t => c*t) =
      cond volume (Set.Ioc (c*a) (c*b)) := by
…
```
theorem OAI.FiniteFactor.cond_closed_interval_eq line 92