theorem periodic_strip_to_global (f : ℂ → ℂ) (hf_per : Function.Periodic f 1) (C : ℝ) (hC : ∀ (s : ℂ), 0 ≤ s.re → s.re ≤ 1 → ‖f s‖ ≤ C * Real.exp |s.im|) (s : ℂ) : ‖f s‖ ≤ C * Real.exp |s.im|

theorem sin_pi_mul_add_one (z : ℂ) : Complex.sin (↑Real.pi * (z + 1)) = -Complex.sin (↑Real.pi * z)

theorem dense_sin_pi_ne_zero : Dense {z : ℂ | Complex.sin (↑Real.pi * z) ≠ 0}

theorem sin_pi_half_ne_zero : Complex.sin (↑Real.pi * (1 / 2)) ≠ 0

theorem int_of_norm_sub_lt_one {k n : ℤ} (h : ‖↑k - ↑n‖ < 1) : k = n

theorem sin_pi_ne_zero_in_ball (n : ℤ) (z : ℂ) (hz : z ∈ Metric.ball (↑n) 1) (hzn : z ≠ ↑n) : Complex.sin (↑Real.pi * z) ≠ 0

theorem dslope_entire {f : ℂ → ℂ} (hf : Differentiable ℂ f) (c : ℂ) : Differentiable ℂ (dslope f c)

theorem dslope_sinpi_at_int_ne_zero (n : ℤ) : dslope (fun (z : ℂ) => Complex.sin (↑Real.pi * z)) ↑n ↑n ≠ 0

theorem sinpi_differentiable : Differentiable ℂ fun (z : ℂ) => Complex.sin (↑Real.pi * z)

noncomputable def mkQuotient (h : ℂ → ℂ) (z : ℂ) : ℂ

theorem entire_quotient_by_sin_pi (h : ℂ → ℂ) (hh_diff : Differentiable ℂ h) (hh_zero : ∀ (n : ℤ), h ↑n = 0) : ∃ (g : ℂ → ℂ), Differentiable ℂ g ∧ ∀ (z : ℂ), Complex.sin (↑Real.pi * z) ≠ 0 → g z = h z / Complex.sin (↑Real.pi * z)

theorem normSq_sin (z : ℂ) : Complex.normSq (Complex.sin z) = Real.sin z.re ^ 2 + Real.sinh z.im ^ 2

theorem norm_sin_ge_abs_sinh_im (z : ℂ) : ‖Complex.sin z‖ ≥ |Real.sinh z.im|

theorem sinh_ge_exp_div_four {t : ℝ} (ht : 1 ≤ t) : Real.sinh t ≥ Real.exp t / 4

theorem norm_sin_pi_lower_bound (z : ℂ) (him : 1 ≤ |z.im|) : ‖Complex.sin (↑Real.pi * z)‖ ≥ Real.exp (Real.pi * |z.im|) / 4

theorem strip_box_compact : IsCompact {z : ℂ | 0 ≤ z.re ∧ z.re ≤ 1 ∧ |z.im| ≤ 1}

theorem quotient_bounded_on_strip (h : ℂ → ℂ) (hh_diff : Differentiable ℂ h) (hh_zero : ∀ (n : ℤ), h ↑n = 0) (C : ℝ) (hC : ∀ (s : ℂ), ‖h s‖ ≤ C * Real.exp |s.im|) (g : ℂ → ℂ) (hg_diff : Differentiable ℂ g) (hg_eq : ∀ (z : ℂ), Complex.sin (↑Real.pi * z) ≠ 0 → g z = h z / Complex.sin (↑Real.pi * z)) : ∃ (M : ℝ), ∀ (s : ℂ), 0 ≤ s.re → s.re ≤ 1 → ‖g s‖ ≤ M

theorem entire_bounded_auxiliary (f : ℂ → ℂ) (hf_diff : Differentiable ℂ f) (hf_per : Function.Periodic f 1) (C : ℝ) (hC_global : ∀ (s : ℂ), ‖f s‖ ≤ C * Real.exp |s.im|) : ∃ (g : ℂ → ℂ), Differentiable ℂ g ∧ (∀ (z : ℂ), Complex.sin (↑Real.pi * z) ≠ 0 → g z = (f z - f 0) / Complex.sin (↑Real.pi * z)) ∧ Bornology.IsBounded (Set.range g)

theorem entire_periodic_exp_growth_bounded (f : ℂ → ℂ) (hf_diff : Differentiable ℂ f) (hf_per : Function.Periodic f 1) (C : ℝ) (hC : ∀ (s : ℂ), 0 ≤ s.re → s.re ≤ 1 → ‖f s‖ ≤ C * Real.exp |s.im|) : Bornology.IsBounded (Set.range f)

theorem periodic_entire_exp_growth_is_const (f : ℂ → ℂ) (hf_diff : Differentiable ℂ f) (hf_per : Function.Periodic f 1) (hf_growth : ∃ (C : ℝ), ∀ (s : ℂ), 0 ≤ s.re → s.re ≤ 1 → ‖f s‖ ≤ C * Real.exp |s.im|) : ∃ (c : ℂ), f = Function.const ℂ c