GeometricCharacterBound.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.norm_geometric_sum_le_two_div line 11

Source documentation

Geometric cancellation on the complex unit circle.

theorem norm_geometric_sum_le_two_div {z : ℂ} (hz : ‖z‖ = 1) (hne : z ≠ 1)
    (N : ℕ) : ‖∑ j ∈ Finset.range N, z ^ j‖ ≤ 2 / ‖z - 1‖ := by
…

theorem OAI.Problem337.norm_geometric_sum_le_card line 20

Source documentation

The elementary peak bound for a geometric kernel.

theorem norm_geometric_sum_le_card {z : ℂ} (hz : ‖z‖ = 1) (N : ℕ) :
    ‖∑ j ∈ Finset.range N, z ^ j‖ ≤ (N : ℝ) := by
…

theorem OAI.Problem337.geometric_fejer_le line 27

Source documentation

Squared cancellation with the usual Fejer normalization.

theorem geometric_fejer_le {z : ℂ} (hz : ‖z‖ = 1) (hne : z ≠ 1)
    {N : ℕ} (hN : 0 < N) :
    ‖∑ j ∈ Finset.range N, z ^ j‖ ^ 2 / (N : ℝ) ≤
      4 / ((N : ℝ) * ‖z - 1‖ ^ 2) := by
…

theorem OAI.Problem337.norm_exp_phase_sub_one line 41

Source documentation

The chord distance for a phase of period one.

theorem norm_exp_phase_sub_one (x : ℝ) :
    ‖Complex.exp (Complex.I * (2 * Real.pi * x : ℝ)) - 1‖ =
      2 * |Real.sin (Real.pi * x)| := by
…

theorem OAI.Problem337.norm_geometric_phase_sum_le line 50

Source documentation

Geometric cancellation expressed directly in terms of the phase sine.

theorem norm_geometric_phase_sum_le {x : ℝ} (hx : Real.sin (Real.pi * x) ≠ 0)
    (N : ℕ) :
    ‖∑ j ∈ Finset.range N, (Complex.exp (Complex.I * (2 * Real.pi * x : ℝ))) ^ j‖ ≤
      1 / |Real.sin (Real.pi * x)| := by
…

theorem OAI.Problem337.sin_pi_mul_lower_on_middle line 67

Source documentation

Uniform lower bound for the sine away from both ends of a period.

theorem sin_pi_mul_lower_on_middle {δ x : ℝ} (hδ : 0 < δ)
    (hleft : δ ≤ x) (hright : x ≤ 1 - δ) :
    2 * δ ≤ Real.sin (Real.pi * x) := by
…

theorem OAI.Problem337.norm_geometric_phase_sum_le_middle line 87

Source documentation

A phase at distance at least δ from the ends gives a uniform kernel bound.

theorem norm_geometric_phase_sum_le_middle {δ x : ℝ} (hδ : 0 < δ)
    (hleft : δ ≤ x) (hright : x ≤ 1 - δ) (N : ℕ) :
    ‖∑ j ∈ Finset.range N, (Complex.exp (Complex.I * (2 * Real.pi * x : ℝ))) ^ j‖ ≤
      1 / (2 * δ) := by
…

theorem OAI.Problem337.geometric_phase_fejer_le_middle line 99

Source documentation

Fejer leakage at phase distance at least δ from zero modulo one.

theorem geometric_phase_fejer_le_middle {δ x : ℝ} (hδ : 0 < δ)
    (hleft : δ ≤ x) (hright : x ≤ 1 - δ) {N : ℕ} (hN : 0 < N) :
    ‖∑ j ∈ Finset.range N, (Complex.exp (Complex.I * (2 * Real.pi * x : ℝ))) ^ j‖ ^ 2 /
      (N : ℝ) ≤ 1 / (4 * (N : ℝ) * δ ^ 2) := by
…

theorem OAI.Problem337.stdAddChar_eq_normalized_phase line 111

Source documentation

The standard cyclic character is the period-one phase at its normalized value.

theorem stdAddChar_eq_normalized_phase {p : ℕ} [NeZero p] (a : ZMod p) :
    ZMod.stdAddChar a =
      Complex.exp (Complex.I * (2 * Real.pi * ((a.val : ℝ) / (p : ℝ)) : ℝ)) := by
…

theorem OAI.Problem337.norm_stdAddChar_range_sum_le line 120

Source documentation

Standard-character cancellation on an interval of consecutive integer multiples.

theorem norm_stdAddChar_range_sum_le {p : ℕ} [NeZero p] (a : ZMod p)
    (ha : a ≠ 0) (N : ℕ) :
    ‖∑ j ∈ Finset.range N, ZMod.stdAddChar ((j : ZMod p) * a)‖ ≤
      2 / ‖ZMod.stdAddChar a - 1‖ := by
…

theorem OAI.Problem337.norm_stdAddChar_range_sum_le_middle line 136

Source documentation

The cyclic-character version ready for interval smoothing.

theorem norm_stdAddChar_range_sum_le_middle {p : ℕ} [NeZero p] (a : ZMod p)
    {δ : ℝ} (hδ : 0 < δ) (hleft : δ ≤ (a.val : ℝ) / p)
    (hright : (a.val : ℝ) / p ≤ 1 - δ) (N : ℕ) :
    ‖∑ j ∈ Finset.range N, ZMod.stdAddChar ((j : ZMod p) * a)‖ ≤ 1 / (2 * δ) := by
…

theorem OAI.Problem337.stdAddChar_fejer_le_middle line 147

Source documentation

Squared cyclic kernel leakage, normalized to have total mass one.

theorem stdAddChar_fejer_le_middle {p : ℕ} [NeZero p] (a : ZMod p)
    {δ : ℝ} (hδ : 0 < δ) (hleft : δ ≤ (a.val : ℝ) / p)
    (hright : (a.val : ℝ) / p ≤ 1 - δ) {N : ℕ} (hN : 0 < N) :
    ‖∑ j ∈ Finset.range N, ZMod.stdAddChar ((j : ZMod p) * a)‖ ^ 2 / (N : ℝ) ≤
      1 / (4 * (N : ℝ) * δ ^ 2) := by
…