KernelTail.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.samplingCharacter_nat line 9
theorem OAI.FiniteFactor.samplingKernel_geometric_bound line 17
Source documentation
Geometric-sum cancellation controls the kernel away from the origin.
```
theorem samplingKernel_geometric_bound (H : ℕ) (t : ℝ) :
    ‖∑ r ∈ Finset.range H, samplingCharacter (r : ℤ) t‖ *
      ‖samplingCharacter 1 t - 1‖ ≤ 2 := by
…
```
Mentions: OAI.FiniteFactor.samplingCharacter
theorem OAI.FiniteFactor.samplingCharacter_chord_lower line 27
Source documentation
Elementary chord lower bound, including both halves of the unit interval.
```
theorem samplingCharacter_chord_lower (δ t : ℝ) (hδ : 0 ≤ δ)
    (ht : δ ≤ t) (ht' : t ≤ 1-δ) :
    4*δ ≤ ‖samplingCharacter 1 t-1‖ := by
…
```
Mentions: OAI.FiniteFactor.samplingCharacter
theorem OAI.FiniteFactor.samplingKernel_tail_bound line 55
theorem OAI.FiniteFactor.samplingKernel_tail_integral line 76
Source documentation
Actual mass of the part of the Fejer kernel outside a delta-neighborhood of the integer cut.
```
theorem samplingKernel_tail_integral (H : ℕ) (hH : 0 < H) (δ : ℝ) (hδ : 0 < δ) :
    (∫ t in Set.Icc δ (1-δ), samplingKernel H t ∂unitIntervalMeasure) ≤
      1/(4*(H : ℝ)*δ^2) := by
…
```
Mentions: OAI.FiniteFactor.samplingKernel, OAI.FiniteFactor.unitIntervalMeasure