FejerBounds.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.GeometricKernel.norm_geometric_sum_le line 9

Source documentation

The basic geometric-sum bound on the closed unit disc.

theorem norm_geometric_sum_le (h : ℕ) (z : ℂ)
    (hz : ‖z‖ ≤ 1) (hz1 : z ≠ 1) :
    ‖∑ j ∈ Finset.range h, z ^ j‖ ≤ 2 / ‖z - 1‖ := by
…

def OAI.Problem337.GeometricKernel.kernel line 22
Source documentation
The nonnegative, degree-normalized squared geometric sum.
```
noncomputable def kernel (h : ℕ) (z : ℂ) : ℝ :=
…
```
theorem OAI.Problem337.GeometricKernel.kernel_nonneg line 25
theorem OAI.Problem337.GeometricKernel.kernel_le_degree line 29
theorem OAI.Problem337.GeometricKernel.kernel_le_four_div line 49
Source documentation
Pointwise decay of the normalized kernel away from the identity.
```
theorem kernel_le_four_div (h : ℕ) (hh : 0 < h) (z : ℂ)
    (hz : ‖z‖ ≤ 1) (hz1 : z ≠ 1) :
    kernel h z ≤ 4 / ((h : ℝ) * ‖z - 1‖ ^ 2) := by
…
```
Mentions: OAI.Problem337.GeometricKernel.kernel
theorem OAI.Problem337.GeometricKernel.cyclic_geometric_sum_eq line 63
theorem OAI.Problem337.GeometricKernel.norm_cyclic_geometric_sum_le line 70