ThreePrimePartialSummation.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.ThreePrimeAnalysis.weighted_sum_norm_le_partial_sum_bound line 10

Source documentation

Finite Abel summation controlled by initial partial sums and total variation.

theorem weighted_sum_norm_le_partial_sum_bound
    (a b : ℕ → ℂ) (n : ℕ) (B : ℝ)
    (hprefix : ∀ k ≤ n + 1, ‖∑ j ∈ Finset.range k, a j‖ ≤ B) :
    ‖∑ j ∈ Finset.range (n + 1), b j * a j‖ ≤
      B * (‖b n‖ + ∑ j ∈ Finset.range n, ‖b (j + 1) - b j‖) := by
…

theorem OAI.Problem337.ThreePrimeAnalysis.norm_exp_I_mul_sub_le line 39

Source documentation

The unit exponential is one-Lipschitz in its real angle.

theorem norm_exp_I_mul_sub_le (x y : ℝ) :
    ‖Complex.exp (Complex.I * (x : ℂ)) - Complex.exp (Complex.I * (y : ℂ))‖ ≤
      |x - y| := by
…

theorem OAI.Problem337.ThreePrimeAnalysis.linear_phase_sum_norm_le line 54

Source documentation

Linear-phase Abel transfer, uniform in the initial angle and frequency.

theorem linear_phase_sum_norm_le
    (a : ℕ → ℂ) (N : ℕ) (B α t : ℝ) (hB : 0 ≤ B)
    (hprefix : ∀ k ≤ N, ‖∑ j ∈ Finset.range k, a j‖ ≤ B) :
    ‖∑ j ∈ Finset.range N,
      Complex.exp (Complex.I * ((α + t * j : ℝ) : ℂ)) * a j‖ ≤
        B * (1 + |t| * N) := by
…

theorem OAI.Problem337.ThreePrimeAnalysis.twisted_sum_sub_norm_le line 88

Source documentation

The major-arc partial-summation error estimate, in turns rather than radians. It is conditional only on the stated finite prefix discrepancy.

theorem twisted_sum_sub_norm_le
    (a b : ℕ → ℂ) (N : ℕ) (B β : ℝ) (hB : 0 ≤ B)
    (hprefix : ∀ k ≤ N,
      ‖(∑ j ∈ Finset.range k, a j) - ∑ j ∈ Finset.range k, b j‖ ≤ B) :
    ‖(∑ j ∈ Finset.range N,
        Complex.exp (Complex.I * ((2 * Real.pi * β * j : ℝ) : ℂ)) * a j) -
      ∑ j ∈ Finset.range N,
        Complex.exp (Complex.I * ((2 * Real.pi * β * j : ℝ) : ℂ)) * b j‖ ≤
      B * (1 + 2 * Real.pi * |β| * N) := by
…