internlm/Lean-Github huggingface dataset:
Theorem: limiting_fourier_lim2
Proof state before:
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 * π))
Tactic:
have := continuous_FourierIntegral ψ
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)
σ' : ℝ
this : Continuous (𝓕 ψ.toFun)
⊢ Continuous fun u => ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π))
Theorem: limiting_fourier_lim2
Proof state before:
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)
σ' : ℝ
this : Continuous (𝓕 ψ.toFun)
⊢ Continuous fun u => ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π))
Tactic:
continuity
Proof state after:
no goals
Theorem: limiting_fourier_lim2
Proof state before:
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))
Tactic:
apply eventually_of_mem (U := Ioo 1 2)
Proof state after:
case intro.hg.refine_2.hU
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)
⊢ Ioo 1 2 ∈ 𝓝[>] 1

case intro.hg.refine_2.h
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 ∈ Ioo 1 2,
    ∀ᵐ (a : ℝ) ∂volume.restrict (Ici (-x.log)),
      ‖↑(rexp (-a * (x_1 - 1))) * 𝓕 ψ.toFun (a / (2 * π))‖ ≤ |x| * (C / (1 + (a / (2 * π)) ^ 2))
Theorem: limiting_fourier_lim2
Proof state before:
case intro.hg.refine_2.hU
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)
⊢ Ioo 1 2 ∈ 𝓝[>] 1
Tactic:
apply Ioo_mem_nhdsWithin_Ioi
Proof state after:
case intro.hg.refine_2.hU.H
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)
⊢ 1 ∈ Ico 1 2
Theorem: limiting_fourier_lim2
Proof state before:
case intro.hg.refine_2.hU.H
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)
⊢ 1 ∈ Ico 1 2
Tactic:
simp
Proof state after:
no goals
Theorem: limiting_fourier_lim2
Proof state before:
case intro.hg.refine_2.h
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 ∈ Ioo 1 2,
    ∀ᵐ (a : ℝ) ∂volume.restrict (Ici (-x.log)),
      ‖↑(rexp (-a * (x_1 - 1))) * 𝓕 ψ.toFun (a / (2 * π))‖ ≤ |x| * (C / (1 + (a / (2 * π)) ^ 2))
Tactic:
intro σ' ⟨h1, h2⟩
Proof state after:
case intro.hg.refine_2.h
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)
σ' : ℝ
h1 : 1 < σ'
h2 : σ' < 2
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ici (-x.log)),
    ‖↑(rexp (-a * (σ' - 1))) * 𝓕 ψ.toFun (a / (2 * π))‖ ≤ |x| * (C / (1 + (a / (2 * π)) ^ 2))
Theorem: limiting_fourier_lim2
Proof state before:
case intro.hg.refine_2.h
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)
σ' : ℝ
h1 : 1 < σ'
h2 : σ' < 2
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ici (-x.log)),
    ‖↑(rexp (-a * (σ' - 1))) * 𝓕 ψ.toFun (a / (2 * π))‖ ≤ |x| * (C / (1 + (a / (2 * π)) ^ 2))
Tactic:
rw [ae_restrict_iff' measurableSet_Ici]
Proof state after:
case intro.hg.refine_2.h
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)
σ' : ℝ
h1 : 1 < σ'
h2 : σ' < 2
⊢ ∀ᵐ (x_1 : ℝ),
    x_1 ∈ Ici (-x.log) → ‖↑(rexp (-x_1 * (σ' - 1))) * 𝓕 ψ.toFun (x_1 / (2 * π))‖ ≤ |x| * (C / (1 + (x_1 / (2 * π)) ^ 2))
Theorem: limiting_fourier_lim2
Proof state before:
case intro.hg.refine_2.h
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)
σ' : ℝ
h1 : 1 < σ'
h2 : σ' < 2
⊢ ∀ᵐ (x_1 : ℝ),
    x_1 ∈ Ici (-x.log) → ‖↑(rexp (-x_1 * (σ' - 1))) * 𝓕 ψ.toFun (x_1 / (2 * π))‖ ≤ |x| * (C / (1 + (x_1 / (2 * π)) ^ 2))
Tactic:
apply eventually_of_forall
Proof state after:
case intro.hg.refine_2.h.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)
σ' : ℝ
h1 : 1 < σ'
h2 : σ' < 2
⊢ ∀ x_1 ∈ Ici (-x.log), ‖↑(rexp (-x_1 * (σ' - 1))) * 𝓕 ψ.toFun (x_1 / (2 * π))‖ ≤ |x| * (C / (1 + (x_1 / (2 * π)) ^ 2))
Theorem: limiting_fourier_lim2
Proof state before:
case intro.hg.refine_2.h.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)
σ' : ℝ
h1 : 1 < σ'
h2 : σ' < 2
⊢ ∀ x_1 ∈ Ici (-x.log), ‖↑(rexp (-x_1 * (σ' - 1))) * 𝓕 ψ.toFun (x_1 / (2 * π))‖ ≤ |x| * (C / (1 + (x_1 / (2 * π)) ^ 2))
Tactic:
intro t (ht : - Real.log x ≤ t)
Proof state after:
case intro.hg.refine_2.h.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)
σ' : ℝ
h1 : 1 < σ'
h2 : σ' < 2
t : ℝ
ht : -x.log ≤ t
⊢ ‖↑(rexp (-t * (σ' - 1))) * 𝓕 ψ.toFun (t / (2 * π))‖ ≤ |x| * (C / (1 + (t / (2 * π)) ^ 2))
Theorem: limiting_fourier_lim2
Proof state before:
case intro.hg.refine_2.h.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)
σ' : ℝ
h1 : 1 < σ'
h2 : σ' < 2
t : ℝ
ht : -x.log ≤ t
⊢ ‖↑(rexp (-t * (σ' - 1))) * 𝓕 ψ.toFun (t / (2 * π))‖ ≤ |x| * (C / (1 + (t / (2 * π)) ^ 2))
Tactic:
rw [norm_mul]
Proof state after:
case intro.hg.refine_2.h.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)
σ' : ℝ
h1 : 1 < σ'
h2 : σ' < 2
t : ℝ
ht : -x.log ≤ t
⊢ ‖↑(rexp (-t * (σ' - 1)))‖ * ‖𝓕 ψ.toFun (t / (2 * π))‖ ≤ |x| * (C / (1 + (t / (2 * π)) ^ 2))
Theorem: limiting_fourier_lim2
Proof state before:
case intro.hg.refine_2.h.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)
σ' : ℝ
h1 : 1 < σ'
h2 : σ' < 2
t : ℝ
ht : -x.log ≤ t
⊢ ‖↑(rexp (-t * (σ' - 1)))‖ * ‖𝓕 ψ.toFun (t / (2 * π))‖ ≤ |x| * (C / (1 + (t / (2 * π)) ^ 2))
Tactic:
refine mul_le_mul ?_ (hC _) (norm_nonneg _) (abs_nonneg _)
Proof state after:
case intro.hg.refine_2.h.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)
σ' : ℝ
h1 : 1 < σ'
h2 : σ' < 2
t : ℝ
ht : -x.log ≤ t
⊢ ‖↑(rexp (-t * (σ' - 1)))‖ ≤ |x|
Theorem: limiting_fourier_lim2
Proof state before:
case intro.hg.refine_2.h.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)
σ' : ℝ
h1 : 1 < σ'
h2 : σ' < 2
t : ℝ
ht : -x.log ≤ t
⊢ ‖↑(rexp (-t * (σ' - 1)))‖ ≤ |x|
Tactic:
simp [Complex.abs_exp]
Proof state after:
case intro.hg.refine_2.h.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)
σ' : ℝ
h1 : 1 < σ'
h2 : σ' < 2
t : ℝ
ht : -x.log ≤ t
⊢ rexp (-(t * (σ' - 1))) ≤ |x|
Theorem: limiting_fourier_lim2
Proof state before:
case intro.hg.refine_2.h.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)
σ' : ℝ
h1 : 1 < σ'
h2 : σ' < 2
t : ℝ
ht : -x.log ≤ t
⊢ rexp (-(t * (σ' - 1))) ≤ |x|
Tactic:
have : -Real.log x * (σ' - 1) ≤ t * (σ' - 1) := mul_le_mul_of_nonneg_right ht (by linarith)
Proof state after:
case intro.hg.refine_2.h.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)
σ' : ℝ
h1 : 1 < σ'
h2 : σ' < 2
t : ℝ
ht : -x.log ≤ t
this : -x.log * (σ' - 1) ≤ t * (σ' - 1)
⊢ rexp (-(t * (σ' - 1))) ≤ |x|
Theorem: limiting_fourier_lim2
Proof state before:
case intro.hg.refine_2.h.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)
σ' : ℝ
h1 : 1 < σ'
h2 : σ' < 2
t : ℝ
ht : -x.log ≤ t
this : -x.log * (σ' - 1) ≤ t * (σ' - 1)
⊢ rexp (-(t * (σ' - 1))) ≤ |x|
Tactic:
have : -(t * (σ' - 1)) ≤ Real.log x * (σ' - 1) := by simpa using neg_le_neg this
Proof state after:
case intro.hg.refine_2.h.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)
σ' : ℝ
h1 : 1 < σ'
h2 : σ' < 2
t : ℝ
ht : -x.log ≤ t
this✝ : -x.log * (σ' - 1) ≤ t * (σ' - 1)
this : -(t * (σ' - 1)) ≤ x.log * (σ' - 1)
⊢ rexp (-(t * (σ' - 1))) ≤ |x|
Theorem: limiting_fourier_lim2
Proof state before:
case intro.hg.refine_2.h.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)
σ' : ℝ
h1 : 1 < σ'
h2 : σ' < 2
t : ℝ
ht : -x.log ≤ t
this✝ : -x.log * (σ' - 1) ≤ t * (σ' - 1)
this : -(t * (σ' - 1)) ≤ x.log * (σ' - 1)
⊢ rexp (-(t * (σ' - 1))) ≤ |x|
Tactic:
have := Real.exp_monotone this
Proof state after:
case intro.hg.refine_2.h.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)
σ' : ℝ
h1 : 1 < σ'
h2 : σ' < 2
t : ℝ
ht : -x.log ≤ t
this✝¹ : -x.log * (σ' - 1) ≤ t * (σ' - 1)
this✝ : -(t * (σ' - 1)) ≤ x.log * (σ' - 1)
this : rexp (-(t * (σ' - 1))) ≤ rexp (x.log * (σ' - 1))
⊢ rexp (-(t * (σ' - 1))) ≤ |x|
Theorem: limiting_fourier_lim2
Proof state before:
case intro.hg.refine_2.h.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)
σ' : ℝ
h1 : 1 < σ'
h2 : σ' < 2
t : ℝ
ht : -x.log ≤ t
this✝¹ : -x.log * (σ' - 1) ≤ t * (σ' - 1)
this✝ : -(t * (σ' - 1)) ≤ x.log * (σ' - 1)
this : rexp (-(t * (σ' - 1))) ≤ rexp (x.log * (σ' - 1))
⊢ rexp (-(t * (σ' - 1))) ≤ |x|
Tactic:
apply this.trans
Proof state after:
case intro.hg.refine_2.h.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)
σ' : ℝ
h1 : 1 < σ'
h2 : σ' < 2
t : ℝ
ht : -x.log ≤ t
this✝¹ : -x.log * (σ' - 1) ≤ t * (σ' - 1)
this✝ : -(t * (σ' - 1)) ≤ x.log * (σ' - 1)
this : rexp (-(t * (σ' - 1))) ≤ rexp (x.log * (σ' - 1))
⊢ rexp (x.log * (σ' - 1)) ≤ |x|
Theorem: limiting_fourier_lim2
Proof state before:
case intro.hg.refine_2.h.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)
σ' : ℝ
h1 : 1 < σ'
h2 : σ' < 2
t : ℝ
ht : -x.log ≤ t
this✝¹ : -x.log * (σ' - 1) ≤ t * (σ' - 1)
this✝ : -(t * (σ' - 1)) ≤ x.log * (σ' - 1)
this : rexp (-(t * (σ' - 1))) ≤ rexp (x.log * (σ' - 1))
⊢ rexp (x.log * (σ' - 1)) ≤ |x|
Tactic:
have l1 : σ' - 1 ≤ 1 := by linarith
Proof state after:
case intro.hg.refine_2.h.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)
σ' : ℝ
h1 : 1 < σ'
h2 : σ' < 2
t : ℝ
ht : -x.log ≤ t
this✝¹ : -x.log * (σ' - 1) ≤ t * (σ' - 1)
this✝ : -(t * (σ' - 1)) ≤ x.log * (σ' - 1)
this : rexp (-(t * (σ' - 1))) ≤ rexp (x.log * (σ' - 1))
l1 : σ' - 1 ≤ 1
⊢ rexp (x.log * (σ' - 1)) ≤ |x|
Theorem: limiting_fourier_lim2
Proof state before:
case intro.hg.refine_2.h.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)
σ' : ℝ
h1 : 1 < σ'
h2 : σ' < 2
t : ℝ
ht : -x.log ≤ t
this✝¹ : -x.log * (σ' - 1) ≤ t * (σ' - 1)
this✝ : -(t * (σ' - 1)) ≤ x.log * (σ' - 1)
this : rexp (-(t * (σ' - 1))) ≤ rexp (x.log * (σ' - 1))
l1 : σ' - 1 ≤ 1
⊢ rexp (x.log * (σ' - 1)) ≤ |x|
Tactic:
have : 0 ≤ Real.log x := Real.log_nonneg hx
Proof state after:
case intro.hg.refine_2.h.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)
σ' : ℝ
h1 : 1 < σ'
h2 : σ' < 2
t : ℝ
ht : -x.log ≤ t
this✝² : -x.log * (σ' - 1) ≤ t * (σ' - 1)
this✝¹ : -(t * (σ' - 1)) ≤ x.log * (σ' - 1)
this✝ : rexp (-(t * (σ' - 1))) ≤ rexp (x.log * (σ' - 1))
l1 : σ' - 1 ≤ 1
this : 0 ≤ x.log
⊢ rexp (x.log * (σ' - 1)) ≤ |x|
Theorem: limiting_fourier_lim2
Proof state before:
case intro.hg.refine_2.h.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)
σ' : ℝ
h1 : 1 < σ'
h2 : σ' < 2
t : ℝ
ht : -x.log ≤ t
this✝² : -x.log * (σ' - 1) ≤ t * (σ' - 1)
this✝¹ : -(t * (σ' - 1)) ≤ x.log * (σ' - 1)
this✝ : rexp (-(t * (σ' - 1))) ≤ rexp (x.log * (σ' - 1))
l1 : σ' - 1 ≤ 1
this : 0 ≤ x.log
⊢ rexp (x.log * (σ' - 1)) ≤ |x|
Tactic:
have := mul_le_mul_of_nonneg_left l1 this
Proof state after:
case intro.hg.refine_2.h.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)
σ' : ℝ
h1 : 1 < σ'
h2 : σ' < 2
t : ℝ
ht : -x.log ≤ t
this✝³ : -x.log * (σ' - 1) ≤ t * (σ' - 1)
this✝² : -(t * (σ' - 1)) ≤ x.log * (σ' - 1)
this✝¹ : rexp (-(t * (σ' - 1))) ≤ rexp (x.log * (σ' - 1))
l1 : σ' - 1 ≤ 1
this✝ : 0 ≤ x.log
this : x.log * (σ' - 1) ≤ x.log * 1
⊢ rexp (x.log * (σ' - 1)) ≤ |x|
Theorem: limiting_fourier_lim2
Proof state before:
case intro.hg.refine_2.h.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)
σ' : ℝ
h1 : 1 < σ'
h2 : σ' < 2
t : ℝ
ht : -x.log ≤ t
this✝³ : -x.log * (σ' - 1) ≤ t * (σ' - 1)
this✝² : -(t * (σ' - 1)) ≤ x.log * (σ' - 1)
this✝¹ : rexp (-(t * (σ' - 1))) ≤ rexp (x.log * (σ' - 1))
l1 : σ' - 1 ≤ 1
this✝ : 0 ≤ x.log
this : x.log * (σ' - 1) ≤ x.log * 1
⊢ rexp (x.log * (σ' - 1)) ≤ |x|
Tactic:
apply (Real.exp_monotone this).trans
Proof state after:
case intro.hg.refine_2.h.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)
σ' : ℝ
h1 : 1 < σ'
h2 : σ' < 2
t : ℝ
ht : -x.log ≤ t
this✝³ : -x.log * (σ' - 1) ≤ t * (σ' - 1)
this✝² : -(t * (σ' - 1)) ≤ x.log * (σ' - 1)
this✝¹ : rexp (-(t * (σ' - 1))) ≤ rexp (x.log * (σ' - 1))
l1 : σ' - 1 ≤ 1
this✝ : 0 ≤ x.log
this : x.log * (σ' - 1) ≤ x.log * 1
⊢ rexp (x.log * 1) ≤ |x|
Theorem: limiting_fourier_lim2
Proof state before:
case intro.hg.refine_2.h.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)
σ' : ℝ
h1 : 1 < σ'
h2 : σ' < 2
t : ℝ
ht : -x.log ≤ t
this✝³ : -x.log * (σ' - 1) ≤ t * (σ' - 1)
this✝² : -(t * (σ' - 1)) ≤ x.log * (σ' - 1)
this✝¹ : rexp (-(t * (σ' - 1))) ≤ rexp (x.log * (σ' - 1))
l1 : σ' - 1 ≤ 1
this✝ : 0 ≤ x.log
this : x.log * (σ' - 1) ≤ x.log * 1
⊢ rexp (x.log * 1) ≤ |x|
Tactic:
simp [Real.exp_log (zero_lt_one.trans_le hx), abs_eq_self.mpr (zero_le_one.trans hx)]
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)
σ' : ℝ
h1 : 1 < σ'
h2 : σ' < 2
t : ℝ
ht : -x.log ≤ t
⊢ 0 ≤ σ' - 1
Tactic:
linarith
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)
σ' : ℝ
h1 : 1 < σ'
h2 : σ' < 2
t : ℝ
ht : -x.log ≤ t
this : -x.log * (σ' - 1) ≤ t * (σ' - 1)
⊢ -(t * (σ' - 1)) ≤ x.log * (σ' - 1)
Tactic:
simpa using neg_le_neg this
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)
σ' : ℝ
h1 : 1 < σ'
h2 : σ' < 2
t : ℝ
ht : -x.log ≤ t
this✝¹ : -x.log * (σ' - 1) ≤ t * (σ' - 1)
this✝ : -(t * (σ' - 1)) ≤ x.log * (σ' - 1)
this : rexp (-(t * (σ' - 1))) ≤ rexp (x.log * (σ' - 1))
⊢ σ' - 1 ≤ 1
Tactic:
linarith
Proof state after:
no goals
Theorem: limiting_fourier_lim2
Proof state before:
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 * π))))
Tactic:
apply eventually_of_forall
Proof state after:
case intro.hg.refine_3.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 : ℝ), Tendsto (fun n => ↑(rexp (-x * (n - 1))) * 𝓕 ψ.toFun (x / (2 * π))) (𝓝[>] 1) (𝓝 (𝓕 ψ.toFun (x / (2 * π))))
Theorem: limiting_fourier_lim2
Proof state before:
case intro.hg.refine_3.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 : ℝ), Tendsto (fun n => ↑(rexp (-x * (n - 1))) * 𝓕 ψ.toFun (x / (2 * π))) (𝓝[>] 1) (𝓝 (𝓕 ψ.toFun (x / (2 * π))))
Tactic:
intro x
Proof state after:
case intro.hg.refine_3.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 : ℝ
⊢ Tendsto (fun n => ↑(rexp (-x * (n - 1))) * 𝓕 ψ.toFun (x / (2 * π))) (𝓝[>] 1) (𝓝 (𝓕 ψ.toFun (x / (2 * π))))
Theorem: limiting_fourier_lim2
Proof state before:
case intro.hg.refine_3.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 : ℝ
⊢ Tendsto (fun n => ↑(rexp (-x * (n - 1))) * 𝓕 ψ.toFun (x / (2 * π))) (𝓝[>] 1) (𝓝 (𝓕 ψ.toFun (x / (2 * π))))
Tactic:
suffices h : Tendsto (fun n ↦ ((rexp (-x * (n - 1))) : ℂ)) (𝓝[>] 1) (𝓝 1) by simpa using h.mul_const _
Proof state after:
case intro.hg.refine_3.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 : ℝ
⊢ Tendsto (fun n => ↑(rexp (-x * (n - 1)))) (𝓝[>] 1) (𝓝 1)
Theorem: limiting_fourier_lim2
Proof state before:
case intro.hg.refine_3.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 : ℝ
⊢ Tendsto (fun n => ↑(rexp (-x * (n - 1)))) (𝓝[>] 1) (𝓝 1)
Tactic:
apply Tendsto.mono_left ?_ nhdsWithin_le_nhds
Proof state after:
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 : ℝ
⊢ Tendsto (fun n => ↑(rexp (-x * (n - 1)))) (𝓝 1) (𝓝 1)
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)
x : ℝ
⊢ Tendsto (fun n => ↑(rexp (-x * (n - 1)))) (𝓝 1) (𝓝 1)
Tactic:
suffices h : Continuous (fun n ↦ ((rexp (-x * (n - 1))) : ℂ)) by simpa using h.tendsto 1
Proof state after:
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 : ℝ
⊢ Continuous fun n => ↑(rexp (-x * (n - 1)))
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)
x : ℝ
⊢ Continuous fun n => ↑(rexp (-x * (n - 1)))
Tactic:
continuity
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)
x : ℝ
h : Tendsto (fun n => ↑(rexp (-x * (n - 1)))) (𝓝[>] 1) (𝓝 1)
⊢ Tendsto (fun n => ↑(rexp (-x * (n - 1))) * 𝓕 ψ.toFun (x / (2 * π))) (𝓝[>] 1) (𝓝 (𝓕 ψ.toFun (x / (2 * π))))
Tactic:
simpa using h.mul_const _
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)
x : ℝ
h : Continuous fun n => ↑(rexp (-x * (n - 1)))
⊢ Tendsto (fun n => ↑(rexp (-x * (n - 1)))) (𝓝 1) (𝓝 1)
Tactic:
simpa using h.tendsto 1
Proof state after:
no goals
Theorem: limiting_fourier_lim3
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
⊢ Tendsto (fun σ' => ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) (𝓝[>] 1)
    (𝓝 (∫ (t : ℝ), G (1 + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)))
Tactic:
by_cases hh : tsupport ψ = ∅
Proof state after:
case pos
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : tsupport ψ.toFun = ∅
⊢ Tendsto (fun σ' => ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) (𝓝[>] 1)
    (𝓝 (∫ (t : ℝ), G (1 + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)))

case neg
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
⊢ Tendsto (fun σ' => ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) (𝓝[>] 1)
    (𝓝 (∫ (t : ℝ), G (1 + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)))