Theorem: limiting_fourier_lim1 (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
⊢ Tendsto (fun σ' => ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)) (𝓝[>] 1)
    (𝓝 (∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)))
Tactic:
obtain ⟨C, hC⟩ := decay_bounds_cor ψ
State after:
case intro
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
⊢ Tendsto (fun σ' => ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)) (𝓝[>] 1)
    (𝓝 (∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)))

State before:
case intro
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
⊢ Tendsto (fun σ' => ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)) (𝓝[>] 1)
    (𝓝 (∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)))
Tactic:
have : 0 ≤ C := by simpa using (norm_nonneg _).trans (hC 0)
State after:
case intro
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this : 0 ≤ C
⊢ Tendsto (fun σ' => ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)) (𝓝[>] 1)
    (𝓝 (∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)))

State before:
case intro
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this : 0 ≤ C
⊢ Tendsto (fun σ' => ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)) (𝓝[>] 1)
    (𝓝 (∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)))
Tactic:
refine tendsto_tsum_of_dominated_convergence (limiting_fourier_lim1_aux hcheby hx C this) (fun n => ?_) ?_
State after:
case intro.refine_1
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this : 0 ≤ C
n : ℕ
⊢ Tendsto (fun x_1 => term f (↑x_1) n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)) (𝓝[>] 1)
    (𝓝 (f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)))

case intro.refine_2
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this : 0 ≤ C
⊢ ∀ᶠ (n : ℝ) in 𝓝[>] 1,
    ∀ (k : ℕ),
      ‖term f (↑n) k * 𝓕 ψ.toFun (1 / (2 * π) * (↑k / x).log)‖ ≤
        ‖f k‖ / ↑k * (C / (1 + (1 / (2 * π) * (↑k / x).log) ^ 2))

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
⊢ 0 ≤ C
Tactic:
simpa using (norm_nonneg _).trans (hC 0)
State after:
no goals

State before:
case intro.refine_1
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this : 0 ≤ C
n : ℕ
⊢ Tendsto (fun x_1 => term f (↑x_1) n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)) (𝓝[>] 1)
    (𝓝 (f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)))
Tactic:
apply Tendsto.mul_const
State after:
case intro.refine_1.h
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this : 0 ≤ C
n : ℕ
⊢ Tendsto (fun k => term f (↑k) n) (𝓝[>] 1) (𝓝 (f n / ↑n))

State before:
case intro.refine_1.h
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this : 0 ≤ C
n : ℕ
⊢ Tendsto (fun k => term f (↑k) n) (𝓝[>] 1) (𝓝 (f n / ↑n))
Tactic:
by_cases h : n = 0 <;> simp [term, h]
State after:
case neg
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this : 0 ≤ C
n : ℕ
h : ¬n = 0
⊢ Tendsto (fun k => f n / ↑n ^ ↑k) (𝓝[>] 1) (𝓝 (f n / ↑n))

State before:
case neg
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this : 0 ≤ C
n : ℕ
h : ¬n = 0
⊢ Tendsto (fun k => f n / ↑n ^ ↑k) (𝓝[>] 1) (𝓝 (f n / ↑n))
Tactic:
refine tendsto_const_nhds.div ?_ (by simp [h])
State after:
case neg
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this : 0 ≤ C
n : ℕ
h : ¬n = 0
⊢ Tendsto (fun k => ↑n ^ ↑k) (𝓝[>] 1) (𝓝 ↑n)

State before:
case neg
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this : 0 ≤ C
n : ℕ
h : ¬n = 0
⊢ Tendsto (fun k => ↑n ^ ↑k) (𝓝[>] 1) (𝓝 ↑n)
Tactic:
simpa using ((continuous_ofReal.tendsto 1).mono_left nhdsWithin_le_nhds).const_cpow
State after:
no goals

State before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this : 0 ≤ C
n : ℕ
h : ¬n = 0
⊢ ↑n ≠ 0
Tactic:
simp [h]
State after:
no goals

State before:
case intro.refine_2
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this : 0 ≤ C
⊢ ∀ᶠ (n : ℝ) in 𝓝[>] 1,
    ∀ (k : ℕ),
      ‖term f (↑n) k * 𝓕 ψ.toFun (1 / (2 * π) * (↑k / x).log)‖ ≤
        ‖f k‖ / ↑k * (C / (1 + (1 / (2 * π) * (↑k / x).log) ^ 2))
Tactic:
rw [eventually_nhdsWithin_iff]
State after:
case intro.refine_2
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this : 0 ≤ C
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝 1,
    x_1 ∈ Ioi 1 →
      ∀ (k : ℕ),
        ‖term f (↑x_1) k * 𝓕 ψ.toFun (1 / (2 * π) * (↑k / x).log)‖ ≤
          ‖f k‖ / ↑k * (C / (1 + (1 / (2 * π) * (↑k / x).log) ^ 2))

State before:
case intro.refine_2
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this : 0 ≤ C
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝 1,
    x_1 ∈ Ioi 1 →
      ∀ (k : ℕ),
        ‖term f (↑x_1) k * 𝓕 ψ.toFun (1 / (2 * π) * (↑k / x).log)‖ ≤
          ‖f k‖ / ↑k * (C / (1 + (1 / (2 * π) * (↑k / x).log) ^ 2))
Tactic:
apply eventually_of_forall
State after:
case intro.refine_2.hp
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this : 0 ≤ C
⊢ ∀ x_1 ∈ Ioi 1,
    ∀ (k : ℕ),
      ‖term f (↑x_1) k * 𝓕 ψ.toFun (1 / (2 * π) * (↑k / x).log)‖ ≤
        ‖f k‖ / ↑k * (C / (1 + (1 / (2 * π) * (↑k / x).log) ^ 2))

State before:
case intro.refine_2.hp
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this : 0 ≤ C
⊢ ∀ x_1 ∈ Ioi 1,
    ∀ (k : ℕ),
      ‖term f (↑x_1) k * 𝓕 ψ.toFun (1 / (2 * π) * (↑k / x).log)‖ ≤
        ‖f k‖ / ↑k * (C / (1 + (1 / (2 * π) * (↑k / x).log) ^ 2))
Tactic:
intro σ' (hσ' : 1 < σ') n
State after:
case intro.refine_2.hp
n✝ : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this : 0 ≤ C
σ' : ℝ
hσ' : 1 < σ'
n : ℕ
⊢ ‖term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)‖ ≤ ‖f n‖ / ↑n * (C / (1 + (1 / (2 * π) * (↑n / x).log) ^ 2))

State before:
case intro.refine_2.hp
n✝ : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this : 0 ≤ C
σ' : ℝ
hσ' : 1 < σ'
n : ℕ
⊢ ‖term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)‖ ≤ ‖f n‖ / ↑n * (C / (1 + (1 / (2 * π) * (↑n / x).log) ^ 2))
Tactic:
rw [norm_mul, ← nterm_eq_norm_term]
State after:
case intro.refine_2.hp
n✝ : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this : 0 ≤ C
σ' : ℝ
hσ' : 1 < σ'
n : ℕ
⊢ nterm f σ' n * ‖𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)‖ ≤ ‖f n‖ / ↑n * (C / (1 + (1 / (2 * π) * (↑n / x).log) ^ 2))

State before:
case intro.refine_2.hp
n✝ : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this : 0 ≤ C
σ' : ℝ
hσ' : 1 < σ'
n : ℕ
⊢ nterm f σ' n * ‖𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)‖ ≤ ‖f n‖ / ↑n * (C / (1 + (1 / (2 * π) * (↑n / x).log) ^ 2))
Tactic:
refine mul_le_mul ?_ (hC _) (norm_nonneg _) (div_nonneg (norm_nonneg _) (Nat.cast_nonneg _))
State after:
case intro.refine_2.hp
n✝ : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this : 0 ≤ C
σ' : ℝ
hσ' : 1 < σ'
n : ℕ
⊢ nterm f σ' n ≤ ‖f n‖ / ↑n

State before:
case intro.refine_2.hp
n✝ : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this : 0 ≤ C
σ' : ℝ
hσ' : 1 < σ'
n : ℕ
⊢ nterm f σ' n ≤ ‖f n‖ / ↑n
Tactic:
by_cases h : n = 0 <;> simp [h, nterm]
State after:
case neg
n✝ : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this : 0 ≤ C
σ' : ℝ
hσ' : 1 < σ'
n : ℕ
h : ¬n = 0
⊢ Complex.abs (f n) / ↑n ^ σ' ≤ Complex.abs (f n) / ↑n

State before:
case neg
n✝ : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this : 0 ≤ C
σ' : ℝ
hσ' : 1 < σ'
n : ℕ
h : ¬n = 0
⊢ Complex.abs (f n) / ↑n ^ σ' ≤ Complex.abs (f n) / ↑n
Tactic:
have : 1 ≤ (n : ℝ) := by simpa using Nat.pos_iff_ne_zero.mpr h
State after:
case neg
n✝ : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this✝ : 0 ≤ C
σ' : ℝ
hσ' : 1 < σ'
n : ℕ
h : ¬n = 0
this : 1 ≤ ↑n
⊢ Complex.abs (f n) / ↑n ^ σ' ≤ Complex.abs (f n) / ↑n

State before:
case neg
n✝ : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this✝ : 0 ≤ C
σ' : ℝ
hσ' : 1 < σ'
n : ℕ
h : ¬n = 0
this : 1 ≤ ↑n
⊢ Complex.abs (f n) / ↑n ^ σ' ≤ Complex.abs (f n) / ↑n
Tactic:
refine div_le_div (by simp only [apply_nonneg]) le_rfl (by simpa [Nat.pos_iff_ne_zero]) ?_
State after:
case neg
n✝ : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this✝ : 0 ≤ C
σ' : ℝ
hσ' : 1 < σ'
n : ℕ
h : ¬n = 0
this : 1 ≤ ↑n
⊢ ↑n ≤ ↑n ^ σ'

State before:
case neg
n✝ : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this✝ : 0 ≤ C
σ' : ℝ
hσ' : 1 < σ'
n : ℕ
h : ¬n = 0
this : 1 ≤ ↑n
⊢ ↑n ≤ ↑n ^ σ'
Tactic:
simpa using Real.rpow_le_rpow_of_exponent_le this hσ'.le
State after:
no goals

State before:
n✝ : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this : 0 ≤ C
σ' : ℝ
hσ' : 1 < σ'
n : ℕ
h : ¬n = 0
⊢ 1 ≤ ↑n
Tactic:
simpa using Nat.pos_iff_ne_zero.mpr h
State after:
no goals

State before:
n✝ : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this✝ : 0 ≤ C
σ' : ℝ
hσ' : 1 < σ'
n : ℕ
h : ¬n = 0
this : 1 ≤ ↑n
⊢ 0 ≤ Complex.abs (f n)
Tactic:
simp only [apply_nonneg]
State after:
no goals

State before:
n✝ : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this✝ : 0 ≤ C
σ' : ℝ
hσ' : 1 < σ'
n : ℕ
h : ¬n = 0
this : 1 ≤ ↑n
⊢ 0 < ↑n
Tactic:
simpa [Nat.pos_iff_ne_zero]
State after:
no goals