The exponential e^{2π i τ} on the upper half-plane

Elementary facts about q = e^{2π i τ}, its square root e^{π i τ} and e^{2π i (x τ + y)} for τ in the upper half-plane, complementing Mathlib.Analysis.Complex.UpperHalfPlane.Exp.

Main results

• TauCeti.UpperHalfPlane.exp_two_pi_I_eq_exp_pi_I_sq: e^{2π i τ} = (e^{π i τ})².
• TauCeti.UpperHalfPlane.norm_exp_two_pi_I_mul: |q| = e^{-2π Im τ}.
• TauCeti.UpperHalfPlane.norm_exp_two_pi_I_mul_add: ‖e^{2π i (x τ + y)}‖ = |q|^x.
• TauCeti.UpperHalfPlane.tendsto_exp_two_pi_I_mul_add: for x > 0, e^{2π i (x τ + y)} → 0 as Im τ → ∞.
• TauCeti.UpperHalfPlane.norm_exp_two_pi_I_mul_le: |q| ≤ e^{-2π t} when t ≤ Im τ.
• TauCeti.UpperHalfPlane.norm_one_sub_exp_two_pi_I_mul: |1 - e^{2π i y}| = |2 sin (π y)|.
• TauCeti.UpperHalfPlane.norm_exp_pi_I_lt_one: ‖e^{π i τ}‖ < 1 on the upper half-plane.
• TauCeti.UpperHalfPlane.one_sub_exp_two_pi_I_ne_zero: 1 - e^{2π i (x τ + y)} has no zero in the upper half-plane unless x = 0 and y ∈ ℤ.
• TauCeti.UpperHalfPlane.exp_two_pi_I_zpow_mul_exp: qᵏ e^{2π i (x τ + y)} = e^{2π i ((k + x) τ + y)} for k ∈ ℤ.

theorem TauCeti.UpperHalfPlane.exp_two_pi_I_eq_exp_pi_I_sq (τ : ℂ) : Complex.exp (2 * ↑Real.pi * Complex.I * τ) = Complex.exp (↑Real.pi * Complex.I * τ) ^ 2

q = e^{2π i τ} is the square of e^{π i τ}.

theorem TauCeti.UpperHalfPlane.norm_exp_two_pi_I_mul (τ : ℂ) : ‖Complex.exp (2 * ↑Real.pi * Complex.I * τ)‖ = Real.exp (-(2 * Real.pi * τ.im))

|q| = e^{-2π Im τ} for q = e^{2π i τ}.

theorem TauCeti.UpperHalfPlane.norm_exp_two_pi_I_mul_add (x y : ℝ) (τ : ℂ) : ‖Complex.exp (2 * ↑Real.pi * Complex.I * (↑x * τ + ↑y))‖ = ‖Complex.exp (2 * ↑Real.pi * Complex.I * τ)‖ ^ x

‖e^{2π i (x τ + y)}‖ = |q|^x for q = e^{2π i τ}.

theorem TauCeti.UpperHalfPlane.tendsto_exp_two_pi_I_mul_add {x : ℝ} (hx : 0 < x) (y : ℝ) : Filter.Tendsto (fun (τ : UpperHalfPlane) => Complex.exp (2 * ↑Real.pi * Complex.I * (↑x * ↑τ + ↑y))) UpperHalfPlane.atImInfty (nhds 0)

For x > 0, e^{2π i (x τ + y)} tends to zero as Im τ → ∞, with no restriction on Re τ.

theorem TauCeti.UpperHalfPlane.norm_exp_two_pi_I_mul_le {t : ℝ} {τ : ℂ} (hτ : t ≤ τ.im) : ‖Complex.exp (2 * ↑Real.pi * Complex.I * τ)‖ ≤ Real.exp (-(2 * Real.pi * t))

Im τ ≥ t means |q| ≤ e^{-2π t} for q = e^{2π i τ}.

theorem TauCeti.UpperHalfPlane.norm_one_sub_exp_two_pi_I_mul (y : ℝ) : ‖1 - Complex.exp (2 * ↑Real.pi * Complex.I * ↑y)‖ = |2 * Real.sin (Real.pi * y)|

|1 - e^{2π i y}| = |2 sin (π y)| for real y.

theorem TauCeti.UpperHalfPlane.norm_exp_pi_I_lt_one {τ : ℂ} (hτ : 0 < τ.im) : ‖Complex.exp (↑Real.pi * Complex.I * τ)‖ < 1

The square root e^{π i τ} of q = e^{2π i τ} has norm less than one on the upper half-plane.

theorem TauCeti.UpperHalfPlane.one_sub_exp_two_pi_I_ne_zero {x y : ℝ} {τ : ℂ} (hτ : 0 < τ.im) (h : ∀ (k : ℤ), x = 0 → y ≠ ↑k) : 1 - Complex.exp (2 * ↑Real.pi * Complex.I * (↑x * τ + ↑y)) ≠ 0

1 - e^{2π i (x τ + y)} vanishes at a point τ of the upper half-plane only when x = 0 and y is an integer.

theorem TauCeti.UpperHalfPlane.exp_two_pi_I_zpow_mul_exp (k : ℤ) (x y : ℝ) (τ : ℂ) : Complex.exp (2 * ↑Real.pi * Complex.I * τ) ^ k * Complex.exp (2 * ↑Real.pi * Complex.I * (↑x * τ + ↑y)) = Complex.exp (2 * ↑Real.pi * Complex.I * (↑(↑k + x) * τ + ↑y))

qᵏ e^{2π i (x τ + y)} = e^{2π i ((k + x) τ + y)} for q = e^{2π i τ} and k ∈ ℤ.