Source indexedlemma · leanprover/lean4:v4.32.0

dirichletApprox_eq_add_dirichletApproxAux

Carleson.Classical.HilbertStrongType · Carleson/Classical/HilbertStrongType.lean:499 to 513

Mathematical statement

Exact Lean statement

lemma dirichletApprox_eq_add_dirichletApproxAux
    {n : ℕ} {x : ℝ} (hx : exp (I * x) ≠ 1) (hn : n ≠ 0) :
    dirichletApprox n x = (1 - exp (I * x)) ⁻¹ + dirichletApproxAux n x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma dirichletApprox_eq_add_dirichletApproxAux    {n : ℕ} {x : ℝ} (hx : exp (I * x) ≠ 1) (hn : n ≠ 0) :    dirichletApprox n x = (1 - exp (I * x)) ⁻¹ + dirichletApproxAux n x := by  have : Finset.Ico n (2 * n) = Finset.Ico (0 + n) (n + n) := by simp [Nat.two_mul n]  simp only [dirichletApprox, this, ← Finset.sum_Ico_add]  simp_rw [dirichletKernel_eq hx]  simp only [Nat.Ico_zero_eq_range, dirichletKernel', Nat.cast_add, mul_assoc, add_mul, neg_mul,    div_eq_inv_mul, ← exp_add, neg_add_cancel, exp_zero, mul_one, Finset.sum_add_distrib,    Finset.sum_const, Finset.card_range, nsmul_eq_mul]  simp only [mul_add, ← mul_assoc]  rw [inv_mul_cancel₀ (mod_cast hn)]  simp only [mul_assoc, Finset.mul_sum, one_mul, dirichletApproxAux, neg_mul, div_eq_inv_mul,    Nat.Ico_zero_eq_range, ← exp_add, add_comm (1 - exp (I * ↑x))⁻¹, add_left_inj]  congr with i  ring_nf