Theorem: limiting_fourier_lim2 (PrimeNumberTheoremAnd/Wiener.lean)

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 ψ
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 * π))))

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
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 * π))))

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
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)

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
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)

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
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)

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)
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)

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)
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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) ?_
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 * π))))

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
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)))

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 σ'
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)))

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
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 * π))

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 ψ
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 * π))

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
State after:
no goals

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)
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))

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
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

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
State after:
no goals

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⟩
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))

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]
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))

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
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))

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)
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))

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]
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))

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 _)
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|

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]
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|

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)
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|

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
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|

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
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|

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
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|

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
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|

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
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|

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
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|

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
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|

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)]
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
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 * π))))

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
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 * π))))

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 _
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)

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
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)

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
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)))

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
State after:
no goals

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 _
State after:
no goals

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
State after:
no goals