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
inst_1 : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
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‖
⊢ ContinuousWithinAt (Y := ℝ) (fun (ε : ℝ) ↦ ‖(↑(ε + sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(ε + sSupNormIm f 1) : ℂ) ^ z‖)
    (Ioi 0) 0
have apply : Tendsto (β := ℝ) (fun (x : ℝ) ↦ (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re) (𝓝[>] 0)
  (𝓝 ((fun (ε : ℝ) ↦ ‖(↑(ε + sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(ε + sSupNormIm f 1) : ℂ) ^ z‖) 0))
Tactic: apply tendsto_nhdsWithin_congr this _
-- 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
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‖
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re) (𝓝[>] 0)
    (𝓝 ((fun (ε : ℝ) ↦ ‖(↑(ε + sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(ε + sSupNormIm f 1) : ℂ) ^ z‖) 0))
have simp : Tendsto (fun (x : ℝ) ↦ (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re) (𝓝[>] 0)
  (𝓝 ‖(↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z‖)
Tactic: simp only [zero_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
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‖
⊢ Tendsto (fun (x : ℝ) ↦ (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re) (𝓝[>] 0)
    (𝓝 ‖(↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z‖)
have rw : Tendsto (fun (x : ℝ) ↦ (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re) (𝓝[>] 0)
  (𝓝 (sSupNormIm f 0 ^ (1 - z).re * sSupNormIm f 1 ^ z.re))
Tactic: rw [norm_mul, norm_cpow_eq_rpow_re_of_nonneg (sSupNormIm_nonneg _ _) _,
        norm_cpow_eq_rpow_re_of_nonneg (sSupNormIm_nonneg _ _) _]
-- 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
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‖
rw :
  Tendsto (fun (x : ℝ) ↦ (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re) (𝓝[>] 0)
    (𝓝 (sSupNormIm f 0 ^ (1 - z).re * sSupNormIm f 1 ^ z.re))
⊢ Tendsto (fun (x : ℝ) ↦ (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re) (𝓝[>] 0)
    (𝓝 ‖(↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z‖)
have rw₁ : z.re ≠ 0
Tactic: rw [norm_mul, norm_cpow_eq_rpow_re_of_nonneg (sSupNormIm_nonneg _ _) _,
        norm_cpow_eq_rpow_re_of_nonneg (sSupNormIm_nonneg _ _) _]
-- 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
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‖
rw :
  Tendsto (fun (x : ℝ) ↦ (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re) (𝓝[>] 0)
    (𝓝 (sSupNormIm f 0 ^ (1 - z).re * sSupNormIm f 1 ^ z.re))
rw₁ : z.re ≠ 0
⊢ Tendsto (fun (x : ℝ) ↦ (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re) (𝓝[>] 0)
    (𝓝 ‖(↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z‖)
have rw₂ : (1 - z).re ≠ 0
Tactic: rw [norm_mul, norm_cpow_eq_rpow_re_of_nonneg (sSupNormIm_nonneg _ _) _,
        norm_cpow_eq_rpow_re_of_nonneg (sSupNormIm_nonneg _ _) _]
-- 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
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‖
⊢ Tendsto (fun (x : ℝ) ↦ (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re) (𝓝[>] 0)
    (𝓝 (sSupNormIm f 0 ^ (1 - z).re * sSupNormIm f 1 ^ z.re))
have hf : Tendsto (fun (x : ℝ) ↦ (x + sSupNormIm f 0) ^ (1 - z.re)) (𝓝[>] 0) (𝓝 (sSupNormIm f 0 ^ (1 - z).re))
Tactic: apply Tendsto.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
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‖
hf : Tendsto (fun (x : ℝ) ↦ (x + sSupNormIm f 0) ^ (1 - z.re)) (𝓝[>] 0) (𝓝 (sSupNormIm f 0 ^ (1 - z).re))
⊢ Tendsto (fun (x : ℝ) ↦ (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re) (𝓝[>] 0)
    (𝓝 (sSupNormIm f 0 ^ (1 - z).re * sSupNormIm f 1 ^ z.re))
have hg : Tendsto (fun (x : ℝ) ↦ (x + sSupNormIm f 1) ^ z.re) (𝓝[>] 0) (𝓝 (sSupNormIm f 1 ^ z.re))
Tactic: apply Tendsto.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
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‖
⊢ Tendsto (fun (x : ℝ) ↦ (x + sSupNormIm f 0) ^ (1 - z.re)) (𝓝[>] 0) (𝓝 (sSupNormIm f 0 ^ (1 - z).re))
have hf : Tendsto (fun (a : ℝ) ↦ a + sSupNormIm f 0) (𝓝[>] 0) (𝓝 (sSupNormIm f 0))
Tactic: apply Tendsto.rpow_const
-- 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
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‖
hf : Tendsto (fun (a : ℝ) ↦ a + sSupNormIm f 0) (𝓝[>] 0) (𝓝 (sSupNormIm f 0))
⊢ Tendsto (fun (x : ℝ) ↦ (x + sSupNormIm f 0) ^ (1 - z.re)) (𝓝[>] 0) (𝓝 (sSupNormIm f 0 ^ (1 - z).re))
have hf₁ : sSupNormIm f 0 ≠ 0 ∨ 0 ≤ 1 - z.re
Tactic: apply Tendsto.rpow_const
-- 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
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‖
⊢ Tendsto (fun (a : ℝ) ↦ a + sSupNormIm f 0) (𝓝[>] 0) (𝓝 (sSupNormIm f 0))
have hf : Tendsto (fun (a : ℝ) ↦ a + sSupNormIm f 0) (𝓝[>] 0) (𝓝 (0 + sSupNormIm f 0))
Tactic: nth_rw 2 [← zero_add (sSupNormIm f 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 : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
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‖
⊢ sSupNormIm f 0 ≠ 0 ∨ 0 ≤ 1 - z.re
have hf : 0 ≤ 1 - z.re
Tactic: right
-- 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
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‖
⊢ Tendsto (fun (x : ℝ) ↦ (x + sSupNormIm f 1) ^ z.re) (𝓝[>] 0) (𝓝 (sSupNormIm f 1 ^ z.re))
have hg : Tendsto (fun (a : ℝ) ↦ a + sSupNormIm f 1) (𝓝[>] 0) (𝓝 (sSupNormIm f 1))
Tactic: apply Tendsto.rpow_const
-- 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
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‖
hg : Tendsto (fun (a : ℝ) ↦ a + sSupNormIm f 1) (𝓝[>] 0) (𝓝 (sSupNormIm f 1))
⊢ Tendsto (fun (x : ℝ) ↦ (x + sSupNormIm f 1) ^ z.re) (𝓝[>] 0) (𝓝 (sSupNormIm f 1 ^ z.re))
have hg₁ : sSupNormIm f 1 ≠ 0 ∨ 0 ≤ z.re
Tactic: apply Tendsto.rpow_const
-- 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
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‖
⊢ Tendsto (fun (a : ℝ) ↦ a + sSupNormIm f 1) (𝓝[>] 0) (𝓝 (sSupNormIm f 1))
have hg : Tendsto (fun (a : ℝ) ↦ a + sSupNormIm f 1) (𝓝[>] 0) (𝓝 (0 + sSupNormIm f 1))
Tactic: nth_rw 2 [← zero_add (sSupNormIm f 1)]
-- 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
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‖
⊢ sSupNormIm f 1 ≠ 0 ∨ 0 ≤ z.re
have hg : 0 ≤ z.re
Tactic: 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
z : ℂ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
⊢ ‖f z‖ ≤ ‖interpStrip f z‖
have hx : z ∈ closure (verticalStrip 0 1)
Tactic: apply le_on_closure (fun w hw ↦ norm_le_interpStrip_of_mem_verticalStrip_zero f w hd hB hw)
    (Continuous.comp_continuousOn' continuous_norm hd.2)
    (Continuous.comp_continuousOn' continuous_norm (diffContOnCl_interpStrip f).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
z : ℂ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
⊢ z ∈ closure (verticalStrip 0 1)
have hx : ∀ (hz : z ∈ re ⁻¹' Icc 0 1) (hd : DiffContOnCl ℂ f (verticalStrip 0 1))
  (hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)), z ∈ closure (verticalStrip 0 1)
Tactic: rwa [verticalClosedStrip, ← closure_Ioo zero_ne_one, ← closure_preimage_re] at hz
Cleared hypotheses: hz, hd, 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
z : ℂ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hx :
  ∀ (hz : z ∈ re ⁻¹' Icc 0 1) (hd : DiffContOnCl ℂ f (verticalStrip 0 1))
    (hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)), z ∈ closure (verticalStrip 0 1)
⊢ z ∈ closure (verticalStrip 0 1)
have hx₁ : ∀ (hz : z ∈ re ⁻¹' closure (Ioo 0 1)) (hd : DiffContOnCl ℂ f (verticalStrip 0 1))
  (hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)), z ∈ closure (verticalStrip 0 1)
Tactic: rwa [verticalClosedStrip, ← closure_Ioo zero_ne_one, ← closure_preimage_re] at hz
Cleared hypotheses: hz, hd, 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
z : ℂ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hx :
  ∀ (hz : z ∈ re ⁻¹' Icc 0 1) (hd : DiffContOnCl ℂ f (verticalStrip 0 1))
    (hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)), z ∈ closure (verticalStrip 0 1)
hx₁ :
  ∀ (hz : z ∈ re ⁻¹' closure (Ioo 0 1)) (hd : DiffContOnCl ℂ f (verticalStrip 0 1))
    (hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)), z ∈ closure (verticalStrip 0 1)
⊢ z ∈ closure (verticalStrip 0 1)
have hx₂ : ∀ (hz : z ∈ closure (re ⁻¹' Ioo 0 1)) (hd : DiffContOnCl ℂ f (verticalStrip 0 1))
  (hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)), z ∈ closure (verticalStrip 0 1)
Tactic: rwa [verticalClosedStrip, ← closure_Ioo zero_ne_one, ← closure_preimage_re] at hz
Cleared hypotheses: hz, hd, 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
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
⊢ ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
have pos : ∀ (h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0), ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
Tactic: by_cases! h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 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
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
pos :
  ∀ (h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0),
    ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
⊢ ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
have neg : ∀ (h : sSupNormIm f 0 ≠ 0 ∧ sSupNormIm f 1 ≠ 0), ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
Tactic: by_cases! h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 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
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0
⊢ ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
have pos : 0 ≤ sSupNormIm f 0 ^ (1 - z.re) ∧ 0 ≤ sSupNormIm f 1 ^ z.re ∨
  sSupNormIm f 0 ^ (1 - z.re) ≤ 0 ∧ sSupNormIm f 1 ^ z.re ≤ 0
Tactic: rw [interpStrip_eq_of_zero f z h, norm_zero, mul_nonneg_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
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0
⊢ 0 ≤ sSupNormIm f 0 ^ (1 - z.re) ∧ 0 ≤ sSupNormIm f 1 ^ z.re ∨
    sSupNormIm f 0 ^ (1 - z.re) ≤ 0 ∧ sSupNormIm f 1 ^ z.re ≤ 0
have pos : 0 ≤ sSupNormIm f 0 ^ (1 - z.re) ∧ 0 ≤ sSupNormIm f 1 ^ z.re
Tactic: 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
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
h : sSupNormIm f 0 ≠ 0 ∧ sSupNormIm f 1 ≠ 0
⊢ ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
have h0 : sSupNormIm f 0 ≠ 0
Tactic: rcases h with ⟨h0, h1⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
h : sSupNormIm f 0 ≠ 0 ∧ sSupNormIm f 1 ≠ 0
h0 : sSupNormIm f 0 ≠ 0
⊢ ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
have h1 : sSupNormIm f 1 ≠ 0
Tactic: rcases h with ⟨h0, h1⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
h0 : sSupNormIm f 0 ≠ 0
h1 : sSupNormIm f 1 ≠ 0
⊢ ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
have h0₁ : 0 ≠ sSupNormIm f 0
Tactic: rw [ne_comm] at h0 h1
Cleared hypotheses: h0, h1
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
h0 : sSupNormIm f 0 ≠ 0
h1 : sSupNormIm f 1 ≠ 0
h0₁ : 0 ≠ sSupNormIm f 0
⊢ ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
have h1₁ : 0 ≠ sSupNormIm f 1
Tactic: rw [ne_comm] at h0 h1
Cleared hypotheses: h0, h1
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
⊢ ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
have neg : ‖(↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
Tactic: simp_rw [interpStrip_eq_of_pos f _ (lt_of_le_of_ne (sSupNormIm_nonneg f 0) h0)
        (lt_of_le_of_ne (sSupNormIm_nonneg f 1) h1)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
⊢ ‖(↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z‖ ≤
    sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
have neg : ‖(↑(sSupNormIm f 0) : ℂ) ^ (1 - z)‖ * ‖(↑(sSupNormIm f 1) : ℂ) ^ z‖ ≤
  sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
Tactic: simp only [norm_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
⊢ ‖(↑(sSupNormIm f 0) : ℂ) ^ (1 - z)‖ * ‖(↑(sSupNormIm f 1) : ℂ) ^ z‖ ≤
    sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
have neg : sSupNormIm f 0 ^ (1 - z).re * ‖(↑(sSupNormIm f 1) : ℂ) ^ z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
Tactic: rw [norm_cpow_eq_rpow_re_of_pos ((Ne.le_iff_lt h0).mp (sSupNormIm_nonneg f _)) _]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
⊢ sSupNormIm f 0 ^ (1 - z).re * ‖(↑(sSupNormIm f 1) : ℂ) ^ z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
have neg : sSupNormIm f 0 ^ (1 - z).re * sSupNormIm f 1 ^ z.re ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
Tactic: rw [norm_cpow_eq_rpow_re_of_pos ((Ne.le_iff_lt h1).mp (sSupNormIm_nonneg f _)) _]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
⊢ ‖f z‖ ≤ a ^ (1 - z.re) * b ^ z.re
have this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
Tactic: have : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re := by
    by_cases! h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0
    · rw [interpStrip_eq_of_zero f z h, norm_zero, mul_nonneg_iff]
      left
      exact ⟨Real.rpow_nonneg (sSupNormIm_nonneg f _) _,
        Real.rpow_nonneg (sSupNormIm_nonneg f _) _ ⟩
    · rcases h with ⟨h0, h1⟩
      rw [ne_comm] at h0 h1
      simp_rw [interpStrip_eq_of_pos f _ (lt_of_le_of_ne (sSupNormIm_nonneg f 0) h0)
        (lt_of_le_of_ne (sSupNormIm_nonneg f 1) h1)]
      simp only [norm_mul]
      rw [norm_cpow_eq_rpow_re_of_pos ((Ne.le_iff_lt h0).mp (sSupNormIm_nonneg f _)) _]
      rw [norm_cpow_eq_rpow_re_of_pos ((Ne.le_iff_lt h1).mp (sSupNormIm_nonneg f _)) _]
      simp only [sub_re, one_re, le_refl]