Theorem: norm_dirichletKernel_le (Carleson/Theorem1_1/Dirichlet_kernel.lean)

State before:
N : ℕ
x : ℝ
⊢ ‖dirichletKernel N x‖ ≤ 2 * ↑N + 1
Tactic:
rw [dirichletKernel]
State after:
N : ℕ
x : ℝ
⊢ ‖∑ n ∈ Icc (-Int.ofNat N) ↑N, (fourier n) ↑x‖ ≤ 2 * ↑N + 1

State before:
N : ℕ
x : ℝ
⊢ ‖∑ n ∈ Icc (-Int.ofNat N) ↑N, (fourier n) ↑x‖ ≤ 2 * ↑N + 1
Tactic:
calc ‖∑ n ∈ Icc (-Int.ofNat N) ↑N, (fourier n) ↑x‖
  _ ≤ ∑ n ∈ Icc (-Int.ofNat N) ↑N, ‖(fourier n) ↑x‖ := by
    apply norm_sum_le
  _ ≤ ∑ n ∈ Icc (-Int.ofNat N) ↑N, 1 := by
    apply sum_le_sum
    intro n _
    have : Fact (0 < 2 * Real.pi) := by
      rw [fact_iff]
      exact Real.two_pi_pos
    apply le_trans (ContinuousMap.norm_coe_le_norm (fourier n) x) (fourier_norm n).le
  _ = 2 * N + 1 := by
    rw [sum_const]
    simp only [Int.ofNat_eq_coe, Int.card_Icc, sub_neg_eq_add, nsmul_eq_mul, mul_one]
    norm_cast
    rw [Int.toNat_ofNat]
    ring
State after:
no goals

State before:
N : ℕ
x : ℝ
⊢ ‖∑ n ∈ Icc (-Int.ofNat N) ↑N, (fourier n) ↑x‖ ≤ ∑ n ∈ Icc (-Int.ofNat N) ↑N, ‖(fourier n) ↑x‖
Tactic:
apply norm_sum_le
State after:
no goals

State before:
N : ℕ
x : ℝ
⊢ ∑ n ∈ Icc (-Int.ofNat N) ↑N, ‖(fourier n) ↑x‖ ≤ ∑ n ∈ Icc (-Int.ofNat N) ↑N, 1
Tactic:
apply sum_le_sum
State after:
case h
N : ℕ
x : ℝ
⊢ ∀ i ∈ Icc (-Int.ofNat N) ↑N, ‖(fourier i) ↑x‖ ≤ 1

State before:
case h
N : ℕ
x : ℝ
⊢ ∀ i ∈ Icc (-Int.ofNat N) ↑N, ‖(fourier i) ↑x‖ ≤ 1
Tactic:
intro n _
State after:
case h
N : ℕ
x : ℝ
n : ℤ
a✝ : n ∈ Icc (-Int.ofNat N) ↑N
⊢ ‖(fourier n) ↑x‖ ≤ 1

State before:
case h
N : ℕ
x : ℝ
n : ℤ
a✝ : n ∈ Icc (-Int.ofNat N) ↑N
⊢ ‖(fourier n) ↑x‖ ≤ 1
Tactic:
have : Fact (0 < 2 * Real.pi) := by
  rw [fact_iff]
  exact Real.two_pi_pos
State after:
case h
N : ℕ
x : ℝ
n : ℤ
a✝ : n ∈ Icc (-Int.ofNat N) ↑N
this : Fact (0 < 2 * Real.pi)
⊢ ‖(fourier n) ↑x‖ ≤ 1

State before:
case h
N : ℕ
x : ℝ
n : ℤ
a✝ : n ∈ Icc (-Int.ofNat N) ↑N
this : Fact (0 < 2 * Real.pi)
⊢ ‖(fourier n) ↑x‖ ≤ 1
Tactic:
apply le_trans (ContinuousMap.norm_coe_le_norm (fourier n) x) (fourier_norm n).le
State after:
no goals

State before:
N : ℕ
x : ℝ
n : ℤ
a✝ : n ∈ Icc (-Int.ofNat N) ↑N
⊢ Fact (0 < 2 * Real.pi)
Tactic:
rw [fact_iff]
State after:
N : ℕ
x : ℝ
n : ℤ
a✝ : n ∈ Icc (-Int.ofNat N) ↑N
⊢ 0 < 2 * Real.pi

State before:
N : ℕ
x : ℝ
n : ℤ
a✝ : n ∈ Icc (-Int.ofNat N) ↑N
⊢ 0 < 2 * Real.pi
Tactic:
exact Real.two_pi_pos
State after:
no goals

State before:
N : ℕ
x : ℝ
⊢ ∑ n ∈ Icc (-Int.ofNat N) ↑N, 1 = 2 * ↑N + 1
Tactic:
rw [sum_const]
State after:
N : ℕ
x : ℝ
⊢ (Icc (-Int.ofNat N) ↑N).card • 1 = 2 * ↑N + 1

State before:
N : ℕ
x : ℝ
⊢ (Icc (-Int.ofNat N) ↑N).card • 1 = 2 * ↑N + 1
Tactic:
simp only [Int.ofNat_eq_coe, Int.card_Icc, sub_neg_eq_add, nsmul_eq_mul, mul_one]
State after:
N : ℕ
x : ℝ
⊢ ↑(↑N + 1 + ↑N).toNat = 2 * ↑N + 1

State before:
N : ℕ
x : ℝ
⊢ ↑(↑N + 1 + ↑N).toNat = 2 * ↑N + 1
Tactic:
norm_cast
State after:
N : ℕ
x : ℝ
⊢ (↑(N + 1 + N)).toNat = 2 * N + 1

State before:
N : ℕ
x : ℝ
⊢ (↑(N + 1 + N)).toNat = 2 * N + 1
Tactic:
rw [Int.toNat_ofNat]
State after:
N : ℕ
x : ℝ
⊢ N + 1 + N = 2 * N + 1

State before:
N : ℕ
x : ℝ
⊢ N + 1 + N = 2 * N + 1
Tactic:
ring
State after:
no goals