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
f : ℂ → E
l u : ℝ
hul : l < u
e : E
h : ∃ (x : ℂ), x.re = u ∧ f x = e
⊢ ∃ (x : ℂ), x.re = 1 ∧ f ((↑l : ℂ) + x * ((↑u : ℂ) - (↑l : ℂ))) = e
have h₁ : ∀ (z : ℂ) (hz₁ : z.re = u) (hz₂ : f z = e), ∃ (x : ℂ), x.re = 1 ∧ f ((↑l : ℂ) + x * ((↑u : ℂ) - (↑l : ℂ))) = e
Tactic: obtain ⟨z, hz₁, hz₂⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = u
hz₂ : f z = e
⊢ ∃ (x : ℂ), x.re = 1 ∧ f ((↑l : ℂ) + x * ((↑u : ℂ) - (↑l : ℂ))) = e
have h : ((z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ))).re = 1 ∧
  f ((↑l : ℂ) + (z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ)) * ((↑u : ℂ) - (↑l : ℂ))) = e
Tactic: use ((z - l) / (u - l))
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = u
hz₂ : f z = e
⊢ ((z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ))).re = 1 ∧
    f ((↑l : ℂ) + (z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ)) * ((↑u : ℂ) - (↑l : ℂ))) = e
have h : ((z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ))).re = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = u
hz₂ : f z = e
h : ((z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ))).re = 1
⊢ ((z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ))).re = 1 ∧
    f ((↑l : ℂ) + (z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ)) * ((↑u : ℂ) - (↑l : ℂ))) = e
have h₁ : f ((↑l : ℂ) + (z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ)) * ((↑u : ℂ) - (↑l : ℂ))) = e
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = u
hz₂ : f z = e
⊢ ((z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ))).re = 1
have h : ((z - (↑l : ℂ)) / (↑(u - l) : ℂ)).re = 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = u
hz₂ : f z = e
⊢ (↑u : ℂ) - (↑l : ℂ) ≠ 0
have norm_cast : ¬u - l = 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = u
hz₂ : f z = e
⊢ ¬u - l = 0
have linarith : u - l = 0 → l - u + (u - l - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = u
hz₂ : f z = e
⊢ f ((↑l : ℂ) + (z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ)) * ((↑u : ℂ) - (↑l : ℂ))) = e
have h : f ((↑l : ℂ) + 1 * (z - (↑l : ℂ))) = e
Tactic: rw [div_mul_comm, div_self (by norm_cast; linarith)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
⊢ sSup (norm '' scale f l u '' re ⁻¹' {1}) = sSup (norm '' f '' re ⁻¹' {u})
have this : scale f l u '' re ⁻¹' {1} = f '' re ⁻¹' {u}
Tactic: have : scale f l u '' re ⁻¹' {1} = f '' re ⁻¹' {u} := by
    ext e
    simp only [scale, smul_eq_mul, mem_image, mem_preimage, mem_singleton_iff]
    constructor
    · intro h
      obtain ⟨z, hz₁, hz₂⟩ := h
      use ↑l + z * (↑u - ↑l)
      simp only [add_re, ofReal_re, mul_re, hz₁, sub_re, one_mul, sub_im, ofReal_im, sub_self,
        mul_zero, sub_zero, add_sub_cancel, hz₂, and_self]
    · intro h
      obtain ⟨z, hz₁, hz₂⟩ := h
      use ((z - l) / (u - l))
      constructor
      · norm_cast
        grind [Complex.div_re, Complex.normSq_ofReal, sub_re, ofReal_re, ofReal_im, mul_eq_zero]
      · rw [div_mul_comm, div_self (by norm_cast; linarith)]
        simp only [one_mul, add_sub_cancel, hz₂]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
this : scale f l u '' re ⁻¹' {1} = f '' re ⁻¹' {u}
⊢ sSup (norm '' scale f l u '' re ⁻¹' {1}) = sSup (norm '' f '' re ⁻¹' {u})
have rw : sSup (norm '' f '' re ⁻¹' {u}) = sSup (norm '' f '' re ⁻¹' {u})
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
z : ℂ
⊢ (if sSupNormIm (scale f l u) 0 = 0 ∨ sSupNormIm (scale f l u) 1 = 0 then 0
    else
      (↑(sSupNormIm (scale f l u) 0) : ℂ) ^ (1 - (z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ))) *
        (↑(sSupNormIm (scale f l u) 1) : ℂ) ^ ((z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ)))) =
    if sSupNormIm f l = 0 ∨ sSupNormIm f u = 0 then 0
    else
      (↑(sSupNormIm f l) : ℂ) ^ (1 - (z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ))) *
        (↑(sSupNormIm f u) : ℂ) ^ ((z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ)))
have simp_rw : (if sSupNormIm f l = 0 ∨ sSupNormIm (scale f l u) 1 = 0 then 0
  else
    (↑(sSupNormIm f l) : ℂ) ^ (1 - (z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ))) *
      (↑(sSupNormIm (scale f l u) 1) : ℂ) ^ ((z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ)))) =
  if sSupNormIm f l = 0 ∨ sSupNormIm f u = 0 then 0
  else
    (↑(sSupNormIm f l) : ℂ) ^ (1 - (z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ))) *
      (↑(sSupNormIm f u) : ℂ) ^ ((z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ)))
Tactic: simp_rw [sSupNormIm_scale_left f hul, sSupNormIm_scale_right f hul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
inst_1 : NormedSpace ℂ E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
⊢ ‖f z‖ ≤ ‖((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (1 - z) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ z‖
have simp : ‖f z‖ ≤ (ε + sSupNormIm f 0) ^ (1 - z.re) * (ε + sSupNormIm f 1) ^ z.re
Tactic: simp only [norm_mul, ← ofReal_add, norm_cpow_eq_rpow_re_of_pos (sSupNormIm_eps_pos f hε _) _,
    sub_re, one_re]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
inst_1 : NormedSpace ℂ E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
⊢ ‖f z‖ ≤ (ε + sSupNormIm f 0) ^ (1 - z.re) * (ε + sSupNormIm f 1) ^ z.re
have rw : ‖f z‖ * HPow.hPow (β := ℝ) ((ε + sSupNormIm f 0) ^ (1 - z.re)) (-1) *
    HPow.hPow (β := ℝ) ((ε + sSupNormIm f 1) ^ z.re) (-1) ≤
  1
Tactic: rw [← mul_inv_le_iff₀', ← one_mul (((ε + sSupNormIm f 1) ^ z.re)), ← mul_inv_le_iff₀,
    ← Real.rpow_neg_one, ← Real.rpow_neg_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
inst_1 : NormedSpace ℂ E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
rw :
  ‖f z‖ * HPow.hPow (β := ℝ) ((ε + sSupNormIm f 0) ^ (1 - z.re)) (-1) *
      HPow.hPow (β := ℝ) ((ε + sSupNormIm f 1) ^ z.re) (-1) ≤
    1
⊢ ‖f z‖ ≤ (ε + sSupNormIm f 0) ^ (1 - z.re) * (ε + sSupNormIm f 1) ^ z.re
have rw₁ : 0 < (ε + sSupNormIm f 1) ^ z.re
Tactic: rw [← mul_inv_le_iff₀', ← one_mul (((ε + sSupNormIm f 1) ^ z.re)), ← mul_inv_le_iff₀,
    ← Real.rpow_neg_one, ← Real.rpow_neg_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
inst_1 : NormedSpace ℂ E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
rw :
  ‖f z‖ * HPow.hPow (β := ℝ) ((ε + sSupNormIm f 0) ^ (1 - z.re)) (-1) *
      HPow.hPow (β := ℝ) ((ε + sSupNormIm f 1) ^ z.re) (-1) ≤
    1
rw₁ : 0 < (ε + sSupNormIm f 1) ^ z.re
⊢ ‖f z‖ ≤ (ε + sSupNormIm f 0) ^ (1 - z.re) * (ε + sSupNormIm f 1) ^ z.re
have rw₂ : 0 < (ε + sSupNormIm f 0) ^ (1 - z.re)
Tactic: rw [← mul_inv_le_iff₀', ← one_mul (((ε + sSupNormIm f 1) ^ z.re)), ← mul_inv_le_iff₀,
    ← Real.rpow_neg_one, ← Real.rpow_neg_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
inst_1 : NormedSpace ℂ E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
⊢ ‖f z‖ * HPow.hPow (β := ℝ) ((ε + sSupNormIm f 0) ^ (1 - z.re)) (-1) *
      HPow.hPow (β := ℝ) ((ε + sSupNormIm f 1) ^ z.re) (-1) ≤
    1
have simp : ‖f z‖ * ((ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)) ≤ 1
Tactic: simp only [← Real.rpow_mul (le_of_lt (sSupNormIm_eps_pos f hε _)),
    mul_neg, mul_one, neg_sub, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
inst_1 : NormedSpace ℂ E
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hz : z ∈ verticalStrip 0 1
ε : ℝ
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) ε →
    ‖f z‖ ≤ ‖((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (1 - z) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ z‖
have h : ∀ (hε : 0 < ε), ‖f z‖ ≤ ‖((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (1 - z) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ z‖
Tactic: (hε : 0 < ε)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
inst_1 : NormedSpace ℂ E
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hz : z ∈ verticalStrip 0 1
⊢ EventuallyLE (β := ℝ) (𝓝[>] 0) (fun (x : ℝ) ↦ ‖f z‖) fun (ε : ℝ) ↦
    ‖((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (1 - z) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ z‖
have h : ∀ (a : ℝ),
  Membership.mem (γ := Set ℝ)
    {x : ℝ |
      Membership.mem (γ := Set ℝ) (Ioi 0) x →
        Membership.mem (γ := Set ℝ)
          {x : ℝ |
            (fun (x : ℝ) ↦
                LE.le (α := ℝ) ((fun (x : ℝ) ↦ ‖f z‖) x)
                  ((fun (ε : ℝ) ↦
                      ‖((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (1 - z) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ z‖)
                    x))
              x}
          x}
    a
Tactic: filter_upwards [self_mem_nhdsWithin] with ε (hε : 0 < ε) using
    norm_le_interpStrip_of_mem_verticalClosedStrip_eps f ε hε z hB hd
      (mem_of_mem_of_subset hz (preimage_mono Ioo_subset_Icc_self))
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
inst_1 : NormedSpace ℂ E
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hz : z ∈ verticalStrip 0 1
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) (Ioi 0) x →
          Membership.mem (γ := Set ℝ)
            {x : ℝ |
              (fun (x : ℝ) ↦
                  LE.le (α := ℝ) ((fun (x : ℝ) ↦ ‖f z‖) x)
                    ((fun (ε : ℝ) ↦
                        ‖((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (1 - z) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ z‖)
                      x))
                x}
            x}
      a
⊢ EventuallyLE (β := ℝ) (𝓝[>] 0) (fun (x : ℝ) ↦ ‖f z‖) fun (ε : ℝ) ↦
    ‖((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (1 - z) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ z‖
have h₁ : ∀ (a : ℝ),
  Membership.mem (γ := Set ℝ) (Ioi 0) a →
    ‖f z‖ ≤ ‖((↑a : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (1 - z) * ((↑a : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ z‖
Tactic: filter_upwards [self_mem_nhdsWithin] with ε (hε : 0 < ε) using
    norm_le_interpStrip_of_mem_verticalClosedStrip_eps f ε hε z hB hd
      (mem_of_mem_of_subset hz (preimage_mono Ioo_subset_Icc_self))
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
inst_1 : NormedSpace ℂ E
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hz : z ∈ verticalStrip 0 1
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) (Ioi 0) x →
          Membership.mem (γ := Set ℝ)
            {x : ℝ |
              (fun (x : ℝ) ↦
                  LE.le (α := ℝ) ((fun (x : ℝ) ↦ ‖f z‖) x)
                    ((fun (ε : ℝ) ↦
                        ‖((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (1 - z) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ z‖)
                      x))
                x}
            x}
      a
h₁ :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) a →
      ‖f z‖ ≤ ‖((↑a : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (1 - z) * ((↑a : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ z‖
⊢ EventuallyLE (β := ℝ) (𝓝[>] 0) (fun (x : ℝ) ↦ ‖f z‖) fun (ε : ℝ) ↦
    ‖((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (1 - z) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ z‖
have h₂ : ∀ (ε : ℝ) (hε : 0 < ε),
  ‖f z‖ ≤ ‖((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (1 - z) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ z‖
Tactic: filter_upwards [self_mem_nhdsWithin] with ε (hε : 0 < ε) using
    norm_le_interpStrip_of_mem_verticalClosedStrip_eps f ε hε z hB hd
      (mem_of_mem_of_subset hz (preimage_mono Ioo_subset_Icc_self))
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
inst_1 : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
⊢ ‖f z‖ ≤ ‖interpStrip f z‖
have apply : Tendsto (fun (x : ℝ) ↦ ‖f z‖) (𝓝[>] 0) (𝓝 ‖f z‖)
Tactic: apply tendsto_le_of_eventuallyLE _ _ (eventuallyle f z hB hd hz)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
inst_1 : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
apply : Tendsto (fun (x : ℝ) ↦ ‖f z‖) (𝓝[>] 0) (𝓝 ‖f z‖)
⊢ ‖f z‖ ≤ ‖interpStrip f z‖
have apply₁ : Tendsto (fun (ε : ℝ) ↦ ‖((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (1 - z) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ z‖)
  (𝓝[>] 0) (𝓝 ‖interpStrip f z‖)
Tactic: apply tendsto_le_of_eventuallyLE _ _ (eventuallyle f z hB hd hz)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
inst_1 : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
⊢ Tendsto (fun (ε : ℝ) ↦ ‖((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (1 - z) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ z‖)
    (𝓝[>] 0) (𝓝 ‖interpStrip f z‖)
have rw : Tendsto (fun (ε : ℝ) ↦ ‖((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (1 - z) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ z‖)
  (𝓝[>] 0) (𝓝 ‖(↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z‖)
Tactic: rw [interpStrip_eq_of_mem_verticalStrip _ _ hz]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
inst_1 : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
⊢ Tendsto (fun (ε : ℝ) ↦ ‖((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (1 - z) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ z‖)
    (𝓝[>] 0) (𝓝 ‖(↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z‖)
have h : ‖(↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z‖ =
  ‖((↑0 : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (1 - z) * ((↑0 : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ z‖
Tactic: convert! ContinuousWithinAt.tendsto _ using 2
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
inst_1 : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
h :
  ‖(↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z‖ =
    ‖((↑0 : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (1 - z) * ((↑0 : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ z‖
⊢ Tendsto (fun (ε : ℝ) ↦ ‖((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (1 - z) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ z‖)
    (𝓝[>] 0) (𝓝 ‖(↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z‖)
have convert_8 : ContinuousWithinAt (Y := ℝ)
  (fun (ε : ℝ) ↦ ‖((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (1 - z) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ z‖) (Ioi 0) 0
Tactic: convert! ContinuousWithinAt.tendsto _ using 2
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
inst_1 : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
⊢ ContinuousWithinAt (Y := ℝ)
    (fun (ε : ℝ) ↦ ‖((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (1 - z) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ z‖) (Ioi 0)
    0
have convert_8 : ContinuousWithinAt (Y := ℝ) (fun (ε : ℝ) ↦ ‖(↑(ε + sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(ε + sSupNormIm f 1) : ℂ) ^ z‖)
  (Ioi 0) 0
Tactic: simp_rw [← ofReal_add]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
inst_1 : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
    ‖(↑(x + sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(x + sSupNormIm f 1) : ℂ) ^ z‖
have simp : (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
  ‖(↑(x + sSupNormIm f 0) : ℂ) ^ (1 - z)‖ * ‖(↑(x + sSupNormIm f 1) : ℂ) ^ z‖
Tactic: simp only [norm_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
inst_1 : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
    ‖(↑(x + sSupNormIm f 0) : ℂ) ^ (1 - z)‖ * ‖(↑(x + sSupNormIm f 1) : ℂ) ^ z‖
have rw : (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
  (x + sSupNormIm f 0) ^ (1 - z).re * ‖(↑(x + sSupNormIm f 1) : ℂ) ^ z‖
Tactic: rw [norm_cpow_eq_rpow_re_of_nonneg (le_of_lt (sSupNormIm_eps_pos f hx _)) _]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
inst_1 : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
rw :
  (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
    (x + sSupNormIm f 0) ^ (1 - z).re * ‖(↑(x + sSupNormIm f 1) : ℂ) ^ z‖
⊢ (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
    ‖(↑(x + sSupNormIm f 0) : ℂ) ^ (1 - z)‖ * ‖(↑(x + sSupNormIm f 1) : ℂ) ^ z‖
have rw₁ : (1 - z).re ≠ 0
Tactic: rw [norm_cpow_eq_rpow_re_of_nonneg (le_of_lt (sSupNormIm_eps_pos f hx _)) _]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
inst_1 : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
    (x + sSupNormIm f 0) ^ (1 - z).re * ‖(↑(x + sSupNormIm f 1) : ℂ) ^ z‖
have rw : (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
  (x + sSupNormIm f 0) ^ (1 - z).re * (x + sSupNormIm f 1) ^ z.re
Tactic: rw [norm_cpow_eq_rpow_re_of_nonneg (le_of_lt (sSupNormIm_eps_pos f hx _)) _]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
inst_1 : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
rw :
  (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
    (x + sSupNormIm f 0) ^ (1 - z).re * (x + sSupNormIm f 1) ^ z.re
⊢ (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
    (x + sSupNormIm f 0) ^ (1 - z).re * ‖(↑(x + sSupNormIm f 1) : ℂ) ^ z‖
have rw₁ : z.re ≠ 0
Tactic: rw [norm_cpow_eq_rpow_re_of_nonneg (le_of_lt (sSupNormIm_eps_pos f hx _)) _]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
inst_1 : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
    ‖(↑(x + sSupNormIm f 0) : ℂ) ^ (1 - z)‖ * ‖(↑(x + sSupNormIm f 1) : ℂ) ^ z‖
have repeat : (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
  (x + sSupNormIm f 0) ^ (1 - z).re * (x + sSupNormIm f 1) ^ z.re
Tactic: repeat rw [norm_cpow_eq_rpow_re_of_nonneg (le_of_lt (sSupNormIm_eps_pos f hx _)) _]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
inst_1 : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
repeat :
  (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
    (x + sSupNormIm f 0) ^ (1 - z).re * (x + sSupNormIm f 1) ^ z.re
⊢ (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
    ‖(↑(x + sSupNormIm f 0) : ℂ) ^ (1 - z)‖ * ‖(↑(x + sSupNormIm f 1) : ℂ) ^ z‖
have repeat₁ : z.re ≠ 0
Tactic: repeat rw [norm_cpow_eq_rpow_re_of_nonneg (le_of_lt (sSupNormIm_eps_pos f hx _)) _]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
inst_1 : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
repeat :
  (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
    (x + sSupNormIm f 0) ^ (1 - z).re * (x + sSupNormIm f 1) ^ z.re
repeat₁ : z.re ≠ 0
⊢ (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
    ‖(↑(x + sSupNormIm f 0) : ℂ) ^ (1 - z)‖ * ‖(↑(x + sSupNormIm f 1) : ℂ) ^ z‖
have repeat₂ : (1 - z).re ≠ 0
Tactic: repeat rw [norm_cpow_eq_rpow_re_of_nonneg (le_of_lt (sSupNormIm_eps_pos f hx _)) _]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
inst_1 : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
⊢ ContinuousWithinAt (Y := ℝ) (fun (ε : ℝ) ↦ ‖(↑(ε + sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(ε + sSupNormIm f 1) : ℂ) ^ z‖)
    (Ioi 0) 0
have this : ∀ (x : ℝ),
  Membership.mem (γ := Set ℝ) (Ioi 0) x →
    (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
      ‖(↑(x + sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(x + sSupNormIm f 1) : ℂ) ^ z‖
Tactic: have : ∀ x ∈ Ioi 0, (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re
          = ‖((x + sSupNormIm f 0 : ℝ) ^ (1 - z) * (x + sSupNormIm f 1 : ℝ) ^ z : ℂ)‖ := by
              intro x hx
              simp only [norm_mul]
              repeat rw [norm_cpow_eq_rpow_re_of_nonneg (le_of_lt (sSupNormIm_eps_pos f hx _)) _]
              · simp only [sub_re, one_re]
              · simpa using (ne_comm.mpr (ne_of_lt hz.1))
              · simpa [sub_eq_zero] using (ne_comm.mpr (ne_of_lt hz.2))