-- 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
z : ℂ
hset : z ∈ verticalClosedStrip 0 1
⊢ ‖((↑ε + ↑(sSupNormIm f 0)) ^ (z - 1) * (↑ε + ↑(sSupNormIm f 1)) ^ (-z)) • f z‖ ≤
    (1 ⊔ (ε + sSupNormIm f 0) ^ (-1)) * (1 ⊔ (ε + sSupNormIm f 1) ^ (-1)) * B

Tactic:
specialize hB (‖f z‖) (by simpa [image_congr, mem_image, comp_apply] using ⟨z, hset, rfl⟩)

Result:
case 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) * (↑ε + ↑(sSupNormIm f 1)) ^ (-z)) • f z‖ ≤
    (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
⊢ -1 ≤ z.re - 1

Tactic:
simp only [neg_le_sub_iff_le_add, le_add_iff_nonneg_left, hset.1]

Result:
no goals

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 1) ^ (-z)‖ ≤ 1 ⊔ (ε + sSupNormIm f 1) ^ (-1)

Tactic:
by_cases hM1_one : 1 ≤ ε + sSupNormIm f 1

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
hM1_one : 1 ≤ ε + sSupNormIm f 1
⊢ ‖↑(ε + sSupNormIm f 1) ^ (-z)‖ ≤ 1 ⊔ (ε + sSupNormIm f 1) ^ (-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
hM1_one : ¬1 ≤ ε + sSupNormIm f 1
⊢ ‖↑(ε + sSupNormIm f 1) ^ (-z)‖ ≤ 1 ⊔ (ε + sSupNormIm f 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
hM1_one : 1 ≤ ε + sSupNormIm f 1
⊢ ‖↑(ε + sSupNormIm f 1) ^ (-z)‖ ≤ 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_one_of_one_le_of_nonpos
  hM1_one (Right.neg_nonpos_iff.mpr hset.1)]

Result:
no goals

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 : ¬1 ≤ ε + sSupNormIm f 1
⊢ ‖↑(ε + sSupNormIm f 1) ^ (-z)‖ ≤ 1 ⊔ (ε + sSupNormIm f 1) ^ (-1)

Tactic:
rw [not_le] at hM1_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
hM1_one : ε + sSupNormIm f 1 < 1
⊢ ‖↑(ε + sSupNormIm f 1) ^ (-z)‖ ≤ 1 ⊔ (ε + sSupNormIm f 1) ^ (-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 (norm ∘ F f ε '' verticalClosedStrip 0 1)

Tactic:
simp only [F, image_congr, comp_apply, map_mul, invInterpStrip]

Result:
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)

Proof state:
case 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)‖ * ‖↑(ε + sSupNormIm f 1) ^ (-z)‖ * ‖f z‖ ≤
    (1 ⊔ (ε + sSupNormIm f 0) ^ (-1)) * (1 ⊔ (ε + sSupNormIm f 1) ^ (-1)) * B

Tactic:
gcongr

Result:
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)

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 1) ^ (-z)‖ ≤ 1 ⊔ (ε + sSupNormIm f 1) ^ (-1)

Proof state:
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

Tactic:
use ((max 1 ((ε + sSupNormIm f 0) ^ (-(1 : ℝ)))) * max 1 ((ε + sSupNormIm f 1) ^ (-(1 : ℝ)))) * B

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
⊢ ∀
    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

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
⊢ ∀ 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

Tactic:
intros z hset

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
z : ℂ
hset : z ∈ verticalClosedStrip 0 1
⊢ ‖((↑ε + ↑(sSupNormIm f 0)) ^ (z - 1) * (↑ε + ↑(sSupNormIm f 1)) ^ (-z)) • f z‖ ≤
    (1 ⊔ (ε + sSupNormIm f 0) ^ (-1)) * (1 ⊔ (ε + sSupNormIm f 1) ^ (-1)) * B

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 : ε + sSupNormIm f 0 < 1
⊢ ‖↑(ε + sSupNormIm f 0) ^ (z - 1)‖ ≤ 1 ⊔ (ε + sSupNormIm f 0) ^ (-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
hM0_one : ε + sSupNormIm f 0 < 1
⊢ ‖↑(ε + sSupNormIm f 0) ^ (z - 1)‖ ≤ (ε + sSupNormIm f 0) ^ (-1)

Proof state:
case 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) * (↑ε + ↑(sSupNormIm f 1)) ^ (-z)) • f z‖ ≤
    (1 ⊔ (ε + sSupNormIm f 0) ^ (-1)) * (1 ⊔ (ε + sSupNormIm f 1) ^ (-1)) * B

Tactic:
simp only [norm_smul, norm_mul, ← ofReal_add]

Result:
case 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)‖ * ‖↑(ε + sSupNormIm f 1) ^ (-z)‖ * ‖f z‖ ≤
    (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 : ℝ
hB : ∀ y ∈ norm ∘ f '' verticalClosedStrip 0 1, y ≤ B
z : ℂ
hset : z ∈ verticalClosedStrip 0 1
⊢ ‖f z‖ ∈ norm ∘ f '' verticalClosedStrip 0 1

Tactic:
simpa [image_congr, mem_image, comp_apply] using ⟨z, hset, rfl⟩

Result:
no goals