Documentation
SpherePacking
.
ModularForms
.
exp_lems
Search
return to top
source
Imports
Init
Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Imported by
exp_upperHalfPlane_lt_one
exp_upperHalfPlane_lt_one_nat
exp_periodo
source
theorem
exp_upperHalfPlane_lt_one
(
z
:
UpperHalfPlane
)
:
‖
Complex.exp
(
2
*
↑
Real.pi
*
Complex.I
*
↑
z
)
‖
<
1
source
theorem
exp_upperHalfPlane_lt_one_nat
(
z
:
UpperHalfPlane
)
(
n
:
ℕ
)
:
‖
Complex.exp
(
2
*
↑
Real.pi
*
Complex.I
*
(
↑
n
+
1
)
*
↑
z
)
‖
<
1
source
theorem
exp_periodo
(
z
:
UpperHalfPlane
)
(
n
:
ℕ
)
:
Complex.exp
(
2
*
↑
Real.pi
*
Complex.I
*
↑
n
*
(
1
+
↑
z
))
=
Complex.exp
(
2
*
↑
Real.pi
*
Complex.I
*
↑
n
*
↑
z
)