awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
hB : ∃ (x : ℝ), ∀ y ∈ norm ∘ f '' verticalClosedStrip 0 1, y ≤ x
⊢ ∃ (x : ℝ),
    ∀ (y : ℝ),
      Membership.mem (γ := Set ℝ)
          ((fun (a : ℂ) ↦
              ‖(((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (a - 1) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ (-a)) • f a‖) ''
            verticalClosedStrip 0 1)
          y →
        y ≤ x
have rcases : ∀ (B : ℝ) (hB : ∀ y ∈ norm ∘ f '' verticalClosedStrip 0 1, y ≤ B),
  ∃ (x : ℝ),
    ∀ (y : ℝ),
      Membership.mem (γ := Set ℝ)
          ((fun (a : ℂ) ↦
              ‖(((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (a - 1) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ (-a)) • f a‖) ''
            verticalClosedStrip 0 1)
          y →
        y ≤ x
Tactic: rcases hB with ⟨B, hB⟩
Cleared hypotheses: hB
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
hB : ∀ y ∈ norm ∘ f '' verticalClosedStrip 0 1, y ≤ B
⊢ ∃ (x : ℝ),
    ∀ (y : ℝ),
      Membership.mem (γ := Set ℝ)
          ((fun (a : ℂ) ↦
              ‖(((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (a - 1) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ (-a)) • f a‖) ''
            verticalClosedStrip 0 1)
          y →
        y ≤ x
have h : ∀ (y : ℝ),
  Membership.mem (γ := Set ℝ)
      ((fun (a : ℂ) ↦
          ‖(((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (a - 1) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ (-a)) • f a‖) ''
        verticalClosedStrip 0 1)
      y →
    y ≤ max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 0) (-1)) * max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 1) (-1)) * B
Tactic: use ((max 1 ((ε + sSupNormIm f 0) ^ (-(1 : ℝ)))) * max 1 ((ε + sSupNormIm f 1) ^ (-(1 : ℝ)))) * B
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
hB : ∀ y ∈ norm ∘ f '' verticalClosedStrip 0 1, y ≤ B
⊢ ∀ (y : ℝ),
    Membership.mem (γ := Set ℝ)
        ((fun (a : ℂ) ↦
            ‖(((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (a - 1) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ (-a)) • f a‖) ''
          verticalClosedStrip 0 1)
        y →
      y ≤
        max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 0) (-1)) * max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 1) (-1)) * B
have h : ∀ a ∈ verticalClosedStrip 0 1,
  ‖(((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (a - 1) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ (-a)) • f a‖ ≤
    max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 0) (-1)) * max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 1) (-1)) * B
Tactic: simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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‖ ≤
    max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 0) (-1)) * max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 1) (-1)) * B
have hB₁ : ‖f z‖ ≤ B
Tactic: specialize hB (‖f z‖) (by simpa [image_congr, mem_image, comp_apply] using ⟨z, hset, rfl⟩)
Cleared hypotheses: hB
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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‖ ≤
    max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 0) (-1)) * max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 1) (-1)) * B
have h : ‖(↑(ε + sSupNormIm f 0) : ℂ) ^ (z - 1)‖ * ‖(↑(ε + sSupNormIm f 1) : ℂ) ^ (-z)‖ * ‖f z‖ ≤
  max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 0) (-1)) * max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 1) (-1)) * B
Tactic: simp only [norm_smul, norm_mul, ← ofReal_add]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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‖ ≤
    max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 0) (-1)) * max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 1) (-1)) * B
have h : ‖(↑(ε + sSupNormIm f 0) : ℂ) ^ (z - 1)‖ ≤ max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 0) (-1))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hset : z ∈ verticalClosedStrip 0 1
hB : ‖f z‖ ≤ B
h : ‖(↑(ε + sSupNormIm f 0) : ℂ) ^ (z - 1)‖ ≤ max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 0) (-1))
⊢ ‖(↑(ε + sSupNormIm f 0) : ℂ) ^ (z - 1)‖ * ‖(↑(ε + sSupNormIm f 1) : ℂ) ^ (-z)‖ * ‖f z‖ ≤
    max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 0) (-1)) * max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 1) (-1)) * B
have h₁ : ‖(↑(ε + sSupNormIm f 1) : ℂ) ^ (-z)‖ ≤ max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 1) (-1))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hset : z ∈ verticalClosedStrip 0 1
hB : ‖f z‖ ≤ B
⊢ ‖(↑(ε + sSupNormIm f 0) : ℂ) ^ (z - 1)‖ ≤ max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 0) (-1))
have pos : ∀ (hM0_one : 1 ≤ ε + sSupNormIm f 0),
  ‖(↑(ε + sSupNormIm f 0) : ℂ) ^ (z - 1)‖ ≤ max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 0) (-1))
Tactic: by_cases hM0_one : 1 ≤ ε + sSupNormIm f 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hset : z ∈ verticalClosedStrip 0 1
hB : ‖f z‖ ≤ B
pos :
  ∀ (hM0_one : 1 ≤ ε + sSupNormIm f 0),
    ‖(↑(ε + sSupNormIm f 0) : ℂ) ^ (z - 1)‖ ≤ max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 0) (-1))
⊢ ‖(↑(ε + sSupNormIm f 0) : ℂ) ^ (z - 1)‖ ≤ max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 0) (-1))
have neg : ∀ (hM0_one : ¬1 ≤ ε + sSupNormIm f 0),
  ‖(↑(ε + sSupNormIm f 0) : ℂ) ^ (z - 1)‖ ≤ max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 0) (-1))
Tactic: by_cases hM0_one : 1 ≤ ε + sSupNormIm f 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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)‖ ≤ max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 0) (-1))
have apply : ‖(↑(ε + sSupNormIm f 0) : ℂ) ^ (z - 1)‖ ≤ 1
Tactic: apply le_trans _ (le_max_left _ _)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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)‖ ≤ max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 0) (-1))
have hM0_one₁ : ε + sSupNormIm f 0 < 1
Tactic: rw [not_le] at hM0_one
Cleared hypotheses: hM0_one
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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)‖ ≤ max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 0) (-1))
have apply : ‖(↑(ε + sSupNormIm f 0) : ℂ) ^ (z - 1)‖ ≤ HPow.hPow (β := ℝ) (ε + sSupNormIm f 0) (-1)
Tactic: apply le_trans _ (le_max_right _ _)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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)‖ ≤ HPow.hPow (β := ℝ) (ε + sSupNormIm f 0) (-1)
have simp : (ε + sSupNormIm f 0) ^ (z.re - 1) ≤ HPow.hPow (β := ℝ) (ε + sSupNormIm f 0) (-1)
Tactic: simp only [norm_cpow_eq_rpow_re_of_pos (sSupNormIm_eps_pos f hε 0), sub_re,
        one_re]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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) ≤ HPow.hPow (β := ℝ) (ε + sSupNormIm f 0) (-1)
have apply : -1 ≤ z.re - 1
Tactic: apply Real.rpow_le_rpow_of_exponent_ge (sSupNormIm_eps_pos f hε 0) (le_of_lt hM0_one) _
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hset : z ∈ verticalClosedStrip 0 1
hB : ‖f z‖ ≤ B
⊢ ‖(↑(ε + sSupNormIm f 1) : ℂ) ^ (-z)‖ ≤ max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 1) (-1))
have pos : ∀ (hM1_one : 1 ≤ ε + sSupNormIm f 1),
  ‖(↑(ε + sSupNormIm f 1) : ℂ) ^ (-z)‖ ≤ max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 1) (-1))
Tactic: by_cases hM1_one : 1 ≤ ε + sSupNormIm f 1
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hset : z ∈ verticalClosedStrip 0 1
hB : ‖f z‖ ≤ B
pos :
  ∀ (hM1_one : 1 ≤ ε + sSupNormIm f 1),
    ‖(↑(ε + sSupNormIm f 1) : ℂ) ^ (-z)‖ ≤ max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 1) (-1))
⊢ ‖(↑(ε + sSupNormIm f 1) : ℂ) ^ (-z)‖ ≤ max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 1) (-1))
have neg : ∀ (hM1_one : ¬1 ≤ ε + sSupNormIm f 1),
  ‖(↑(ε + sSupNormIm f 1) : ℂ) ^ (-z)‖ ≤ max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 1) (-1))
Tactic: by_cases hM1_one : 1 ≤ ε + sSupNormIm f 1
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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)‖ ≤ max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 1) (-1))
have apply : ‖(↑(ε + sSupNormIm f 1) : ℂ) ^ (-z)‖ ≤ 1
Tactic: apply le_trans _ (le_max_left _ _)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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)‖ ≤ max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 1) (-1))
have hM1_one₁ : ε + sSupNormIm f 1 < 1
Tactic: rw [not_le] at hM1_one
Cleared hypotheses: hM1_one
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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)‖ ≤ max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 1) (-1))
have apply : ‖(↑(ε + sSupNormIm f 1) : ℂ) ^ (-z)‖ ≤ HPow.hPow (β := ℝ) (ε + sSupNormIm f 1) (-1)
Tactic: apply le_trans _ (le_max_right _ _)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ re ⁻¹' {0, 1}
⊢ ‖F f ε z‖ ≤ 1
have simp : (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re) * ‖f z‖ ≤ 1
Tactic: simp only [F, norm_smul, norm_invInterpStrip f z hε]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ re ⁻¹' {0, 1}
⊢ (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re) * ‖f z‖ ≤ 1
have inl : ∀ (hz0 : z.re = 0), (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re) * ‖f z‖ ≤ 1
Tactic: rcases hz with hz0 | hz1
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ re ⁻¹' {0, 1}
inl : ∀ (hz0 : z.re = 0), (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re) * ‖f z‖ ≤ 1
⊢ (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re) * ‖f z‖ ≤ 1
have inr : ∀ (hz1 : Membership.mem (γ := Set ℝ) {1} z.re),
  (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re) * ‖f z‖ ≤ 1
Tactic: rcases hz with hz0 | hz1
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz0 : z.re = 0
⊢ (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re) * ‖f z‖ ≤ 1
have inl : ‖f z‖ ≤ ε + sSupNormIm f 0
Tactic: simp only [hz0, zero_sub, Real.rpow_neg_one, neg_zero, Real.rpow_zero, mul_one,
      inv_mul_le_iff₀ (sSupNormIm_eps_pos f hε 0)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz0 : z.re = 0
⊢ ‖f z‖ ≤ ε + sSupNormIm f 0
have inl : ‖f z‖ ≤ ε + sSupNormIm f z.re
Tactic: rw [← hz0]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz0 : z.re = 0
⊢ ‖f z‖ ≤ ε + sSupNormIm f z.re
have apply : z ∈ verticalClosedStrip 0 1
Tactic: apply le_of_lt (norm_lt_sSupNormIm_eps f ε hε _ _ hB)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz1 : Membership.mem (γ := Set ℝ) {1} z.re
⊢ (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re) * ‖f z‖ ≤ 1
have hz1₁ : z.re = 1
Tactic: rw [mem_singleton_iff] at hz1
Cleared hypotheses: hz1
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz1 : z.re = 1
⊢ (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re) * ‖f z‖ ≤ 1
have inr : ‖f z‖ ≤ ε + sSupNormIm f 1
Tactic: simp only [hz1, one_mul, Real.rpow_zero, sub_self, Real.rpow_neg_one,
      inv_mul_le_iff₀ (sSupNormIm_eps_pos f hε 1), mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz1 : z.re = 1
⊢ ‖f z‖ ≤ ε + sSupNormIm f 1
have inr : ‖f z‖ ≤ ε + sSupNormIm f z.re
Tactic: rw [← hz1]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz1 : z.re = 1
⊢ ‖f z‖ ≤ ε + sSupNormIm f z.re
have apply : z ∈ verticalClosedStrip 0 1
Tactic: apply le_of_lt (norm_lt_sSupNormIm_eps f ε hε _ _ hB)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : 0 < ε
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
⊢ ‖F f ε z‖ ≤ 1
have apply : ∃ c < Real.pi / HSub.hSub (α := ℝ) 1 0,
  ∃ (B : ℝ),
    Asymptotics.IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1))
      (fun (x : ℂ) ↦ invInterpStrip f x ε • f x) fun (z : ℂ) ↦ Real.exp (B * Real.exp (c * |z.im|))
Tactic: apply PhragmenLindelof.vertical_strip
    (DiffContOnCl.smul (diffContOnCl_invInterpStrip f hε) hd) _
    (fun x hx ↦ F_edge_le_one f ε hε x hB (Or.inl hx))
    (fun x hx ↦ F_edge_le_one f ε hε x hB (Or.inr hx)) hz.1 hz.2
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : 0 < ε
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
⊢ ∃ c < Real.pi / HSub.hSub (α := ℝ) 1 0,
    ∃ (B : ℝ),
      Asymptotics.IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1))
        (fun (x : ℂ) ↦ invInterpStrip f x ε • f x) fun (z : ℂ) ↦ Real.exp (B * Real.exp (c * |z.im|))
have h : 0 < Real.pi / HSub.hSub (α := ℝ) 1 0 ∧
  ∃ (B : ℝ),
    Asymptotics.IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1))
      (fun (x : ℂ) ↦ invInterpStrip f x ε • f x) fun (z : ℂ) ↦ Real.exp (B * Real.exp (0 * |z.im|))
Tactic: use 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : 0 < ε
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
⊢ 0 < Real.pi / HSub.hSub (α := ℝ) 1 0 ∧
    ∃ (B : ℝ),
      Asymptotics.IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1))
        (fun (x : ℂ) ↦ invInterpStrip f x ε • f x) fun (z : ℂ) ↦ Real.exp (B * Real.exp (0 * |z.im|))
have h : 0 < Real.pi ∧
  ∃ (B : ℝ),
    Asymptotics.IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1))
      (fun (x : ℂ) ↦ invInterpStrip f x ε • f x) fun (z : ℂ) ↦ Real.exp (B * Real.exp (0 * |z.im|))
Tactic: rw [sub_zero, div_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : 0 < ε
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
⊢ 0 < Real.pi ∧
    ∃ (B : ℝ),
      Asymptotics.IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1))
        (fun (x : ℂ) ↦ invInterpStrip f x ε • f x) fun (z : ℂ) ↦ Real.exp (B * Real.exp (0 * |z.im|))
have h : ∃ (B : ℝ),
  Asymptotics.IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1))
    (fun (x : ℂ) ↦ invInterpStrip f x ε • f x) fun (z : ℂ) ↦ Real.exp (B * Real.exp (0 * |z.im|))
Tactic: refine ⟨ Real.pi_pos, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : 0 < ε
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
⊢ ∃ (B : ℝ),
    Asymptotics.IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1))
      (fun (x : ℂ) ↦ invInterpStrip f x ε • f x) fun (z : ℂ) ↦ Real.exp (B * Real.exp (0 * |z.im|))
have h : ∀ (BF : ℝ) (hBF : BF ∈ upperBounds (norm ∘ F f ε '' verticalClosedStrip 0 1)),
  ∃ (B : ℝ),
    Asymptotics.IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1))
      (fun (x : ℂ) ↦ invInterpStrip f x ε • f x) fun (z : ℂ) ↦ Real.exp (B * Real.exp (0 * |z.im|))
Tactic: obtain ⟨BF, hBF⟩ := F_BddAbove f ε hε hB
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : 0 < ε
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
BF : ℝ
hBF : BF ∈ upperBounds (norm ∘ F f ε '' verticalClosedStrip 0 1)
⊢ ∃ (B : ℝ),
    Asymptotics.IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1))
      (fun (x : ℂ) ↦ invInterpStrip f x ε • f x) fun (z : ℂ) ↦ Real.exp (B * Real.exp (0 * |z.im|))
have hBF₁ : ∀ a ∈ verticalClosedStrip 0 1, ‖F f ε a‖ ≤ BF
Tactic: simp only [comp_apply, mem_upperBounds, mem_image, forall_exists_index, and_imp,
    forall_apply_eq_imp_iff₂] at hBF
Cleared hypotheses: hBF
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : 0 < ε
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
BF : ℝ
hBF : ∀ a ∈ verticalClosedStrip 0 1, ‖F f ε a‖ ≤ BF
⊢ ∃ (B : ℝ),
    Asymptotics.IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1))
      (fun (x : ℂ) ↦ invInterpStrip f x ε • f x) fun (z : ℂ) ↦ Real.exp (B * Real.exp (0 * |z.im|))
have h : Asymptotics.IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1))
  (fun (x : ℂ) ↦ invInterpStrip f x ε • f x) fun (z : ℂ) ↦ Real.exp (BF * Real.exp (0 * |z.im|))
Tactic: use BF
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : 0 < ε
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
BF : ℝ
hBF : ∀ a ∈ verticalClosedStrip 0 1, ‖F f ε a‖ ≤ BF
⊢ Asymptotics.IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1))
    (fun (x : ℂ) ↦ invInterpStrip f x ε • f x) fun (z : ℂ) ↦ Real.exp (BF * Real.exp (0 * |z.im|))
have h : ∃ (c : ℝ),
  ∀ᶠ (x : ℂ) in comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1),
    ‖invInterpStrip f x ε • f x‖ ≤ c * ‖Real.exp (BF * Real.exp (0 * |x.im|))‖
Tactic: rw [Asymptotics.isBigO_iff]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : 0 < ε
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
BF : ℝ
hBF : ∀ a ∈ verticalClosedStrip 0 1, ‖F f ε a‖ ≤ BF
⊢ ∃ (c : ℝ),
    ∀ᶠ (x : ℂ) in comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1),
      ‖invInterpStrip f x ε • f x‖ ≤ c * ‖Real.exp (BF * Real.exp (0 * |x.im|))‖
have h : ∀ᶠ (x : ℂ) in comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1),
  ‖invInterpStrip f x ε • f x‖ ≤ 1 * ‖Real.exp (BF * Real.exp (0 * |x.im|))‖
Tactic: use 1
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : 0 < ε
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
BF : ℝ
hBF : ∀ a ∈ verticalClosedStrip 0 1, ‖F f ε a‖ ≤ BF
⊢ ∀ᶠ (x : ℂ) in comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1),
    ‖invInterpStrip f x ε • f x‖ ≤ 1 * ‖Real.exp (BF * Real.exp (0 * |x.im|))‖
have h : ∀ᶠ (x : ℂ) in comap (abs ∘ im) atTop,
  x ∈ re ⁻¹' Ioo 0 1 → ‖invInterpStrip f x ε • f x‖ ≤ 1 * ‖Real.exp (BF * Real.exp (0 * |x.im|))‖
Tactic: rw [eventually_inf_principal]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : 0 < ε
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
BF : ℝ
hBF : ∀ a ∈ verticalClosedStrip 0 1, ‖F f ε a‖ ≤ BF
⊢ ∀ᶠ (x : ℂ) in comap (abs ∘ im) atTop,
    x ∈ re ⁻¹' Ioo 0 1 → ‖invInterpStrip f x ε • f x‖ ≤ 1 * ‖Real.exp (BF * Real.exp (0 * |x.im|))‖
have h : ∀ x ∈ re ⁻¹' Ioo 0 1, ‖invInterpStrip f x ε • f x‖ ≤ 1 * ‖Real.exp (BF * Real.exp (0 * |x.im|))‖
Tactic: apply Eventually.of_forall