-- Mathlib/Analysis/Complex/Hadamard.lean
/-- When the function `f` is bounded above on a vertical strip, then so is `F`. -/
lemma F_BddAbove (f : ℂ → E) (ε : ℝ) (hε : ε > 0)
    (hB : BddAbove ((norm ∘ f) '' verticalClosedStrip 0 1)) :
    BddAbove ((norm ∘ (F f ε)) '' verticalClosedStrip 0 1)

Proof state:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
hB : ∀ y ∈ norm ∘ f '' verticalClosedStrip 0 1, y ≤ B
⊢ ∀
    y ∈
      (fun a => ‖((↑ε + ↑(sSupNormIm f 0)) ^ (a - 1) * (↑ε + ↑(sSupNormIm f 1)) ^ (-a)) • f a‖) ''
        verticalClosedStrip 0 1,
    y ≤ (1 ⊔ (ε + sSupNormIm f 0) ^ (-1)) * (1 ⊔ (ε + sSupNormIm f 1) ^ (-1)) * B

Tactic:
simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]

Result:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
hB : ∀ y ∈ norm ∘ f '' verticalClosedStrip 0 1, y ≤ B
⊢ ∀ a ∈ verticalClosedStrip 0 1,
    ‖((↑ε + ↑(sSupNormIm f 0)) ^ (a - 1) * (↑ε + ↑(sSupNormIm f 1)) ^ (-a)) • f a‖ ≤
      (1 ⊔ (ε + sSupNormIm f 0) ^ (-1)) * (1 ⊔ (ε + sSupNormIm f 1) ^ (-1)) * B

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hset : z ∈ verticalClosedStrip 0 1
hB : ‖f z‖ ≤ B
hM0_one : ε + sSupNormIm f 0 < 1
⊢ (ε + sSupNormIm f 0) ^ (z.re - 1) ≤ (ε + sSupNormIm f 0) ^ (-1)

Tactic:
apply Real.rpow_le_rpow_of_exponent_ge (sSupNormIm_eps_pos f hε 0) (le_of_lt hM0_one) _

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hset : z ∈ verticalClosedStrip 0 1
hB : ‖f z‖ ≤ B
hM0_one : ε + sSupNormIm f 0 < 1
⊢ -1 ≤ z.re - 1

Proof state:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hset : z ∈ verticalClosedStrip 0 1
hB : ‖f z‖ ≤ B
hM1_one : ε + sSupNormIm f 1 < 1
⊢ ‖↑(ε + sSupNormIm f 1) ^ (-z)‖ ≤ 1 ⊔ (ε + sSupNormIm f 1) ^ (-1)

Tactic:
apply le_trans _ (le_max_right _ _)

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hset : z ∈ verticalClosedStrip 0 1
hB : ‖f z‖ ≤ B
hM1_one : ε + sSupNormIm f 1 < 1
⊢ ‖↑(ε + sSupNormIm f 1) ^ (-z)‖ ≤ (ε + sSupNormIm f 1) ^ (-1)

Proof state:
case h.h₁.h₁
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hset : z ∈ verticalClosedStrip 0 1
hB : ‖f z‖ ≤ B
⊢ ‖↑(ε + sSupNormIm f 0) ^ (z - 1)‖ ≤ 1 ⊔ (ε + sSupNormIm f 0) ^ (-1)

Tactic:
by_cases hM0_one : 1 ≤ ε + sSupNormIm f 0

Result:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hset : z ∈ verticalClosedStrip 0 1
hB : ‖f z‖ ≤ B
hM0_one : 1 ≤ ε + sSupNormIm f 0
⊢ ‖↑(ε + sSupNormIm f 0) ^ (z - 1)‖ ≤ 1 ⊔ (ε + sSupNormIm f 0) ^ (-1)

case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hset : z ∈ verticalClosedStrip 0 1
hB : ‖f z‖ ≤ B
hM0_one : ¬1 ≤ ε + sSupNormIm f 0
⊢ ‖↑(ε + sSupNormIm f 0) ^ (z - 1)‖ ≤ 1 ⊔ (ε + sSupNormIm f 0) ^ (-1)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hset : z ∈ verticalClosedStrip 0 1
hB : ‖f z‖ ≤ B
hM1_one : ε + sSupNormIm f 1 < 1
⊢ ‖↑(ε + sSupNormIm f 1) ^ (-z)‖ ≤ (ε + sSupNormIm f 1) ^ (-1)

Tactic:
simp only [norm_cpow_eq_rpow_re_of_pos (sSupNormIm_eps_pos f hε 1), sub_re,
  one_re, neg_re, Real.rpow_le_rpow_of_exponent_ge (sSupNormIm_eps_pos f hε 1)
  (le_of_lt hM1_one) (neg_le_neg_iff.mpr hset.2)]

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
hB : ∃ x, ∀ y ∈ norm ∘ f '' verticalClosedStrip 0 1, y ≤ x
⊢ ∃ x,
    ∀
      y ∈
        (fun a => ‖((↑ε + ↑(sSupNormIm f 0)) ^ (a - 1) * (↑ε + ↑(sSupNormIm f 1)) ^ (-a)) • f a‖) ''
          verticalClosedStrip 0 1,
      y ≤ x

Tactic:
rcases hB with ⟨B, hB⟩

Result:
case intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
hB : ∀ y ∈ norm ∘ f '' verticalClosedStrip 0 1, y ≤ B
⊢ ∃ x,
    ∀
      y ∈
        (fun a => ‖((↑ε + ↑(sSupNormIm f 0)) ^ (a - 1) * (↑ε + ↑(sSupNormIm f 1)) ^ (-a)) • f a‖) ''
          verticalClosedStrip 0 1,
      y ≤ x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hset : z ∈ verticalClosedStrip 0 1
hB : ‖f z‖ ≤ B
hM0_one : ε + sSupNormIm f 0 < 1
⊢ ‖↑(ε + sSupNormIm f 0) ^ (z - 1)‖ ≤ (ε + sSupNormIm f 0) ^ (-1)

Tactic:
simp only [norm_cpow_eq_rpow_re_of_pos (sSupNormIm_eps_pos f hε 0), sub_re,
  one_re]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hset : z ∈ verticalClosedStrip 0 1
hB : ‖f z‖ ≤ B
hM0_one : ε + sSupNormIm f 0 < 1
⊢ (ε + sSupNormIm f 0) ^ (z.re - 1) ≤ (ε + sSupNormIm f 0) ^ (-1)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
⊢ BddAbove
    ((fun a => ‖((↑ε + ↑(sSupNormIm f 0)) ^ (a - 1) * (↑ε + ↑(sSupNormIm f 1)) ^ (-a)) • f a‖) ''
      verticalClosedStrip 0 1)

Tactic:
rw [bddAbove_def] at *

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
hB : ∃ x, ∀ y ∈ norm ∘ f '' verticalClosedStrip 0 1, y ≤ x
⊢ ∃ x,
    ∀
      y ∈
        (fun a => ‖((↑ε + ↑(sSupNormIm f 0)) ^ (a - 1) * (↑ε + ↑(sSupNormIm f 1)) ^ (-a)) • f a‖) ''
          verticalClosedStrip 0 1,
      y ≤ x

Proof state:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hset : z ∈ verticalClosedStrip 0 1
hB : ‖f z‖ ≤ B
hM0_one : ¬1 ≤ ε + sSupNormIm f 0
⊢ ‖↑(ε + sSupNormIm f 0) ^ (z - 1)‖ ≤ 1 ⊔ (ε + sSupNormIm f 0) ^ (-1)

Tactic:
rw [not_le] at hM0_one

Result:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hset : z ∈ verticalClosedStrip 0 1
hB : ‖f z‖ ≤ B
hM0_one : ε + sSupNormIm f 0 < 1
⊢ ‖↑(ε + sSupNormIm f 0) ^ (z - 1)‖ ≤ 1 ⊔ (ε + sSupNormIm f 0) ^ (-1)

Proof state:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hset : z ∈ verticalClosedStrip 0 1
hB : ‖f z‖ ≤ B
hM0_one : 1 ≤ ε + sSupNormIm f 0
⊢ ‖↑(ε + sSupNormIm f 0) ^ (z - 1)‖ ≤ 1 ⊔ (ε + sSupNormIm f 0) ^ (-1)

Tactic:
apply le_trans _ (le_max_left _ _)

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hset : z ∈ verticalClosedStrip 0 1
hB : ‖f z‖ ≤ B
hM0_one : 1 ≤ ε + sSupNormIm f 0
⊢ ‖↑(ε + sSupNormIm f 0) ^ (z - 1)‖ ≤ 1

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hset : z ∈ verticalClosedStrip 0 1
hB : ‖f z‖ ≤ B
hM0_one : 1 ≤ ε + sSupNormIm f 0
⊢ ‖↑(ε + sSupNormIm f 0) ^ (z - 1)‖ ≤ 1

Tactic:
simp only [norm_cpow_eq_rpow_re_of_pos (sSupNormIm_eps_pos f hε 0), sub_re,
  one_re, Real.rpow_le_one_of_one_le_of_nonpos hM0_one (sub_nonpos.mpr hset.2)]

Result:
no goals

Proof state:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hset : z ∈ verticalClosedStrip 0 1
hB : ‖f z‖ ≤ B
hM1_one : 1 ≤ ε + sSupNormIm f 1
⊢ ‖↑(ε + sSupNormIm f 1) ^ (-z)‖ ≤ 1 ⊔ (ε + sSupNormIm f 1) ^ (-1)

Tactic:
apply le_trans _ (le_max_left _ _)

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hset : z ∈ verticalClosedStrip 0 1
hB : ‖f z‖ ≤ B
hM1_one : 1 ≤ ε + sSupNormIm f 1
⊢ ‖↑(ε + sSupNormIm f 1) ^ (-z)‖ ≤ 1