Theorem: second_fourier (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a b c d u x✝ y t σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
⊢ ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ (u / (2 * π)) =
    ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ t * ↑x ^ (↑t * I)
Tactic:
conv in ↑(rexp _) * _ => { rw [Real.fourierIntegral_real_eq, ← smul_eq_mul, ← integral_smul] }
State after:
n : ℕ
A a b c d u x✝ y t σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
⊢ ∫ (u : ℝ) in Ici (-x.log), ∫ (a : ℝ), ↑(rexp (-u * (σ' - 1))) • 𝐞 (-(a * (u / (2 * π)))) • ψ a =
    ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ t * ↑x ^ (↑t * I)

State before:
n : ℕ
A a b c d u x✝ y t σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
⊢ ∫ (u : ℝ) in Ici (-x.log), ∫ (a : ℝ), ↑(rexp (-u * (σ' - 1))) • 𝐞 (-(a * (u / (2 * π)))) • ψ a =
    ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ t * ↑x ^ (↑t * I)
Tactic:
rw [MeasureTheory.integral_integral_swap]
State after:
n : ℕ
A a b c d u x✝ y t σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
⊢ ∫ (y : ℝ), ∫ (x : ℝ) in Ici (-x.log), ↑(rexp (-x * (σ' - 1))) • 𝐞 (-(y * (x / (2 * π)))) • ψ y =
    ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ t * ↑x ^ (↑t * I)

case hf
n : ℕ
A a b c d u x✝ y t σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
⊢ Integrable (Function.uncurry fun u a => ↑(rexp (-u * (σ' - 1))) • 𝐞 (-(a * (u / (2 * π)))) • ψ a)
    ((volume.restrict (Ici (-x.log))).prod volume)

State before:
n : ℕ
A a b c d u x✝ y t σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
⊢ ∫ (y : ℝ), ∫ (x : ℝ) in Ici (-x.log), ↑(rexp (-x * (σ' - 1))) • 𝐞 (-(y * (x / (2 * π)))) • ψ y =
    ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ t * ↑x ^ (↑t * I)

case hf
n : ℕ
A a b c d u x✝ y t σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
⊢ Integrable (Function.uncurry fun u a => ↑(rexp (-u * (σ' - 1))) • 𝐞 (-(a * (u / (2 * π)))) • ψ a)
    ((volume.restrict (Ici (-x.log))).prod volume)
Tactic:
swap
State after:
case hf
n : ℕ
A a b c d u x✝ y t σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
⊢ Integrable (Function.uncurry fun u a => ↑(rexp (-u * (σ' - 1))) • 𝐞 (-(a * (u / (2 * π)))) • ψ a)
    ((volume.restrict (Ici (-x.log))).prod volume)

n : ℕ
A a b c d u x✝ y t σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
⊢ ∫ (y : ℝ), ∫ (x : ℝ) in Ici (-x.log), ↑(rexp (-x * (σ' - 1))) • 𝐞 (-(y * (x / (2 * π)))) • ψ y =
    ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ t * ↑x ^ (↑t * I)

State before:
case hf
n : ℕ
A a b c d u x✝ y t σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
⊢ Integrable (Function.uncurry fun u a => ↑(rexp (-u * (σ' - 1))) • 𝐞 (-(a * (u / (2 * π)))) • ψ a)
    ((volume.restrict (Ici (-x.log))).prod volume)

n : ℕ
A a b c d u x✝ y t σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
⊢ ∫ (y : ℝ), ∫ (x : ℝ) in Ici (-x.log), ↑(rexp (-x * (σ' - 1))) • 𝐞 (-(y * (x / (2 * π)))) • ψ y =
    ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ t * ↑x ^ (↑t * I)
Tactic:
exact second_fourier_integrable_aux1 hcont hsupp hσ
State after:
n : ℕ
A a b c d u x✝ y t σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
⊢ ∫ (y : ℝ), ∫ (x : ℝ) in Ici (-x.log), ↑(rexp (-x * (σ' - 1))) • 𝐞 (-(y * (x / (2 * π)))) • ψ y =
    ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ t * ↑x ^ (↑t * I)

State before:
n : ℕ
A a b c d u x✝ y t σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
⊢ ∫ (y : ℝ), ∫ (x : ℝ) in Ici (-x.log), ↑(rexp (-x * (σ' - 1))) • 𝐞 (-(y * (x / (2 * π)))) • ψ y =
    ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ t * ↑x ^ (↑t * I)
Tactic:
rw [← integral_mul_left]
State after:
n : ℕ
A a b c d u x✝ y t σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
⊢ ∫ (y : ℝ), ∫ (x : ℝ) in Ici (-x.log), ↑(rexp (-x * (σ' - 1))) • 𝐞 (-(y * (x / (2 * π)))) • ψ y =
    ∫ (a : ℝ), ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ a * ↑x ^ (↑a * I))

State before:
n : ℕ
A a b c d u x✝ y t σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
⊢ ∫ (y : ℝ), ∫ (x : ℝ) in Ici (-x.log), ↑(rexp (-x * (σ' - 1))) • 𝐞 (-(y * (x / (2 * π)))) • ψ y =
    ∫ (a : ℝ), ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ a * ↑x ^ (↑a * I))
Tactic:
congr 1
State after:
case e_f
n : ℕ
A a b c d u x✝ y t σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
⊢ (fun y => ∫ (x : ℝ) in Ici (-x.log), ↑(rexp (-x * (σ' - 1))) • 𝐞 (-(y * (x / (2 * π)))) • ψ y) = fun a =>
    ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ a * ↑x ^ (↑a * I))

State before:
case e_f
n : ℕ
A a b c d u x✝ y t σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
⊢ (fun y => ∫ (x : ℝ) in Ici (-x.log), ↑(rexp (-x * (σ' - 1))) • 𝐞 (-(y * (x / (2 * π)))) • ψ y) = fun a =>
    ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ a * ↑x ^ (↑a * I))
Tactic:
ext t
State after:
case e_f.h
n : ℕ
A a b c d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
⊢ ∫ (x : ℝ) in Ici (-x.log), ↑(rexp (-x * (σ' - 1))) • 𝐞 (-(t * (x / (2 * π)))) • ψ t =
    ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1) * ψ t * ↑x ^ (↑t * I))

State before:
case e_f.h
n : ℕ
A a b c d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
⊢ ∫ (x : ℝ) in Ici (-x.log), ↑(rexp (-x * (σ' - 1))) • 𝐞 (-(t * (x / (2 * π)))) • ψ t =
    ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1) * ψ t * ↑x ^ (↑t * I))
Tactic:
dsimp [Real.fourierChar, expMapCircle]
State after:
case e_f.h
n : ℕ
A a b c d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
⊢ ∫ (x : ℝ) in Ici (-x.log), ↑(rexp (-x * (σ' - 1))) * (cexp (↑(2 * π * -(t * (x / (2 * π)))) * I) * ψ t) =
    ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1) * ψ t * ↑x ^ (↑t * I))

State before:
case e_f.h
n : ℕ
A a b c d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
⊢ ∫ (x : ℝ) in Ici (-x.log), ↑(rexp (-x * (σ' - 1))) * (cexp (↑(2 * π * -(t * (x / (2 * π)))) * I) * ψ t) =
    ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1) * ψ t * ↑x ^ (↑t * I))
Tactic:
simp_rw [← mul_assoc _ _ (ψ _), integral_mul_right]
State after:
case e_f.h
n : ℕ
A a b c d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
⊢ (∫ (a : ℝ) in Ici (-x.log), ↑(rexp (-a * (σ' - 1))) * cexp (↑(2 * π * -(t * (a / (2 * π)))) * I)) * ψ t =
    ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1) * ψ t * ↑x ^ (↑t * I))

State before:
case e_f.h
n : ℕ
A a b c d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
⊢ (∫ (a : ℝ) in Ici (-x.log), ↑(rexp (-a * (σ' - 1))) * cexp (↑(2 * π * -(t * (a / (2 * π)))) * I)) * ψ t =
    ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1) * ψ t * ↑x ^ (↑t * I))
Tactic:
rw [fun (a b d : ℂ) ↦ show a * (b * (ψ t) * d) = (a * b * d) * ψ t by ring]
State after:
case e_f.h
n : ℕ
A a b c d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
⊢ (∫ (a : ℝ) in Ici (-x.log), ↑(rexp (-a * (σ' - 1))) * cexp (↑(2 * π * -(t * (a / (2 * π)))) * I)) * ψ t =
    ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1)) * ↑x ^ (↑t * I) * ψ t

State before:
case e_f.h
n : ℕ
A a b c d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
⊢ (∫ (a : ℝ) in Ici (-x.log), ↑(rexp (-a * (σ' - 1))) * cexp (↑(2 * π * -(t * (a / (2 * π)))) * I)) * ψ t =
    ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1)) * ↑x ^ (↑t * I) * ψ t
Tactic:
congr 1
State after:
case e_f.h.e_a
n : ℕ
A a b c d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
⊢ ∫ (a : ℝ) in Ici (-x.log), ↑(rexp (-a * (σ' - 1))) * cexp (↑(2 * π * -(t * (a / (2 * π)))) * I) =
    ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1)) * ↑x ^ (↑t * I)

State before:
case e_f.h.e_a
n : ℕ
A a b c d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
⊢ ∫ (a : ℝ) in Ici (-x.log), ↑(rexp (-a * (σ' - 1))) * cexp (↑(2 * π * -(t * (a / (2 * π)))) * I) =
    ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1)) * ↑x ^ (↑t * I)
Tactic:
push_cast
State after:
case e_f.h.e_a
n : ℕ
A a b c d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
⊢ ∫ (a : ℝ) in Ici (-x.log), cexp (-↑a * (↑σ' - 1)) * cexp (2 * ↑π * -(↑t * (↑a / (2 * ↑π))) * I) =
    ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1)) * ↑x ^ (↑t * I)

State before:
case e_f.h.e_a
n : ℕ
A a b c d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
⊢ ∫ (a : ℝ) in Ici (-x.log), cexp (-↑a * (↑σ' - 1)) * cexp (2 * ↑π * -(↑t * (↑a / (2 * ↑π))) * I) =
    ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1)) * ↑x ^ (↑t * I)
Tactic:
simp_rw [← Complex.exp_add]
State after:
case e_f.h.e_a
n : ℕ
A a b c d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
⊢ ∫ (a : ℝ) in Ici (-x.log), cexp (-↑a * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑a / (2 * ↑π))) * I) =
    ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1)) * ↑x ^ (↑t * I)

State before:
case e_f.h.e_a
n : ℕ
A a b c d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
⊢ ∫ (a : ℝ) in Ici (-x.log), cexp (-↑a * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑a / (2 * ↑π))) * I) =
    ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1)) * ↑x ^ (↑t * I)
Tactic:
have (u : ℝ) :
    -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - σ' - t * I) * u := calc
  _ = -↑u * (↑σ' - 1) + (2 * ↑π) / (2 * ↑π) * -(↑t * ↑u) * I := by ring
  _ = -↑u * (↑σ' - 1) + 1 * -(↑t * ↑u) * I := by rw [div_self (by norm_num; exact pi_ne_zero)]
  _ = _ := by ring
State after:
case e_f.h.e_a
n : ℕ
A a b c d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
⊢ ∫ (a : ℝ) in Ici (-x.log), cexp (-↑a * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑a / (2 * ↑π))) * I) =
    ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1)) * ↑x ^ (↑t * I)

State before:
case e_f.h.e_a
n : ℕ
A a b c d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
⊢ ∫ (a : ℝ) in Ici (-x.log), cexp (-↑a * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑a / (2 * ↑π))) * I) =
    ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1)) * ↑x ^ (↑t * I)
Tactic:
simp_rw [this]
State after:
case e_f.h.e_a
n : ℕ
A a b c d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
⊢ ∫ (a : ℝ) in Ici (-x.log), cexp ((1 - ↑σ' - ↑t * I) * ↑a) = ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1)) * ↑x ^ (↑t * I)

State before:
case e_f.h.e_a
n : ℕ
A a b c d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
⊢ ∫ (a : ℝ) in Ici (-x.log), cexp ((1 - ↑σ' - ↑t * I) * ↑a) = ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1)) * ↑x ^ (↑t * I)
Tactic:
let c : ℂ := (1 - ↑σ' - ↑t * I)
State after:
case e_f.h.e_a
n : ℕ
A a b c✝ d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
⊢ ∫ (a : ℝ) in Ici (-x.log), cexp ((1 - ↑σ' - ↑t * I) * ↑a) = ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1)) * ↑x ^ (↑t * I)

State before:
case e_f.h.e_a
n : ℕ
A a b c✝ d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
⊢ ∫ (a : ℝ) in Ici (-x.log), cexp ((1 - ↑σ' - ↑t * I) * ↑a) = ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1)) * ↑x ^ (↑t * I)
Tactic:
have : c ≠ 0 := by simp [Complex.ext_iff, c] ; intro h ; linarith
State after:
case e_f.h.e_a
n : ℕ
A a b c✝ d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
⊢ ∫ (a : ℝ) in Ici (-x.log), cexp ((1 - ↑σ' - ↑t * I) * ↑a) = ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1)) * ↑x ^ (↑t * I)

State before:
case e_f.h.e_a
n : ℕ
A a b c✝ d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
⊢ ∫ (a : ℝ) in Ici (-x.log), cexp ((1 - ↑σ' - ↑t * I) * ↑a) = ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1)) * ↑x ^ (↑t * I)
Tactic:
let f' (u : ℝ) := cexp (c * u)
State after:
case e_f.h.e_a
n : ℕ
A a b c✝ d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
⊢ ∫ (a : ℝ) in Ici (-x.log), cexp ((1 - ↑σ' - ↑t * I) * ↑a) = ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1)) * ↑x ^ (↑t * I)

State before:
case e_f.h.e_a
n : ℕ
A a b c✝ d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
⊢ ∫ (a : ℝ) in Ici (-x.log), cexp ((1 - ↑σ' - ↑t * I) * ↑a) = ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1)) * ↑x ^ (↑t * I)
Tactic:
let f := fun (u : ℝ) ↦ (f' u) / c
State after:
case e_f.h.e_a
n : ℕ
A a b c✝ d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
⊢ ∫ (a : ℝ) in Ici (-x.log), cexp ((1 - ↑σ' - ↑t * I) * ↑a) = ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1)) * ↑x ^ (↑t * I)

State before:
case e_f.h.e_a
n : ℕ
A a b c✝ d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
⊢ ∫ (a : ℝ) in Ici (-x.log), cexp ((1 - ↑σ' - ↑t * I) * ↑a) = ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1)) * ↑x ^ (↑t * I)
Tactic:
have hderiv : ∀ u ∈ Ici (-Real.log x), HasDerivAt f (f' u) u := by
  intro u _
  rw [show f' u = cexp (c * u) * (c * 1) / c by field_simp]
  exact (hasDerivAt_id' u).ofReal_comp.const_mul c |>.cexp.div_const c
State after:
case e_f.h.e_a
n : ℕ
A a b c✝ d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
hderiv : ∀ u ∈ Ici (-x.log), HasDerivAt f (f' u) u
⊢ ∫ (a : ℝ) in Ici (-x.log), cexp ((1 - ↑σ' - ↑t * I) * ↑a) = ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1)) * ↑x ^ (↑t * I)

State before:
case e_f.h.e_a
n : ℕ
A a b c✝ d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
hderiv : ∀ u ∈ Ici (-x.log), HasDerivAt f (f' u) u
⊢ ∫ (a : ℝ) in Ici (-x.log), cexp ((1 - ↑σ' - ↑t * I) * ↑a) = ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1)) * ↑x ^ (↑t * I)
Tactic:
have hf : Tendsto f atTop (𝓝 0) := by
  apply tendsto_zero_iff_norm_tendsto_zero.mpr
  suffices Tendsto (fun (x : ℝ) ↦ abs (cexp (c * ↑x)) / abs c) atTop (𝓝 (0 / abs c)) by simpa [f, f'] using this
  apply Filter.Tendsto.div_const
  suffices Tendsto (. * (1 - σ')) atTop atBot by simpa [Complex.abs_exp, mul_comm (1 - σ'), c]
  exact Tendsto.atTop_mul_neg_const (by linarith) fun ⦃s⦄ h ↦ h
State after:
case e_f.h.e_a
n : ℕ
A a b c✝ d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
hderiv : ∀ u ∈ Ici (-x.log), HasDerivAt f (f' u) u
hf : Tendsto f atTop (𝓝 0)
⊢ ∫ (a : ℝ) in Ici (-x.log), cexp ((1 - ↑σ' - ↑t * I) * ↑a) = ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1)) * ↑x ^ (↑t * I)

State before:
case e_f.h.e_a
n : ℕ
A a b c✝ d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
hderiv : ∀ u ∈ Ici (-x.log), HasDerivAt f (f' u) u
hf : Tendsto f atTop (𝓝 0)
⊢ ∫ (a : ℝ) in Ici (-x.log), cexp ((1 - ↑σ' - ↑t * I) * ↑a) = ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1)) * ↑x ^ (↑t * I)
Tactic:
rw [integral_Ici_eq_integral_Ioi,
  integral_Ioi_of_hasDerivAt_of_tendsto' hderiv (second_fourier_integrable_aux2 hσ) hf]
State after:
case e_f.h.e_a
n : ℕ
A a b c✝ d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
hderiv : ∀ u ∈ Ici (-x.log), HasDerivAt f (f' u) u
hf : Tendsto f atTop (𝓝 0)
⊢ 0 - f (-x.log) = ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1)) * ↑x ^ (↑t * I)

State before:
case e_f.h.e_a
n : ℕ
A a b c✝ d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
hderiv : ∀ u ∈ Ici (-x.log), HasDerivAt f (f' u) u
hf : Tendsto f atTop (𝓝 0)
⊢ 0 - f (-x.log) = ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑t * I - 1)) * ↑x ^ (↑t * I)
Tactic:
simpa [f, f'] using second_fourier_aux hx
State after:
no goals

State before:
n : ℕ
A a✝ b✝ c d✝ u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
a b d : ℂ
⊢ a * (b * ψ t * d) = a * b * d * ψ t
Tactic:
ring
State after:
no goals

State before:
n : ℕ
A a b c d u✝ x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t u : ℝ
⊢ -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = -↑u * (↑σ' - 1) + 2 * ↑π / (2 * ↑π) * -(↑t * ↑u) * I
Tactic:
ring
State after:
no goals

State before:
n : ℕ
A a b c d u✝ x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t u : ℝ
⊢ -↑u * (↑σ' - 1) + 2 * ↑π / (2 * ↑π) * -(↑t * ↑u) * I = -↑u * (↑σ' - 1) + 1 * -(↑t * ↑u) * I
Tactic:
rw [div_self (by norm_num; exact pi_ne_zero)]
State after:
no goals

State before:
n : ℕ
A a b c d u✝ x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t u : ℝ
⊢ 2 * ↑π ≠ 0
Tactic:
norm_num
State after:
n : ℕ
A a b c d u✝ x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t u : ℝ
⊢ ¬π = 0

State before:
n : ℕ
A a b c d u✝ x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t u : ℝ
⊢ ¬π = 0
Tactic:
exact pi_ne_zero
State after:
no goals

State before:
n : ℕ
A a b c d u✝ x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t u : ℝ
⊢ -↑u * (↑σ' - 1) + 1 * -(↑t * ↑u) * I = (1 - ↑σ' - ↑t * I) * ↑u
Tactic:
ring
State after:
no goals

State before:
n : ℕ
A a b c✝ d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
⊢ c ≠ 0
Tactic:
simp [Complex.ext_iff, c]
State after:
n : ℕ
A a b c✝ d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
⊢ 1 - σ' = 0 → ¬t = 0

State before:
n : ℕ
A a b c✝ d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
⊢ 1 - σ' = 0 → ¬t = 0
Tactic:
intro h
State after:
n : ℕ
A a b c✝ d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
h : 1 - σ' = 0
⊢ ¬t = 0

State before:
n : ℕ
A a b c✝ d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
h : 1 - σ' = 0
⊢ ¬t = 0
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 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
⊢ ∀ u ∈ Ici (-x.log), HasDerivAt f (f' u) u
Tactic:
intro u _
State after:
n : ℕ
A a b c✝ d u✝ x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
u : ℝ
a✝ : u ∈ Ici (-x.log)
⊢ HasDerivAt f (f' u) u

State before:
n : ℕ
A a b c✝ d u✝ x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
u : ℝ
a✝ : u ∈ Ici (-x.log)
⊢ HasDerivAt f (f' u) u
Tactic:
rw [show f' u = cexp (c * u) * (c * 1) / c by field_simp]
State after:
n : ℕ
A a b c✝ d u✝ x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
u : ℝ
a✝ : u ∈ Ici (-x.log)
⊢ HasDerivAt f (cexp (c * ↑u) * (c * 1) / c) u

State before:
n : ℕ
A a b c✝ d u✝ x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
u : ℝ
a✝ : u ∈ Ici (-x.log)
⊢ HasDerivAt f (cexp (c * ↑u) * (c * 1) / c) u
Tactic:
exact (hasDerivAt_id' u).ofReal_comp.const_mul c |>.cexp.div_const c
State after:
no goals

State before:
n : ℕ
A a b c✝ d u✝ x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
u : ℝ
a✝ : u ∈ Ici (-x.log)
⊢ f' u = cexp (c * ↑u) * (c * 1) / c
Tactic:
field_simp
State after:
no goals

State before:
n : ℕ
A a b c✝ d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
hderiv : ∀ u ∈ Ici (-x.log), HasDerivAt f (f' u) u
⊢ Tendsto f atTop (𝓝 0)
Tactic:
apply tendsto_zero_iff_norm_tendsto_zero.mpr
State after:
n : ℕ
A a b c✝ d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
hderiv : ∀ u ∈ Ici (-x.log), HasDerivAt f (f' u) u
⊢ Tendsto (fun x => ‖f x‖) atTop (𝓝 0)

State before:
n : ℕ
A a b c✝ d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
hderiv : ∀ u ∈ Ici (-x.log), HasDerivAt f (f' u) u
⊢ Tendsto (fun x => ‖f x‖) atTop (𝓝 0)
Tactic:
suffices Tendsto (fun (x : ℝ) ↦ abs (cexp (c * ↑x)) / abs c) atTop (𝓝 (0 / abs c)) by simpa [f, f'] using this
State after:
n : ℕ
A a b c✝ d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
hderiv : ∀ u ∈ Ici (-x.log), HasDerivAt f (f' u) u
⊢ Tendsto (fun x => Complex.abs (cexp (c * ↑x)) / Complex.abs c) atTop (𝓝 (0 / Complex.abs c))

State before:
n : ℕ
A a b c✝ d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
hderiv : ∀ u ∈ Ici (-x.log), HasDerivAt f (f' u) u
⊢ Tendsto (fun x => Complex.abs (cexp (c * ↑x)) / Complex.abs c) atTop (𝓝 (0 / Complex.abs c))
Tactic:
apply Filter.Tendsto.div_const
State after:
case hf
n : ℕ
A a b c✝ d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
hderiv : ∀ u ∈ Ici (-x.log), HasDerivAt f (f' u) u
⊢ Tendsto (fun a => Complex.abs (cexp (c * ↑a))) atTop (𝓝 0)

State before:
case hf
n : ℕ
A a b c✝ d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
hderiv : ∀ u ∈ Ici (-x.log), HasDerivAt f (f' u) u
⊢ Tendsto (fun a => Complex.abs (cexp (c * ↑a))) atTop (𝓝 0)
Tactic:
suffices Tendsto (. * (1 - σ')) atTop atBot by simpa [Complex.abs_exp, mul_comm (1 - σ'), c]
State after:
case hf
n : ℕ
A a b c✝ d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
hderiv : ∀ u ∈ Ici (-x.log), HasDerivAt f (f' u) u
⊢ Tendsto (fun x => x * (1 - σ')) atTop atBot

State before:
case hf
n : ℕ
A a b c✝ d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
hderiv : ∀ u ∈ Ici (-x.log), HasDerivAt f (f' u) u
⊢ Tendsto (fun x => x * (1 - σ')) atTop atBot
Tactic:
exact Tendsto.atTop_mul_neg_const (by linarith) fun ⦃s⦄ h ↦ h
State after:
no goals

State before:
n : ℕ
A a b c✝ d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this✝¹ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this✝ : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
hderiv : ∀ u ∈ Ici (-x.log), HasDerivAt f (f' u) u
this : Tendsto (fun x => Complex.abs (cexp (c * ↑x)) / Complex.abs c) atTop (𝓝 (0 / Complex.abs c))
⊢ Tendsto (fun x => ‖f x‖) atTop (𝓝 0)
Tactic:
simpa [f, f'] using this
State after:
no goals

State before:
n : ℕ
A a b c✝ d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this✝¹ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this✝ : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
hderiv : ∀ u ∈ Ici (-x.log), HasDerivAt f (f' u) u
this : Tendsto (fun x => x * (1 - σ')) atTop atBot
⊢ Tendsto (fun a => Complex.abs (cexp (c * ↑a))) atTop (𝓝 0)
Tactic:
simpa [Complex.abs_exp, mul_comm (1 - σ'), c]
State after:
no goals

State before:
n : ℕ
A a b c✝ d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
hderiv : ∀ u ∈ Ici (-x.log), HasDerivAt f (f' u) u
⊢ 1 - σ' < 0
Tactic:
linarith
State after:
no goals