Theorem: arg_exp_of_im (Ray/Hartogs/FubiniBall.lean)

State before:
t : ℝ
⊢ ∃ n, (↑t * I).exp.arg = t - 2 * π * ↑n
Tactic:
generalize hn : ⌈t / (2 * π) - 1 / 2⌉ = n
State after:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
⊢ ∃ n, (↑t * I).exp.arg = t - 2 * π * ↑n

State before:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
⊢ ∃ n, (↑t * I).exp.arg = t - 2 * π * ↑n
Tactic:
exists n
State after:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
⊢ (↑t * I).exp.arg = t - 2 * π * ↑n

State before:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
⊢ (↑t * I).exp.arg = t - 2 * π * ↑n
Tactic:
have en : exp (2 * π * n * I) = 1 := by
  rw [mul_comm _ (n:ℂ), mul_assoc, Complex.exp_int_mul]
  simp only [Complex.exp_two_pi_mul_I, one_zpow]
State after:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
⊢ (↑t * I).exp.arg = t - 2 * π * ↑n

State before:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
⊢ (↑t * I).exp.arg = t - 2 * π * ↑n
Tactic:
have e : exp (t * I) = exp (↑(t - 2 * π * n) * I) := by
  simp [mul_sub_right_distrib, Complex.exp_sub, en]
State after:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
⊢ (↑t * I).exp.arg = t - 2 * π * ↑n

State before:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
ts : t - 2 * π * ↑n ∈ Ioc (-π) π
⊢ (↑t * I).exp.arg = t - 2 * π * ↑n
Tactic:
rw [e, exp_of_im, ← Complex.cos_eq_cos, ← Complex.sin_eq_sin, Complex.arg_cos_add_sin_mul_I ts]
State after:
no goals

State before:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
⊢ (2 * ↑π * ↑n * I).exp = 1
Tactic:
rw [mul_comm _ (n:ℂ), mul_assoc, Complex.exp_int_mul]
State after:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
⊢ (2 * ↑π * I).exp ^ n = 1

State before:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
⊢ (2 * ↑π * I).exp ^ n = 1
Tactic:
simp only [Complex.exp_two_pi_mul_I, one_zpow]
State after:
no goals

State before:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
⊢ (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
Tactic:
simp [mul_sub_right_distrib, Complex.exp_sub, en]
State after:
no goals

State before:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
⊢ t - 2 * π * ↑n ∈ Ioc (-π) π
Tactic:
simp only [mem_Ioc, neg_lt_sub_iff_lt_add, tsub_le_iff_right]
State after:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
⊢ 2 * π * ↑n < π + t ∧ t ≤ π + 2 * π * ↑n

State before:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
⊢ 2 * π * ↑n < π + t ∧ t ≤ π + 2 * π * ↑n
Tactic:
constructor
State after:
case left
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
⊢ 2 * π * ↑n < π + t

case right
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
⊢ t ≤ π + 2 * π * ↑n

State before:
case left
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
⊢ 2 * π * ↑n < π + t
Tactic:
have h : ↑n < t * (2 * π)⁻¹ - 1 / 2 + 1 := by rw [← hn]; exact Int.ceil_lt_add_one _
State after:
case left
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
h : ↑n < t * (2 * π)⁻¹ - 1 / 2 + 1
⊢ 2 * π * ↑n < π + t

State before:
case left
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
h : ↑n < t * (2 * π)⁻¹ - 1 / 2 + 1
⊢ 2 * π * ↑n < π + t
Tactic:
calc 2 * π * ↑n
  _ < 2 * π * (t * (2 * π)⁻¹ - 1 / 2 + 1) := by bound
  _ = π + 2 * π * (2 * π)⁻¹ * t := by ring
  _ = π + t := by field_simp [Real.two_pi_pos.ne']
State after:
no goals

State before:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
⊢ ↑n < t * (2 * π)⁻¹ - 1 / 2 + 1
Tactic:
rw [← hn]
State after:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
⊢ ↑⌈t / (2 * π) - 1 / 2⌉ < t * (2 * π)⁻¹ - 1 / 2 + 1

State before:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
⊢ ↑⌈t / (2 * π) - 1 / 2⌉ < t * (2 * π)⁻¹ - 1 / 2 + 1
Tactic:
exact Int.ceil_lt_add_one _
State after:
no goals

State before:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
h : ↑n < t * (2 * π)⁻¹ - 1 / 2 + 1
⊢ 2 * π * ↑n < 2 * π * (t * (2 * π)⁻¹ - 1 / 2 + 1)
Tactic:
bound
State after:
no goals

State before:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
h : ↑n < t * (2 * π)⁻¹ - 1 / 2 + 1
⊢ 2 * π * (t * (2 * π)⁻¹ - 1 / 2 + 1) = π + 2 * π * (2 * π)⁻¹ * t
Tactic:
ring
State after:
no goals

State before:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
h : ↑n < t * (2 * π)⁻¹ - 1 / 2 + 1
⊢ π + 2 * π * (2 * π)⁻¹ * t = π + t
Tactic:
field_simp [Real.two_pi_pos.ne']
State after:
no goals

State before:
case right
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
⊢ t ≤ π + 2 * π * ↑n
Tactic:
have h : ↑n ≥ t * (2 * π)⁻¹ - 1 / 2 := by rw [← hn]; exact Int.le_ceil _
State after:
case right
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
h : ↑n ≥ t * (2 * π)⁻¹ - 1 / 2
⊢ t ≤ π + 2 * π * ↑n

State before:
case right
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
h : ↑n ≥ t * (2 * π)⁻¹ - 1 / 2
⊢ t ≤ π + 2 * π * ↑n
Tactic:
calc π + 2 * π * ↑n
  _ ≥ π + 2 * π * (t * (2 * π)⁻¹ - 1 / 2) := by bound
  _ = 2 * π * (2 * π)⁻¹ * t := by ring
  _ = t := by field_simp [Real.two_pi_pos.ne']
State after:
no goals

State before:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
⊢ ↑n ≥ t * (2 * π)⁻¹ - 1 / 2
Tactic:
rw [← hn]
State after:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
⊢ ↑⌈t / (2 * π) - 1 / 2⌉ ≥ t * (2 * π)⁻¹ - 1 / 2

State before:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
⊢ ↑⌈t / (2 * π) - 1 / 2⌉ ≥ t * (2 * π)⁻¹ - 1 / 2
Tactic:
exact Int.le_ceil _
State after:
no goals

State before:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
h : ↑n ≥ t * (2 * π)⁻¹ - 1 / 2
⊢ π + 2 * π * ↑n ≥ π + 2 * π * (t * (2 * π)⁻¹ - 1 / 2)
Tactic:
bound
State after:
no goals

State before:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
h : ↑n ≥ t * (2 * π)⁻¹ - 1 / 2
⊢ π + 2 * π * (t * (2 * π)⁻¹ - 1 / 2) = 2 * π * (2 * π)⁻¹ * t
Tactic:
ring
State after:
no goals

State before:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
h : ↑n ≥ t * (2 * π)⁻¹ - 1 / 2
⊢ 2 * π * (2 * π)⁻¹ * t = t
Tactic:
field_simp [Real.two_pi_pos.ne']
State after:
no goals