IntervalError.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.interval_membership_stable line 11
Source documentation
Interval membership cannot change under a displacement smaller than delta when the starting point is farther than delta from both endpoints.
```
theorem interval_membership_stable (a b δ t u : ℝ) (_hδ : 0 ≤ δ)
    (ha : δ < |t-a|) (hb : δ < |t-b|) (htu : |t-u| < δ) :
    u ∈ Set.Icc a b ↔ t ∈ Set.Icc a b := by
…
```
theorem OAI.FiniteFactor.fract_displacement_middle line 33
Source documentation
A separated pair of representatives, with the first away from the cut, has a fractional displacement outside the kernel's exceptional arc.
```
theorem fract_displacement_middle (δ t u : ℝ) (hδ : 0 < δ)
    (ht : δ ≤ t) (ht' : t ≤ 1-δ) (hu : u ∈ Set.Ico (0 : ℝ) 1)
    (hsep : δ ≤ |t-u|) : Int.fract (t-u) ∈ Set.Icc δ (1-δ) := by
…
```

theorem OAI.FiniteFactor.samplingSmooth_interval_error line 49

Source documentation

The actual interval convolution differs from its indicator only by the proved kernel tail, away from interval endpoints and the circle cut.

theorem samplingSmooth_interval_error (H : ℕ) (hH : 0 < H) (a b δ t : ℝ)
    (hδ : 0 < δ) (ht : δ ≤ t) (ht' : t ≤ 1-δ)
    (ha : δ < |t-a|) (hb : δ < |t-b|) :
    |samplingSmooth H (Set.Icc a b) t - (Set.Icc a b).indicator (fun _ => (1 : ℝ)) t| ≤
      1/(4*(H : ℝ)*δ^2) := by
…

Mentions: OAI.FiniteFactor.samplingSmooth