Source indexedlemma · leanprover/lean4:v4.32.0

norm_dirichletApproxAux_le

Carleson.Classical.HilbertStrongType · Carleson/Classical/HilbertStrongType.lean:585 to 596

Mathematical statement

Exact Lean statement

lemma norm_dirichletApproxAux_le {n : ℕ} {x r : ℝ} (hx : exp (I * x) ≠ 1)
    (hxr : r ≤ |x|) (hxpi : |x| ≤ π)
    (hn : r⁻¹ ≤ n) (hr : 0 < r) (h'r : r < 1) :
    ‖dirichletApproxAux n x‖ ≤ 10 * niceKernel r x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma norm_dirichletApproxAux_le {n : ℕ} {x r : ℝ} (hx : exp (I * x) ≠ 1)    (hxr : r ≤ |x|) (hxpi : |x| ≤ π)    (hn : r⁻¹ ≤ n) (hr : 0 < r) (h'r : r < 1) :    ‖dirichletApproxAux n x‖ ≤ 10 * niceKernel r x := by  have A : ‖dirichletApproxAux n x‖ ≤ 2 * (1 + r / ‖1 - exp (I * x)‖ ^ 2) := by    rcases le_total (re (exp (I * x))) 0 with h'x | h'x    · apply norm_dirichletApproxAux_le_of_re_nonpos h'x hr    · apply norm_dirichletApproxAux_le_of_re_nonneg hx h'x hn hr  apply A.trans  rw [show (10 : ℝ) = 2 * 5 by norm_num, mul_assoc]  gcongr  exact niceKernel_lowerBound' hr h'r ⟨hxr, hxpi⟩