E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g : ℂ → E
z : ℂ
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hB : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)] fun z => expR (B * ↑Complex.abs z ^ c)
hre : ∀ (x : ℝ), x ≤ 0 → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
hz_re : z.re ≤ 0
hz_im : 0 ≤ z.im
⊢ ∃ z', z' * I = z

case intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hB : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)] fun z => expR (B * ↑Complex.abs z ^ c)
hre : ∀ (x : ℝ), x ≤ 0 → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
z : ℂ
hz_re : (z * I).re ≤ 0
hz_im : 0 ≤ (z * I).im
⊢ ‖f (z * I)‖ ≤ C
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g : ℂ → E
z : ℂ
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hB : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)] fun z => expR (B * ↑Complex.abs z ^ c)
hre : ∀ (x : ℝ), x ≤ 0 → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
hz_re : z.re ≤ 0
hz_im : 0 ≤ z.im
⊢ ‖f z‖ ≤ C
obtain ⟨z, rfl⟩ : ∃ z', z' * I = z
case intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hB : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)] fun z => expR (B * ↑Complex.abs z ^ c)
hre : ∀ (x : ℝ), x ≤ 0 → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
z : ℂ
hz_re : (z * I).re ≤ 0
hz_im : 0 ≤ (z * I).im
⊢ ‖f (z * I)‖ ≤ C
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g : ℂ → E
z : ℂ
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hB : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)] fun z => expR (B * ↑Complex.abs z ^ c)
hre : ∀ (x : ℝ), x ≤ 0 → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
hz_re : z.re ≤ 0
hz_im : 0 ≤ z.im
⊢ ∃ z', z' * I = z

case intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hB : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)] fun z => expR (B * ↑Complex.abs z ^ c)
hre : ∀ (x : ℝ), x ≤ 0 → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
z : ℂ
hz_re : (z * I).re ≤ 0
hz_im : 0 ≤ (z * I).im
⊢ ‖f (z * I)‖ ≤ C
exact ⟨z / I, div_mul_cancel _ I_ne_zero⟩
case intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hB : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)] fun z => expR (B * ↑Complex.abs z ^ c)
hre : ∀ (x : ℝ), x ≤ 0 → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.im
hz_im : 0 ≤ z.re
⊢ ‖f (z * I)‖ ≤ C
case intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hB : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)] fun z => expR (B * ↑Complex.abs z ^ c)
hre : ∀ (x : ℝ), x ≤ 0 → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
z : ℂ
hz_re : (z * I).re ≤ 0
hz_im : 0 ≤ (z * I).im
⊢ ‖f (z * I)‖ ≤ C
simp only [mul_I_re, mul_I_im, neg_nonpos] at hz_re hz_im
case intro.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hre : ∀ (x : ℝ), x ≤ 0 → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.im
hz_im : 0 ≤ z.re
H : MapsTo (fun x => x * I) (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Ioi 0)
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)] fun z => expR (B * ↑Complex.abs z ^ c)
⊢ ‖(f ∘ fun x => x * I) z‖ ≤ C
case intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hB : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)] fun z => expR (B * ↑Complex.abs z ^ c)
hre : ∀ (x : ℝ), x ≤ 0 → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.im
hz_im : 0 ≤ z.re
H : MapsTo (fun x => x * I) (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Ioi 0)
⊢ ‖(f ∘ fun x => x * I) z‖ ≤ C
rcases hB with ⟨c, hc, B, hO⟩
case intro.intro.intro.intro.refine'_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hre : ∀ (x : ℝ), x ≤ 0 → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.im
hz_im : 0 ≤ z.re
H : MapsTo (fun x => x * I) (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Ioi 0)
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)] fun z => expR (B * ↑Complex.abs z ^ c)
⊢ (f ∘ fun x => x * I) =O[comap (↑Complex.abs) atTop ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z => expR (B * ↑Complex.abs z ^ c)

case intro.intro.intro.intro.refine'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hre : ∀ (x : ℝ), x ≤ 0 → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.im
hz_im : 0 ≤ z.re
H : MapsTo (fun x => x * I) (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Ioi 0)
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)] fun z => expR (B * ↑Complex.abs z ^ c)
x : ℝ
hx : 0 ≤ x
⊢ ‖(f ∘ fun x => x * I) (↑x * I)‖ ≤ C
case intro.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hre : ∀ (x : ℝ), x ≤ 0 → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.im
hz_im : 0 ≤ z.re
H : MapsTo (fun x => x * I) (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Ioi 0)
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)] fun z => expR (B * ↑Complex.abs z ^ c)
⊢ ‖(f ∘ fun x => x * I) z‖ ≤ C
refine' quadrant_I (hd.comp (differentiable_id.mul_const _).diffContOnCl H) ⟨c, hc, B, ?_⟩ him
  (fun x hx => _) hz_im hz_re
no goals
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hB : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)] fun z => expR (B * ↑Complex.abs z ^ c)
hre : ∀ (x : ℝ), x ≤ 0 → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.im
hz_im : 0 ≤ z.re
w : ℂ
hw : w ∈ Ioi 0 ×ℂ Ioi 0
⊢ (fun x => x * I) w ∈ Iio 0 ×ℂ Ioi 0
simpa only [mem_reProdIm, mul_I_re, mul_I_im, neg_lt_zero, mem_Iio] using hw.symm
case intro.intro.intro.intro.refine'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hre : ∀ (x : ℝ), x ≤ 0 → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.im
hz_im : 0 ≤ z.re
H : MapsTo (fun x => x * I) (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Ioi 0)
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)] fun z => expR (B * ↑Complex.abs z ^ c)
x : ℝ
hx : 0 ≤ x
⊢ ‖f ↑(-x)‖ ≤ C
case intro.intro.intro.intro.refine'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hre : ∀ (x : ℝ), x ≤ 0 → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.im
hz_im : 0 ≤ z.re
H : MapsTo (fun x => x * I) (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Ioi 0)
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)] fun z => expR (B * ↑Complex.abs z ^ c)
x : ℝ
hx : 0 ≤ x
⊢ ‖(f ∘ fun x => x * I) (↑x * I)‖ ≤ C
rw [comp_apply, mul_assoc, I_mul_I, mul_neg_one, ← ofReal_neg]
no goals
case intro.intro.intro.intro.refine'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hre : ∀ (x : ℝ), x ≤ 0 → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.im
hz_im : 0 ≤ z.re
H : MapsTo (fun x => x * I) (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Ioi 0)
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)] fun z => expR (B * ↑Complex.abs z ^ c)
x : ℝ
hx : 0 ≤ x
⊢ ‖f ↑(-x)‖ ≤ C
exact hre _ (neg_nonpos.2 hx)