Theorem: first_fourier_aux2 (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
⊢ term f (↑σ') n * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y = term f (↑σ' + ↑y * I) n • (ψ y * ↑x ^ (↑y * I))
Tactic:
by_cases hn : n = 0
State after:
case pos
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : n = 0
⊢ term f (↑σ') n * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y = term f (↑σ' + ↑y * I) n • (ψ y * ↑x ^ (↑y * I))

case neg
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ term f (↑σ') n * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y = term f (↑σ' + ↑y * I) n • (ψ y * ↑x ^ (↑y * I))

State before:
case pos
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : n = 0
⊢ term f (↑σ') n * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y = term f (↑σ' + ↑y * I) n • (ψ y * ↑x ^ (↑y * I))

case neg
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ term f (↑σ') n * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y = term f (↑σ' + ↑y * I) n • (ψ y * ↑x ^ (↑y * I))
Tactic:
simp [term, hn]
State after:
case neg
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ term f (↑σ') n * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y = term f (↑σ' + ↑y * I) n • (ψ y * ↑x ^ (↑y * I))

State before:
case neg
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ term f (↑σ') n * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y = term f (↑σ' + ↑y * I) n • (ψ y * ↑x ^ (↑y * I))
Tactic:
simp only [term, hn, ↓reduceIte, fourierChar_apply]
State after:
case neg
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ f n / ↑n ^ ↑σ' * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y = (f n / ↑n ^ (↑σ' + ↑y * I)) • (ψ y * ↑x ^ (↑y * I))

State before:
case neg
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ f n / ↑n ^ ↑σ' * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y = (f n / ↑n ^ (↑σ' + ↑y * I)) • (ψ y * ↑x ^ (↑y * I))
Tactic:
calc
  _ = (f n * (cexp ((2 * π * -(y * (1 / (2 * π) * Real.log (n / x)))) * I) / ↑((n : ℝ) ^ σ'))) • ψ y := by
    have : ((↑n : ℂ) ^ (σ' : ℂ) : ℂ) = ((↑n : ℝ) ^ (σ' : ℝ) : ℝ) := by
      rw [Complex.cpow_def_of_ne_zero (by simp [hn]), Real.rpow_def_of_nonneg (Nat.cast_nonneg n)]
      simp [hn]
    simp [Real.fourierChar, expMapCircle, smul_eq_mul, mul_assoc, this] ; ring
  _ = (f n * (x ^ (y * I) / n ^ (σ' + y * I))) • ψ y := by
    congr 2
    have l1 : 0 < (n : ℝ) := by simpa using Nat.pos_iff_ne_zero.mpr hn
    have l2 : (x : ℂ) ≠ 0 := by simp [hx.ne.symm]
    have l3 : (n : ℂ) ≠ 0 := by simp [hn]
    rw [Real.rpow_def_of_pos l1, Complex.cpow_def_of_ne_zero l2, Complex.cpow_def_of_ne_zero l3]
    push_cast
    simp_rw [← Complex.exp_sub]
    congr 1
    rw [first_fourier_aux2a, Real.log_div l1.ne.symm hx.ne.symm]
    push_cast
    rw [Complex.ofReal_log hx.le]
    ring
  _ = _ := by simp ; group
State after:
no goals

State before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ f n / ↑n ^ ↑σ' * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y =
    (f n * (cexp (2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) * I) / ↑(↑n ^ σ'))) • ψ y
Tactic:
have : ((↑n : ℂ) ^ (σ' : ℂ) : ℂ) = ((↑n : ℝ) ^ (σ' : ℝ) : ℝ) := by
  rw [Complex.cpow_def_of_ne_zero (by simp [hn]), Real.rpow_def_of_nonneg (Nat.cast_nonneg n)]
  simp [hn]
State after:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
this : ↑n ^ ↑σ' = ↑(↑n ^ σ')
⊢ f n / ↑n ^ ↑σ' * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y =
    (f n * (cexp (2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) * I) / ↑(↑n ^ σ'))) • ψ y

State before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
this : ↑n ^ ↑σ' = ↑(↑n ^ σ')
⊢ f n / ↑n ^ ↑σ' * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y =
    (f n * (cexp (2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) * I) / ↑(↑n ^ σ'))) • ψ y
Tactic:
simp [Real.fourierChar, expMapCircle, smul_eq_mul, mul_assoc, this]
State after:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
this : ↑n ^ ↑σ' = ↑(↑n ^ σ')
⊢ f n / ↑(↑n ^ σ') * (cexp (-(2 * (↑π * (↑y * ((↑π)⁻¹ * (2⁻¹ * (↑(↑n / x).log * I))))))) * ψ y) =
    f n * (cexp (-(2 * (↑π * (↑y * ((↑π)⁻¹ * (2⁻¹ * (↑(↑n / x).log * I))))))) / ↑(↑n ^ σ') * ψ y)

State before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
this : ↑n ^ ↑σ' = ↑(↑n ^ σ')
⊢ f n / ↑(↑n ^ σ') * (cexp (-(2 * (↑π * (↑y * ((↑π)⁻¹ * (2⁻¹ * (↑(↑n / x).log * I))))))) * ψ y) =
    f n * (cexp (-(2 * (↑π * (↑y * ((↑π)⁻¹ * (2⁻¹ * (↑(↑n / x).log * I))))))) / ↑(↑n ^ σ') * ψ y)
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 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ ↑n ^ ↑σ' = ↑(↑n ^ σ')
Tactic:
rw [Complex.cpow_def_of_ne_zero (by simp [hn]), Real.rpow_def_of_nonneg (Nat.cast_nonneg n)]
State after:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ cexp ((↑n).log * ↑σ') = ↑(if ↑n = 0 then if σ' = 0 then 1 else 0 else rexp ((↑n).log * σ'))

State before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ cexp ((↑n).log * ↑σ') = ↑(if ↑n = 0 then if σ' = 0 then 1 else 0 else rexp ((↑n).log * σ'))
Tactic:
simp [hn]
State after:
no goals

State before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ ↑n ≠ 0
Tactic:
simp [hn]
State after:
no goals

State before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ (f n * (cexp (2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) * I) / ↑(↑n ^ σ'))) • ψ y =
    (f n * (↑x ^ (↑y * I) / ↑n ^ (↑σ' + ↑y * I))) • ψ y
Tactic:
congr 2
State after:
case e_a.e_a
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ cexp (2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) * I) / ↑(↑n ^ σ') = ↑x ^ (↑y * I) / ↑n ^ (↑σ' + ↑y * I)

State before:
case e_a.e_a
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ cexp (2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) * I) / ↑(↑n ^ σ') = ↑x ^ (↑y * I) / ↑n ^ (↑σ' + ↑y * I)
Tactic:
have l1 : 0 < (n : ℝ) := by simpa using Nat.pos_iff_ne_zero.mpr hn
State after:
case e_a.e_a
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
⊢ cexp (2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) * I) / ↑(↑n ^ σ') = ↑x ^ (↑y * I) / ↑n ^ (↑σ' + ↑y * I)

State before:
case e_a.e_a
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
⊢ cexp (2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) * I) / ↑(↑n ^ σ') = ↑x ^ (↑y * I) / ↑n ^ (↑σ' + ↑y * I)
Tactic:
have l2 : (x : ℂ) ≠ 0 := by simp [hx.ne.symm]
State after:
case e_a.e_a
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
l2 : ↑x ≠ 0
⊢ cexp (2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) * I) / ↑(↑n ^ σ') = ↑x ^ (↑y * I) / ↑n ^ (↑σ' + ↑y * I)

State before:
case e_a.e_a
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
l2 : ↑x ≠ 0
⊢ cexp (2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) * I) / ↑(↑n ^ σ') = ↑x ^ (↑y * I) / ↑n ^ (↑σ' + ↑y * I)
Tactic:
have l3 : (n : ℂ) ≠ 0 := by simp [hn]
State after:
case e_a.e_a
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
l2 : ↑x ≠ 0
l3 : ↑n ≠ 0
⊢ cexp (2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) * I) / ↑(↑n ^ σ') = ↑x ^ (↑y * I) / ↑n ^ (↑σ' + ↑y * I)

State before:
case e_a.e_a
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
l2 : ↑x ≠ 0
l3 : ↑n ≠ 0
⊢ cexp (2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) * I) / ↑(↑n ^ σ') = ↑x ^ (↑y * I) / ↑n ^ (↑σ' + ↑y * I)
Tactic:
rw [Real.rpow_def_of_pos l1, Complex.cpow_def_of_ne_zero l2, Complex.cpow_def_of_ne_zero l3]
State after:
case e_a.e_a
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
l2 : ↑x ≠ 0
l3 : ↑n ≠ 0
⊢ cexp (2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) * I) / ↑(rexp ((↑n).log * σ')) =
    cexp ((↑x).log * (↑y * I)) / cexp ((↑n).log * (↑σ' + ↑y * I))

State before:
case e_a.e_a
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
l2 : ↑x ≠ 0
l3 : ↑n ≠ 0
⊢ cexp (2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) * I) / ↑(rexp ((↑n).log * σ')) =
    cexp ((↑x).log * (↑y * I)) / cexp ((↑n).log * (↑σ' + ↑y * I))
Tactic:
push_cast
State after:
case e_a.e_a
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
l2 : ↑x ≠ 0
l3 : ↑n ≠ 0
⊢ cexp (2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) * I) / cexp ((↑n).log * ↑σ') =
    cexp ((↑x).log * (↑y * I)) / cexp ((↑n).log * (↑σ' + ↑y * I))

State before:
case e_a.e_a
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
l2 : ↑x ≠ 0
l3 : ↑n ≠ 0
⊢ cexp (2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) * I) / cexp ((↑n).log * ↑σ') =
    cexp ((↑x).log * (↑y * I)) / cexp ((↑n).log * (↑σ' + ↑y * I))
Tactic:
simp_rw [← Complex.exp_sub]
State after:
case e_a.e_a
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
l2 : ↑x ≠ 0
l3 : ↑n ≠ 0
⊢ cexp (2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) * I - (↑n).log * ↑σ') =
    cexp ((↑x).log * (↑y * I) - (↑n).log * (↑σ' + ↑y * I))

State before:
case e_a.e_a
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
l2 : ↑x ≠ 0
l3 : ↑n ≠ 0
⊢ cexp (2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) * I - (↑n).log * ↑σ') =
    cexp ((↑x).log * (↑y * I) - (↑n).log * (↑σ' + ↑y * I))
Tactic:
congr 1
State after:
case e_a.e_a.e_z
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
l2 : ↑x ≠ 0
l3 : ↑n ≠ 0
⊢ 2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) * I - (↑n).log * ↑σ' = (↑x).log * (↑y * I) - (↑n).log * (↑σ' + ↑y * I)

State before:
case e_a.e_a.e_z
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
l2 : ↑x ≠ 0
l3 : ↑n ≠ 0
⊢ 2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) * I - (↑n).log * ↑σ' = (↑x).log * (↑y * I) - (↑n).log * (↑σ' + ↑y * I)
Tactic:
rw [first_fourier_aux2a, Real.log_div l1.ne.symm hx.ne.symm]
State after:
case e_a.e_a.e_z
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
l2 : ↑x ≠ 0
l3 : ↑n ≠ 0
⊢ -(↑y * ↑((↑n).log - x.log)) * I - (↑n).log * ↑σ' = (↑x).log * (↑y * I) - (↑n).log * (↑σ' + ↑y * I)

State before:
case e_a.e_a.e_z
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
l2 : ↑x ≠ 0
l3 : ↑n ≠ 0
⊢ -(↑y * ↑((↑n).log - x.log)) * I - (↑n).log * ↑σ' = (↑x).log * (↑y * I) - (↑n).log * (↑σ' + ↑y * I)
Tactic:
push_cast
State after:
case e_a.e_a.e_z
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
l2 : ↑x ≠ 0
l3 : ↑n ≠ 0
⊢ -(↑y * ((↑n).log - ↑x.log)) * I - (↑n).log * ↑σ' = (↑x).log * (↑y * I) - (↑n).log * (↑σ' + ↑y * I)

State before:
case e_a.e_a.e_z
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
l2 : ↑x ≠ 0
l3 : ↑n ≠ 0
⊢ -(↑y * ((↑n).log - ↑x.log)) * I - (↑n).log * ↑σ' = (↑x).log * (↑y * I) - (↑n).log * (↑σ' + ↑y * I)
Tactic:
rw [Complex.ofReal_log hx.le]
State after:
case e_a.e_a.e_z
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
l2 : ↑x ≠ 0
l3 : ↑n ≠ 0
⊢ -(↑y * ((↑n).log - (↑x).log)) * I - (↑n).log * ↑σ' = (↑x).log * (↑y * I) - (↑n).log * (↑σ' + ↑y * I)

State before:
case e_a.e_a.e_z
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
l2 : ↑x ≠ 0
l3 : ↑n ≠ 0
⊢ -(↑y * ((↑n).log - (↑x).log)) * I - (↑n).log * ↑σ' = (↑x).log * (↑y * I) - (↑n).log * (↑σ' + ↑y * 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 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ 0 < ↑n
Tactic:
simpa using Nat.pos_iff_ne_zero.mpr hn
State after:
no goals

State before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
⊢ ↑x ≠ 0
Tactic:
simp [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 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
l2 : ↑x ≠ 0
⊢ ↑n ≠ 0
Tactic:
simp [hn]
State after:
no goals

State before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ (f n * (↑x ^ (↑y * I) / ↑n ^ (↑σ' + ↑y * I))) • ψ y = (f n / ↑n ^ (↑σ' + ↑y * I)) • (ψ y * ↑x ^ (↑y * I))
Tactic:
simp
State after:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ f n * (↑x ^ (↑y * I) / ↑n ^ (↑σ' + ↑y * I)) * ψ y = f n / ↑n ^ (↑σ' + ↑y * I) * (ψ y * ↑x ^ (↑y * I))

State before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ f n * (↑x ^ (↑y * I) / ↑n ^ (↑σ' + ↑y * I)) * ψ y = f n / ↑n ^ (↑σ' + ↑y * I) * (ψ y * ↑x ^ (↑y * I))
Tactic:
group
State after:
no goals