E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g : ℂ → E
z : ℂ
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
⊢ ∀ᶠ (ε : ℝ) in 𝓝[Iio 0] 0, ‖exp (↑ε * z) • f z‖ ≤ C
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g : ℂ → E
z : ℂ
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
⊢ ‖f z‖ ≤ C
suffices ∀ᶠ ε : ℝ in 𝓝[<] 0, ‖exp (ε * z) • f z‖ ≤ C by
  refine' le_of_tendsto (Tendsto.mono_left _ nhdsWithin_le_nhds) this
  apply ((continuous_ofReal.mul continuous_const).cexp.smul continuous_const).norm.tendsto'
  simp
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g : ℂ → E
z : ℂ
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε ∈ Iio 0
⊢ ‖exp (↑ε * z) • f z‖ ≤ C
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g : ℂ → E
z : ℂ
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
⊢ ∀ᶠ (ε : ℝ) in 𝓝[Iio 0] 0, ‖exp (↑ε * z) • f z‖ ≤ C
filter_upwards [self_mem_nhdsWithin] with ε ε₀
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g : ℂ → E
z : ℂ
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
⊢ ‖exp (↑ε * z) • f z‖ ≤ C
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g : ℂ → E
z : ℂ
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε ∈ Iio 0
⊢ ‖exp (↑ε * z) • f z‖ ≤ C
change ε < 0 at ε₀
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g✝ : ℂ → E
z : ℂ
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z => exp (↑ε * z) • f z
⊢ ‖exp (↑ε * z) • f z‖ ≤ C
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g : ℂ → E
z : ℂ
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
⊢ ‖exp (↑ε * z) • f z‖ ≤ C
set g : ℂ → E := fun z => exp (ε * z) • f z
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g✝ : ℂ → E
z : ℂ
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z => exp (↑ε * z) • f z
⊢ ‖g z‖ ≤ C
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g✝ : ℂ → E
z : ℂ
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z => exp (↑ε * z) • f z
⊢ ‖exp (↑ε * z) • f z‖ ≤ C
change ‖g z‖ ≤ C
case hd
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g✝ : ℂ → E
z : ℂ
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z => exp (↑ε * z) • f z
⊢ DiffContOnCl ℂ g {z | 0 < z.re}

case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g✝ : ℂ → E
z : ℂ
hexp : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z => exp (↑ε * z) • f z
hd : DiffContOnCl ℂ g {z | 0 < z.re}
⊢ ‖g z‖ ≤ C
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g✝ : ℂ → E
z : ℂ
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z => exp (↑ε * z) • f z
⊢ ‖g z‖ ≤ C
replace hd : DiffContOnCl ℂ g {z : ℂ | 0 < z.re}
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g✝ : ℂ → E
z : ℂ
hexp : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z => exp (↑ε * z) • f z
hd : DiffContOnCl ℂ g {z | 0 < z.re}
⊢ ‖g z‖ ≤ C
case hd
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g✝ : ℂ → E
z : ℂ
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z => exp (↑ε * z) • f z
⊢ DiffContOnCl ℂ g {z | 0 < z.re}

case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g✝ : ℂ → E
z : ℂ
hexp : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z => exp (↑ε * z) • f z
hd : DiffContOnCl ℂ g {z | 0 < z.re}
⊢ ‖g z‖ ≤ C
exact (differentiable_id.const_mul _).cexp.diffContOnCl.smul hd
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g✝ : ℂ → E
z : ℂ
hexp : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z => exp (↑ε * z) • f z
hd : DiffContOnCl ℂ g {z | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
⊢ ‖g z‖ ≤ C
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g✝ : ℂ → E
z : ℂ
hexp : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z => exp (↑ε * z) • f z
hd : DiffContOnCl ℂ g {z | 0 < z.re}
⊢ ‖g z‖ ≤ C
have hgn : ∀ z, ‖g z‖ = expR (ε * z.re) * ‖f z‖ := fun z ↦ by
  rw [norm_smul, norm_eq_abs, abs_exp, ofReal_mul_re]
case h.refine'_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g✝ : ℂ → E
z : ℂ
hexp : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z => exp (↑ε * z) • f z
hd : DiffContOnCl ℂ g {z | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
⊢ ∃ c, c < 2 ∧ ∃ B, g =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)

case h.refine'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g✝ : ℂ → E
z : ℂ
hexp : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z => exp (↑ε * z) • f z
hd : DiffContOnCl ℂ g {z | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
⊢ Tendsto (fun x => g ↑x) atTop (𝓝 0)

case h.refine'_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g✝ : ℂ → E
z : ℂ
hexp : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z => exp (↑ε * z) • f z
hd : DiffContOnCl ℂ g {z | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
y : ℝ
⊢ ‖g (↑y * I)‖ ≤ C
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g✝ : ℂ → E
z : ℂ
hexp : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z => exp (↑ε * z) • f z
hd : DiffContOnCl ℂ g {z | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
⊢ ‖g z‖ ≤ C
refine' right_half_plane_of_tendsto_zero_on_real hd _ _ (fun y => _) hz
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g : ℂ → E
z : ℂ
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
this : ∀ᶠ (ε : ℝ) in 𝓝[Iio 0] 0, ‖exp (↑ε * z) • f z‖ ≤ C
⊢ Tendsto (fun c => ‖exp (↑c * z) • f z‖) (𝓝 0) (𝓝 ‖f z‖)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g : ℂ → E
z : ℂ
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
this : ∀ᶠ (ε : ℝ) in 𝓝[Iio 0] 0, ‖exp (↑ε * z) • f z‖ ≤ C
⊢ ‖f z‖ ≤ C
refine' le_of_tendsto (Tendsto.mono_left _ nhdsWithin_le_nhds) this
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g : ℂ → E
z : ℂ
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
this : ∀ᶠ (ε : ℝ) in 𝓝[Iio 0] 0, ‖exp (↑ε * z) • f z‖ ≤ C
⊢ ‖exp (↑0 * z) • f z‖ = ‖f z‖
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g : ℂ → E
z : ℂ
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
this : ∀ᶠ (ε : ℝ) in 𝓝[Iio 0] 0, ‖exp (↑ε * z) • f z‖ ≤ C
⊢ Tendsto (fun c => ‖exp (↑c * z) • f z‖) (𝓝 0) (𝓝 ‖f z‖)
apply ((continuous_ofReal.mul continuous_const).cexp.smul continuous_const).norm.tendsto'
no goals
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g : ℂ → E
z : ℂ
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
this : ∀ᶠ (ε : ℝ) in 𝓝[Iio 0] 0, ‖exp (↑ε * z) • f z‖ ≤ C
⊢ ‖exp (↑0 * z) • f z‖ = ‖f z‖
simp
no goals
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g✝ : ℂ → E
z✝ : ℂ
hexp : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z✝.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z => exp (↑ε * z) • f z
hd : DiffContOnCl ℂ g {z | 0 < z.re}
z : ℂ
⊢ ‖g z‖ = expR (ε * z.re) * ‖f z‖
rw [norm_smul, norm_eq_abs, abs_exp, ofReal_mul_re]
case h.refine'_1.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g✝ : ℂ → E
z : ℂ
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z => exp (↑ε * z) • f z
hd : DiffContOnCl ℂ g {z | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
⊢ ∃ c, c < 2 ∧ ∃ B, g =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
case h.refine'_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g✝ : ℂ → E
z : ℂ
hexp : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z => exp (↑ε * z) • f z
hd : DiffContOnCl ℂ g {z | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
⊢ ∃ c, c < 2 ∧ ∃ B, g =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
rcases hexp with ⟨c, hc, B, hO⟩
case h.refine'_1.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g✝ : ℂ → E
z : ℂ
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z => exp (↑ε * z) • f z
hd : DiffContOnCl ℂ g {z | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
⊢ ∀ᶠ (x : ℂ) in comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}, ‖g x‖ ≤ 1 * ‖f x‖
case h.refine'_1.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g✝ : ℂ → E
z : ℂ
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z => exp (↑ε * z) • f z
hd : DiffContOnCl ℂ g {z | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
⊢ ∃ c, c < 2 ∧ ∃ B, g =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
refine ⟨c, hc, B, (IsBigO.of_bound 1 ?_).trans hO⟩
case h.refine'_1.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g✝ : ℂ → E
z✝ : ℂ
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz✝ : 0 ≤ z✝.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z => exp (↑ε * z) • f z
hd : DiffContOnCl ℂ g {z | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
z : ℂ
hz : z ∈ {z | 0 < z.re}
⊢ ‖g z‖ ≤ 1 * ‖f z‖
case h.refine'_1.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g✝ : ℂ → E
z : ℂ
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z => exp (↑ε * z) • f z
hd : DiffContOnCl ℂ g {z | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
⊢ ∀ᶠ (x : ℂ) in comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}, ‖g x‖ ≤ 1 * ‖f x‖
refine' eventually_inf_principal.2 <| eventually_of_forall fun z hz => _
case h.refine'_1.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g✝ : ℂ → E
z✝ : ℂ
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz✝ : 0 ≤ z✝.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z => exp (↑ε * z) • f z
hd : DiffContOnCl ℂ g {z | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
z : ℂ
hz : z ∈ {z | 0 < z.re}
⊢ expR (ε * z.re) * ‖f z‖ ≤ ‖f z‖
case h.refine'_1.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g✝ : ℂ → E
z✝ : ℂ
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz✝ : 0 ≤ z✝.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z => exp (↑ε * z) • f z
hd : DiffContOnCl ℂ g {z | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
z : ℂ
hz : z ∈ {z | 0 < z.re}
⊢ ‖g z‖ ≤ 1 * ‖f z‖
rw [hgn, one_mul]
case h.refine'_1.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g✝ : ℂ → E
z✝ : ℂ
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz✝ : 0 ≤ z✝.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z => exp (↑ε * z) • f z
hd : DiffContOnCl ℂ g {z | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
z : ℂ
hz : z ∈ {z | 0 < z.re}
⊢ ε * z.re ≤ 0
case h.refine'_1.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g✝ : ℂ → E
z✝ : ℂ
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz✝ : 0 ≤ z✝.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z => exp (↑ε * z) • f z
hd : DiffContOnCl ℂ g {z | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
z : ℂ
hz : z ∈ {z | 0 < z.re}
⊢ expR (ε * z.re) * ‖f z‖ ≤ ‖f z‖
refine' mul_le_of_le_one_left (norm_nonneg _) (Real.exp_le_one_iff.2 _)
no goals
case h.refine'_1.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g✝ : ℂ → E
z✝ : ℂ
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz✝ : 0 ≤ z✝.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z => exp (↑ε * z) • f z
hd : DiffContOnCl ℂ g {z | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
z : ℂ
hz : z ∈ {z | 0 < z.re}
⊢ ε * z.re ≤ 0
exact mul_nonpos_of_nonpos_of_nonneg ε₀.le (le_of_lt hz)
case h.refine'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g✝ : ℂ → E
z : ℂ
hexp : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z => exp (↑ε * z) • f z
hd : DiffContOnCl ℂ g {z | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
⊢ Tendsto (fun x => expR (ε * x) • f ↑x) atTop (𝓝 0)
case h.refine'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g✝ : ℂ → E
z : ℂ
hexp : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z => exp (↑ε * z) • f z
hd : DiffContOnCl ℂ g {z | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
⊢ Tendsto (fun x => g ↑x) atTop (𝓝 0)
simp_rw [← ofReal_mul, ← ofReal_exp, coe_smul]
case h.refine'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g✝ : ℂ → E
z : ℂ
hexp : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z => exp (↑ε * z) • f z
hd : DiffContOnCl ℂ g {z | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
h₀ : Tendsto (fun x => expR (ε * x)) atTop (𝓝 0)
⊢ Tendsto (fun x => expR (ε * x) • f ↑x) atTop (𝓝 0)
case h.refine'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g✝ : ℂ → E
z : ℂ
hexp : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z => exp (↑ε * z) • f z
hd : DiffContOnCl ℂ g {z | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
⊢ Tendsto (fun x => expR (ε * x) • f ↑x) atTop (𝓝 0)
have h₀ : Tendsto (fun x : ℝ => expR (ε * x)) atTop (𝓝 0) :=
  Real.tendsto_exp_atBot.comp (tendsto_const_nhds.neg_mul_atTop ε₀ tendsto_id)
no goals
case h.refine'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g✝ : ℂ → E
z : ℂ
hexp : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z => exp (↑ε * z) • f z
hd : DiffContOnCl ℂ g {z | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
h₀ : Tendsto (fun x => expR (ε * x)) atTop (𝓝 0)
⊢ Tendsto (fun x => expR (ε * x) • f ↑x) atTop (𝓝 0)
exact h₀.zero_smul_isBoundedUnder_le hre
case h.refine'_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g✝ : ℂ → E
z : ℂ
hexp : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z => exp (↑ε * z) • f z
hd : DiffContOnCl ℂ g {z | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
y : ℝ
⊢ ‖f (↑y * I)‖ ≤ C
case h.refine'_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g✝ : ℂ → E
z : ℂ
hexp : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z => exp (↑ε * z) • f z
hd : DiffContOnCl ℂ g {z | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
y : ℝ
⊢ ‖g (↑y * I)‖ ≤ C
rw [hgn, ofReal_mul_re, I_re, mul_zero, mul_zero, Real.exp_zero,
  one_mul]
no goals
case h.refine'_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f g✝ : ℂ → E
z : ℂ
hexp : ∃ c, c < 2 ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ↑Complex.abs z ^ c)
hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z => exp (↑ε * z) • f z
hd : DiffContOnCl ℂ g {z | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
y : ℝ
⊢ ‖f (↑y * I)‖ ≤ C
exact him y