internlm/Lean-Github huggingface dataset:
Theorem: limiting_fourier_lim1
Proof 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 => ?_) ?_
Proof 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))
Theorem: limiting_fourier_lim1
Proof 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)
Proof state after:
no goals
Theorem: limiting_fourier_lim1
Proof 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
Proof 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))
Theorem: limiting_fourier_lim1
Proof 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]
Proof 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))
Theorem: limiting_fourier_lim1
Proof 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])
Proof 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)
Theorem: limiting_fourier_lim1
Proof 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
Proof state after:
no goals
Theorem: limiting_fourier_lim1
Proof 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]
Proof state after:
no goals
Theorem: limiting_fourier_lim1
Proof 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]
Proof 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))
Theorem: limiting_fourier_lim1
Proof 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
Proof 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))
Theorem: limiting_fourier_lim1
Proof 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
Proof 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))
Theorem: limiting_fourier_lim1
Proof 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]
Proof 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))
Theorem: limiting_fourier_lim1
Proof 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 _))
Proof 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
Theorem: limiting_fourier_lim1
Proof 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]
Proof 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
Theorem: limiting_fourier_lim1
Proof 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
Proof 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
Theorem: limiting_fourier_lim1
Proof 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]) ?_
Proof 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 ^ σ'
Theorem: limiting_fourier_lim1
Proof 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
Proof state after:
no goals
Theorem: limiting_fourier_lim1
Proof 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
Proof state after:
no goals
Theorem: limiting_fourier_lim1
Proof 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]
Proof state after:
no goals
Theorem: limiting_fourier_lim1
Proof 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]
Proof state after:
no goals
Theorem: limiting_fourier_lim2_aux
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x C : ℝ
⊢ Integrable (fun t => |x| * (C / (1 + (t / (2 * π)) ^ 2))) (volume.restrict (Ici (-x.log)))
Tactic:
simp_rw [div_eq_mul_inv C]
Proof state after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x C : ℝ
⊢ Integrable (fun t => |x| * (C * (1 + (t / (2 * π)) ^ 2)⁻¹)) (volume.restrict (Ici (-x.log)))
Theorem: limiting_fourier_lim2_aux
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x C : ℝ
⊢ Integrable (fun t => |x| * (C * (1 + (t / (2 * π)) ^ 2)⁻¹)) (volume.restrict (Ici (-x.log)))
Tactic:
exact (((integrable_inv_one_add_sq.comp_div (by simp [pi_ne_zero])).const_mul _).const_mul _).restrict
Proof state after:
no goals
Theorem: limiting_fourier_lim2_aux
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x C : ℝ
⊢ 2 * π ≠ 0
Tactic:
simp [pi_ne_zero]
Proof state after:
no goals
Theorem: limiting_fourier_lim2
Proof state before:
n : ℕ
A✝ a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
A : ℝ
ψ : W21
hx : 1 ≤ x
⊢ Tendsto
    (fun σ' => ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)))
    (𝓝[>] 1) (𝓝 (↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))))
Tactic:
obtain ⟨C, hC⟩ := decay_bounds_cor ψ
Proof state after:
case intro
n : ℕ
A✝ a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
A : ℝ
ψ : W21
hx : 1 ≤ x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
⊢ Tendsto
    (fun σ' => ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)))
    (𝓝[>] 1) (𝓝 (↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))))
Theorem: limiting_fourier_lim2
Proof state before:
case intro
n : ℕ
A✝ a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
A : ℝ
ψ : W21
hx : 1 ≤ x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
⊢ Tendsto
    (fun σ' => ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)))
    (𝓝[>] 1) (𝓝 (↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))))
Tactic:
apply Tendsto.mul
Proof state after:
case intro.hf
n : ℕ
A✝ a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
A : ℝ
ψ : W21
hx : 1 ≤ x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
⊢ Tendsto (fun x_1 => ↑A * ↑(x ^ (1 - x_1))) (𝓝[>] 1) (𝓝 ↑A)

case intro.hg
n : ℕ
A✝ a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
A : ℝ
ψ : W21
hx : 1 ≤ x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
⊢ Tendsto (fun x_1 => ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (x_1 - 1))) * 𝓕 ψ.toFun (u / (2 * π))) (𝓝[>] 1)
    (𝓝 (∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))))
Theorem: limiting_fourier_lim2
Proof state before:
case intro.hf
n : ℕ
A✝ a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
A : ℝ
ψ : W21
hx : 1 ≤ x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
⊢ Tendsto (fun x_1 => ↑A * ↑(x ^ (1 - x_1))) (𝓝[>] 1) (𝓝 ↑A)
Tactic:
suffices h : Tendsto (fun σ' : ℝ ↦ ofReal' (x ^ (1 - σ'))) (𝓝[>] 1) (𝓝 1) by simpa using h.const_mul ↑A
Proof state after:
case intro.hf
n : ℕ
A✝ a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
A : ℝ
ψ : W21
hx : 1 ≤ x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
⊢ Tendsto (fun σ' => ↑(x ^ (1 - σ'))) (𝓝[>] 1) (𝓝 1)
Theorem: limiting_fourier_lim2
Proof state before:
case intro.hf
n : ℕ
A✝ a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
A : ℝ
ψ : W21
hx : 1 ≤ x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
⊢ Tendsto (fun σ' => ↑(x ^ (1 - σ'))) (𝓝[>] 1) (𝓝 1)
Tactic:
suffices h : Tendsto (fun σ' : ℝ ↦ x ^ (1 - σ')) (𝓝[>] 1) (𝓝 1) from (continuous_ofReal.tendsto 1).comp h
Proof state after:
case intro.hf
n : ℕ
A✝ a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
A : ℝ
ψ : W21
hx : 1 ≤ x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
⊢ Tendsto (fun σ' => x ^ (1 - σ')) (𝓝[>] 1) (𝓝 1)
Theorem: limiting_fourier_lim2
Proof state before:
case intro.hf
n : ℕ
A✝ a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
A : ℝ
ψ : W21
hx : 1 ≤ x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
⊢ Tendsto (fun σ' => x ^ (1 - σ')) (𝓝[>] 1) (𝓝 1)
Tactic:
have : Tendsto (fun σ' : ℝ ↦ σ') (𝓝 1) (𝓝 1) := fun _ a ↦ a
Proof state after:
case intro.hf
n : ℕ
A✝ a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
A : ℝ
ψ : W21
hx : 1 ≤ x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this : Tendsto (fun σ' => σ') (𝓝 1) (𝓝 1)
⊢ Tendsto (fun σ' => x ^ (1 - σ')) (𝓝[>] 1) (𝓝 1)
Theorem: limiting_fourier_lim2
Proof state before:
case intro.hf
n : ℕ
A✝ a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
A : ℝ
ψ : W21
hx : 1 ≤ x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this : Tendsto (fun σ' => σ') (𝓝 1) (𝓝 1)
⊢ Tendsto (fun σ' => x ^ (1 - σ')) (𝓝[>] 1) (𝓝 1)
Tactic:
have : Tendsto (fun σ' : ℝ ↦ 1 - σ') (𝓝[>] 1) (𝓝 0) :=
  tendsto_nhdsWithin_of_tendsto_nhds (by simpa using this.const_sub 1)
Proof state after:
case intro.hf
n : ℕ
A✝ a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
A : ℝ
ψ : W21
hx : 1 ≤ x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this✝ : Tendsto (fun σ' => σ') (𝓝 1) (𝓝 1)
this : Tendsto (fun σ' => 1 - σ') (𝓝[>] 1) (𝓝 0)
⊢ Tendsto (fun σ' => x ^ (1 - σ')) (𝓝[>] 1) (𝓝 1)
Theorem: limiting_fourier_lim2
Proof state before:
case intro.hf
n : ℕ
A✝ a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
A : ℝ
ψ : W21
hx : 1 ≤ x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this✝ : Tendsto (fun σ' => σ') (𝓝 1) (𝓝 1)
this : Tendsto (fun σ' => 1 - σ') (𝓝[>] 1) (𝓝 0)
⊢ Tendsto (fun σ' => x ^ (1 - σ')) (𝓝[>] 1) (𝓝 1)
Tactic:
simpa using tendsto_const_nhds.rpow this (Or.inl (zero_lt_one.trans_le hx).ne.symm)
Proof state after:
no goals
Theorem: limiting_fourier_lim2
Proof state before:
n : ℕ
A✝ a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
A : ℝ
ψ : W21
hx : 1 ≤ x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
h : Tendsto (fun σ' => ↑(x ^ (1 - σ'))) (𝓝[>] 1) (𝓝 1)
⊢ Tendsto (fun x_1 => ↑A * ↑(x ^ (1 - x_1))) (𝓝[>] 1) (𝓝 ↑A)
Tactic:
simpa using h.const_mul ↑A
Proof state after:
no goals
Theorem: limiting_fourier_lim2
Proof state before:
n : ℕ
A✝ a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
A : ℝ
ψ : W21
hx : 1 ≤ x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this : Tendsto (fun σ' => σ') (𝓝 1) (𝓝 1)
⊢ Tendsto (fun σ' => 1 - σ') (𝓝 1) (𝓝 0)
Tactic:
simpa using this.const_sub 1
Proof state after:
no goals
Theorem: limiting_fourier_lim2
Proof state before:
case intro.hg
n : ℕ
A✝ a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
A : ℝ
ψ : W21
hx : 1 ≤ x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
⊢ Tendsto (fun x_1 => ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (x_1 - 1))) * 𝓕 ψ.toFun (u / (2 * π))) (𝓝[>] 1)
    (𝓝 (∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))))
Tactic:
refine tendsto_integral_filter_of_dominated_convergence _ ?_ ?_ (limiting_fourier_lim2_aux x C) ?_
Proof state after:
case intro.hg.refine_1
n : ℕ
A✝ a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
A : ℝ
ψ : W21
hx : 1 ≤ x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
⊢ ∀ᶠ (n : ℝ) in 𝓝[>] 1,
    AEStronglyMeasurable (fun u => ↑(rexp (-u * (n - 1))) * 𝓕 ψ.toFun (u / (2 * π))) (volume.restrict (Ici (-x.log)))

case intro.hg.refine_2
n : ℕ
A✝ a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
A : ℝ
ψ : W21
hx : 1 ≤ x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
⊢ ∀ᶠ (n : ℝ) in 𝓝[>] 1,
    ∀ᵐ (a : ℝ) ∂volume.restrict (Ici (-x.log)),
      ‖↑(rexp (-a * (n - 1))) * 𝓕 ψ.toFun (a / (2 * π))‖ ≤ |x| * (C / (1 + (a / (2 * π)) ^ 2))

case intro.hg.refine_3
n : ℕ
A✝ a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
A : ℝ
ψ : W21
hx : 1 ≤ x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ici (-x.log)),
    Tendsto (fun n => ↑(rexp (-a * (n - 1))) * 𝓕 ψ.toFun (a / (2 * π))) (𝓝[>] 1) (𝓝 (𝓕 ψ.toFun (a / (2 * π))))
Theorem: limiting_fourier_lim2
Proof state before:
case intro.hg.refine_1
n : ℕ
A✝ a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
A : ℝ
ψ : W21
hx : 1 ≤ x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
⊢ ∀ᶠ (n : ℝ) in 𝓝[>] 1,
    AEStronglyMeasurable (fun u => ↑(rexp (-u * (n - 1))) * 𝓕 ψ.toFun (u / (2 * π))) (volume.restrict (Ici (-x.log)))
Tactic:
apply eventually_of_forall
Proof state after:
case intro.hg.refine_1.hp
n : ℕ
A✝ a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
A : ℝ
ψ : W21
hx : 1 ≤ x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
⊢ ∀ (x_1 : ℝ),
    AEStronglyMeasurable (fun u => ↑(rexp (-u * (x_1 - 1))) * 𝓕 ψ.toFun (u / (2 * π))) (volume.restrict (Ici (-x.log)))
Theorem: limiting_fourier_lim2
Proof state before:
case intro.hg.refine_1.hp
n : ℕ
A✝ a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
A : ℝ
ψ : W21
hx : 1 ≤ x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
⊢ ∀ (x_1 : ℝ),
    AEStronglyMeasurable (fun u => ↑(rexp (-u * (x_1 - 1))) * 𝓕 ψ.toFun (u / (2 * π))) (volume.restrict (Ici (-x.log)))
Tactic:
intro σ'
Proof state after:
case intro.hg.refine_1.hp
n : ℕ
A✝ a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
A : ℝ
ψ : W21
hx : 1 ≤ x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
σ' : ℝ
⊢ AEStronglyMeasurable (fun u => ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π))) (volume.restrict (Ici (-x.log)))
Theorem: limiting_fourier_lim2
Proof state before:
case intro.hg.refine_1.hp
n : ℕ
A✝ a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
A : ℝ
ψ : W21
hx : 1 ≤ x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
σ' : ℝ
⊢ AEStronglyMeasurable (fun u => ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π))) (volume.restrict (Ici (-x.log)))
Tactic:
apply Continuous.aestronglyMeasurable
Proof state after:
case intro.hg.refine_1.hp.hf
n : ℕ
A✝ a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
A : ℝ
ψ : W21
hx : 1 ≤ x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
σ' : ℝ
⊢ Continuous fun u => ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π))