awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z_1 : ℂ
hre : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hz_1 : 0 ≤ z_1.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun (z : ℂ) ↦ cexp ((↑ε : ℂ) * z) • f z
hd : DiffContOnCl ℂ g {z : ℂ | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.re} z
⊢ expR (ε * z.re) * ‖f z‖ ≤ ‖f z‖
have h : ε * z.re ≤ 0
Tactic: refine mul_le_of_le_one_left (norm_nonneg _) (Real.exp_le_one_iff.2 ?_)
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun (z : ℂ) ↦ cexp ((↑ε : ℂ) * z) • f z
hd : DiffContOnCl ℂ g {z : ℂ | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
⊢ Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ g (↑x : ℂ)) atTop (𝓝 0)
have h : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ expR (ε * x) • f (↑x : ℂ)) atTop (𝓝 0)
Tactic: simp_rw [g, ← ofReal_mul, ← ofReal_exp, coe_smul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun (z : ℂ) ↦ cexp ((↑ε : ℂ) * z) • f z
hd : DiffContOnCl ℂ g {z : ℂ | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
⊢ Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ expR (ε * x) • f (↑x : ℂ)) atTop (𝓝 0)
have h₀ : Tendsto (β := ℝ) (fun (x : ℝ) ↦ expR (ε * x)) atTop (𝓝 0)
Tactic: have h₀ : Tendsto (fun x : ℝ => expR (ε * x)) atTop (𝓝 0) :=
      Real.tendsto_exp_atBot.comp (tendsto_const_nhds.neg_mul_atTop ε₀ tendsto_id)
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun (z : ℂ) ↦ cexp ((↑ε : ℂ) * z) • f z
hd : DiffContOnCl ℂ g {z : ℂ | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
y : ℝ
⊢ ‖g ((↑y : ℂ) * I)‖ ≤ C
have h : ‖f ((↑y : ℂ) * I)‖ ≤ C
Tactic: rw [hgn, re_ofReal_mul, I_re, mul_zero, mul_zero, Real.exp_zero,
      one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z : ℂ | 0 < z.re}
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
him : ∃ (C : ℝ), ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
⊢ EqOn f 0 {z : ℂ | 0 ≤ z.re}
have rcases : ∀ (C : ℝ) (hC : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C), EqOn f 0 {z : ℂ | 0 ≤ z.re}
Tactic: rcases him with ⟨C, hC⟩
Cleared hypotheses: him
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z : ℂ | 0 < z.re}
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
C : ℝ
hC : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
⊢ EqOn f 0 {z : ℂ | 0 ≤ z.re}
have suffices : ∀ (z : ℂ), 0 < z.re → f z = 0
Tactic: suffices ∀ z : ℂ, 0 < z.re → f z = 0 by
    simpa only [closure_setOf_lt_re] using
      EqOn.of_subset_closure this hd.continuousOn continuousOn_const subset_closure Subset.rfl
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z : ℂ | 0 < z.re}
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
C : ℝ
hC : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
g : ℕ → ℂ → E := fun (n : ℕ) (z : ℂ) ↦ cexp z ^ n • f z
⊢ ∀ (z : ℂ), 0 < z.re → f z = 0
have hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
Tactic: have hg : ∀ n z, ‖g n z‖ = expR z.re ^ n * ‖f z‖ := fun n z ↦ by
    simp only [g, norm_smul, norm_pow, norm_exp]
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z : ℂ | 0 < z.re}
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
C : ℝ
hC : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
g : ℕ → ℂ → E := fun (n : ℕ) (z : ℂ) ↦ cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
z : ℂ
hz : 0 < z.re
H : ∀ (n : ℕ), ‖g n z‖ ≤ C
⊢ f z = 0
have contrapose! : ∀ (H : f z ≠ 0), ∃ (n : ℕ), C < ‖g n z‖
Tactic: contrapose! H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z : ℂ | 0 < z.re}
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
C : ℝ
hC : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
g : ℕ → ℂ → E := fun (n : ℕ) (z : ℂ) ↦ cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
z : ℂ
hz : 0 < z.re
H : f z ≠ 0
⊢ ∃ (n : ℕ), C < ‖g n z‖
have simp : ∃ (n : ℕ), C < expR z.re ^ n * ‖f z‖
Tactic: simp only [hg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z : ℂ | 0 < z.re}
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
C : ℝ
hC : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
g : ℕ → ℂ → E := fun (n : ℕ) (z : ℂ) ↦ cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
z : ℂ
hz : 0 < z.re
⊢ f z = 0
have suffices : ∀ (n : ℕ), ‖g n z‖ ≤ C
Tactic: suffices H : ∀ n : ℕ, ‖g n z‖ ≤ C by
    contrapose! H
    simp only [hg]
    exact (((tendsto_pow_atTop_atTop_of_one_lt (Real.one_lt_exp_iff.2 hz)).atTop_mul_const
      (norm_pos_iff.2 H)).eventually (eventually_gt_atTop C)).exists
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z : ℂ | 0 < z.re}
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
C : ℝ
hC : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
g : ℕ → ℂ → E := fun (n : ℕ) (z : ℂ) ↦ cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
z : ℂ
hz : 0 < z.re
n : ℕ
⊢ ‖g n z‖ ≤ C
have refine_1 : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) (g n) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
Tactic: refine right_half_plane_of_tendsto_zero_on_real ((differentiable_exp.pow n).diffContOnCl.smul hd)
    ?_ ?_ (fun y => ?_) hz.le
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z : ℂ | 0 < z.re}
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
C : ℝ
hC : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
g : ℕ → ℂ → E := fun (n : ℕ) (z : ℂ) ↦ cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
z : ℂ
hz : 0 < z.re
n : ℕ
refine_1 :
  ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) (g n) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
⊢ ‖g n z‖ ≤ C
have refine_2 : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ g n (↑x : ℂ)) atTop (𝓝 0)
Tactic: refine right_half_plane_of_tendsto_zero_on_real ((differentiable_exp.pow n).diffContOnCl.smul hd)
    ?_ ?_ (fun y => ?_) hz.le
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z : ℂ | 0 < z.re}
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
C : ℝ
hC : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
g : ℕ → ℂ → E := fun (n : ℕ) (z : ℂ) ↦ cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
z : ℂ
hz : 0 < z.re
n : ℕ
refine_1 :
  ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) (g n) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
refine_2 : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ g n (↑x : ℂ)) atTop (𝓝 0)
⊢ ‖g n z‖ ≤ C
have refine_3 : ∀ (y : ℝ), ‖g n ((↑y : ℂ) * I)‖ ≤ C
Tactic: refine right_half_plane_of_tendsto_zero_on_real ((differentiable_exp.pow n).diffContOnCl.smul hd)
    ?_ ?_ (fun y => ?_) hz.le
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z : ℂ | 0 < z.re}
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
C : ℝ
hC : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
g : ℕ → ℂ → E := fun (n : ℕ) (z : ℂ) ↦ cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
z : ℂ
hz : 0 < z.re
n : ℕ
⊢ ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) (g n) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
have refine_1 : ∀ (c : ℝ) (hc : c < 2) (B : ℝ)
  (hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)),
  ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) (g n) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
Tactic: rcases hexp with ⟨c, hc, B, hO⟩
Cleared hypotheses: hexp
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z : ℂ | 0 < z.re}
hre : SuperpolynomialDecay atTop expR fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
C : ℝ
hC : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
g : ℕ → ℂ → E := fun (n : ℕ) (z : ℂ) ↦ cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
z : ℂ
hz : 0 < z.re
n : ℕ
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
⊢ ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) (g n) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
have refine_1 : IsBigO (E := ℝ) (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) (fun (x : ℂ) ↦ ‖g n x‖) fun (z : ℂ) ↦
  expR (((↑n : ℝ) + max B 0) * ‖z‖ ^ max c 1)
Tactic: refine ⟨max c 1, max_lt hc one_lt_two, n + max B 0, .of_norm_left ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z : ℂ | 0 < z.re}
hre : SuperpolynomialDecay atTop expR fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
C : ℝ
hC : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
g : ℕ → ℂ → E := fun (n : ℕ) (z : ℂ) ↦ cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
z : ℂ
hz : 0 < z.re
n : ℕ
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
⊢ IsBigO (E := ℝ) (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) (fun (x : ℂ) ↦ ‖g n x‖) fun (z : ℂ) ↦
    expR (((↑n : ℝ) + max B 0) * ‖z‖ ^ max c 1)
have refine_1 : IsBigO (E := ℝ) (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) (fun (x : ℂ) ↦ expR x.re ^ n * ‖f x‖) fun (z : ℂ) ↦
  expR (((↑n : ℝ) + max B 0) * ‖z‖ ^ max c 1)
Tactic: simp only [hg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z : ℂ | 0 < z.re}
hre : SuperpolynomialDecay atTop expR fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
C : ℝ
hC : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
g : ℕ → ℂ → E := fun (n : ℕ) (z : ℂ) ↦ cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
z : ℂ
hz : 0 < z.re
n : ℕ
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
⊢ IsBigO (E := ℝ) (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) (fun (x : ℂ) ↦ expR x.re ^ n * ‖f x‖) fun (z : ℂ) ↦
    expR (((↑n : ℝ) + max B 0) * ‖z‖ ^ max c 1)
have refine_1 : ∀ᶠ (x : ℂ) in cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re},
  ‖expR x.re ^ n * expR (B * ‖x‖ ^ c)‖ ≤ ‖expR (((↑n : ℝ) + max B 0) * ‖x‖ ^ max c 1)‖
Tactic: refine ((isBigO_refl (fun z : ℂ => expR z.re ^ n) _).mul hO.norm_left).trans (.of_bound' ?_)
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z : ℂ | 0 < z.re}
hre : SuperpolynomialDecay atTop expR fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
C : ℝ
hC : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
g : ℕ → ℂ → E := fun (n : ℕ) (z : ℂ) ↦ cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
z : ℂ
hz : 0 < z.re
n : ℕ
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
⊢ ∀ᶠ (x : ℂ) in cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re},
    ‖expR x.re ^ n * expR (B * ‖x‖ ^ c)‖ ≤ ‖expR (((↑n : ℝ) + max B 0) * ‖x‖ ^ max c 1)‖
have h : ∀ (z : ℂ) (hz : 1 ≤ ‖z‖), ‖expR z.re ^ n * expR (B * ‖z‖ ^ c)‖ ≤ ‖expR (((↑n : ℝ) + max B 0) * ‖z‖ ^ max c 1)‖
Tactic: filter_upwards [(eventually_cobounded_le_norm 1).filter_mono inf_le_left] with z hz
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z : ℂ | 0 < z.re}
hre : SuperpolynomialDecay atTop expR fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
C : ℝ
hC : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
g : ℕ → ℂ → E := fun (n : ℕ) (z : ℂ) ↦ cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
z_1 : ℂ
hz_1 : 0 < z_1.re
n : ℕ
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
z : ℂ
hz : 1 ≤ ‖z‖
⊢ ‖expR z.re ^ n * expR (B * ‖z‖ ^ c)‖ ≤ ‖expR (((↑n : ℝ) + max B 0) * ‖z‖ ^ max c 1)‖
have h : expR ((↑n : ℝ) * z.re + B * ‖z‖ ^ c) ≤ expR ((↑n : ℝ) * ‖z‖ ^ max c 1 + max B 0 * ‖z‖ ^ max c 1)
Tactic: simp only [← Real.exp_nat_mul, ← Real.exp_add, Real.norm_eq_abs, Real.abs_exp, add_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z : ℂ | 0 < z.re}
hre : SuperpolynomialDecay atTop expR fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
C : ℝ
hC : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
g : ℕ → ℂ → E := fun (n : ℕ) (z : ℂ) ↦ cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
z_1 : ℂ
hz_1 : 0 < z_1.re
n : ℕ
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
z : ℂ
hz : 1 ≤ ‖z‖
⊢ expR ((↑n : ℝ) * z.re + B * ‖z‖ ^ c) ≤ expR ((↑n : ℝ) * ‖z‖ ^ max c 1 + max B 0 * ‖z‖ ^ max c 1)
have h : z.re ≤ ‖z‖ ^ max c 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z : ℂ | 0 < z.re}
hre : SuperpolynomialDecay atTop expR fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
C : ℝ
hC : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
g : ℕ → ℂ → E := fun (n : ℕ) (z : ℂ) ↦ cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
z_1 : ℂ
hz_1 : 0 < z_1.re
n : ℕ
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
z : ℂ
hz : 1 ≤ ‖z‖
h : z.re ≤ ‖z‖ ^ max c 1
⊢ expR ((↑n : ℝ) * z.re + B * ‖z‖ ^ c) ≤ expR ((↑n : ℝ) * ‖z‖ ^ max c 1 + max B 0 * ‖z‖ ^ max c 1)
have h₁ : B ≤ max B 0
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z : ℂ | 0 < z.re}
hre : SuperpolynomialDecay atTop expR fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
C : ℝ
hC : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
g : ℕ → ℂ → E := fun (n : ℕ) (z : ℂ) ↦ cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
z_1 : ℂ
hz_1 : 0 < z_1.re
n : ℕ
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
z : ℂ
hz : 1 ≤ ‖z‖
h : z.re ≤ ‖z‖ ^ max c 1
h₁ : B ≤ max B 0
⊢ expR ((↑n : ℝ) * z.re + B * ‖z‖ ^ c) ≤ expR ((↑n : ℝ) * ‖z‖ ^ max c 1 + max B 0 * ‖z‖ ^ max c 1)
have h₂ : c ≤ max c 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z : ℂ | 0 < z.re}
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
C : ℝ
hC : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
g : ℕ → ℂ → E := fun (n : ℕ) (z : ℂ) ↦ cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
z : ℂ
hz : 0 < z.re
n : ℕ
⊢ Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ g n (↑x : ℂ)) atTop (𝓝 0)
have refine_2 : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖g n (↑x : ℂ)‖) atTop (𝓝 0)
Tactic: rw [tendsto_zero_iff_norm_tendsto_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z : ℂ | 0 < z.re}
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
C : ℝ
hC : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
g : ℕ → ℂ → E := fun (n : ℕ) (z : ℂ) ↦ cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
z : ℂ
hz : 0 < z.re
n : ℕ
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖g n (↑x : ℂ)‖) atTop (𝓝 0)
have refine_2 : Tendsto (β := ℝ) (fun (x : ℝ) ↦ expR (↑x : ℂ).re ^ n * ‖f (↑x : ℂ)‖) atTop (𝓝 0)
Tactic: simp only [hg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z : ℂ | 0 < z.re}
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
C : ℝ
hC : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
g : ℕ → ℂ → E := fun (n : ℕ) (z : ℂ) ↦ cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
z : ℂ
hz : 0 < z.re
n : ℕ
y : ℝ
⊢ ‖g n ((↑y : ℂ) * I)‖ ≤ C
have refine_3 : ‖f ((↑y : ℂ) * I)‖ ≤ C
Tactic: rw [hg, re_ofReal_mul, I_re, mul_zero, Real.exp_zero, one_pow, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : ℂ → E
hfd : DiffContOnCl ℂ f {z : ℂ | 0 < z.re}
hgd : DiffContOnCl ℂ g {z : ℂ | 0 < z.re}
hfexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hgexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) g fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun (x : ℝ) ↦ ‖f (↑x : ℂ) - g (↑x : ℂ)‖
hfim : ∃ (C : ℝ), ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hgim : ∃ (C : ℝ), ∀ (x : ℝ), ‖g ((↑x : ℂ) * I)‖ ≤ C
⊢ EqOn f g {z : ℂ | 0 ≤ z.re}
have suffices : EqOn (f - g) 0 {z : ℂ | 0 ≤ z.re}
Tactic: suffices EqOn (f - g) 0 {z : ℂ | 0 ≤ z.re} by
    simpa only [EqOn, Pi.sub_apply, Pi.zero_apply, sub_eq_zero] using this
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : ℂ → E
hfd : DiffContOnCl ℂ f {z : ℂ | 0 < z.re}
hgd : DiffContOnCl ℂ g {z : ℂ | 0 < z.re}
hfexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hgexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) g fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun (x : ℝ) ↦ ‖f (↑x : ℂ) - g (↑x : ℂ)‖
hfim : ∃ (C : ℝ), ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hgim : ∃ (C : ℝ), ∀ (x : ℝ), ‖g ((↑x : ℂ) * I)‖ ≤ C
⊢ EqOn (f - g) 0 {z : ℂ | 0 ≤ z.re}
have refine_1 : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) (f - g) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
Tactic: refine eq_zero_on_right_half_plane_of_superexponential_decay (hfd.sub hgd) ?_ hre ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : ℂ → E
hfd : DiffContOnCl ℂ f {z : ℂ | 0 < z.re}
hgd : DiffContOnCl ℂ g {z : ℂ | 0 < z.re}
hfexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hgexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) g fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun (x : ℝ) ↦ ‖f (↑x : ℂ) - g (↑x : ℂ)‖
hfim : ∃ (C : ℝ), ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hgim : ∃ (C : ℝ), ∀ (x : ℝ), ‖g ((↑x : ℂ) * I)‖ ≤ C
refine_1 :
  ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) (f - g) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
⊢ EqOn (f - g) 0 {z : ℂ | 0 ≤ z.re}
have refine_2 : ∃ (C : ℝ), ∀ (x : ℝ), ‖(f - g) ((↑x : ℂ) * I)‖ ≤ C
Tactic: refine eq_zero_on_right_half_plane_of_superexponential_decay (hfd.sub hgd) ?_ hre ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : ℂ → E
hfd : DiffContOnCl ℂ f {z : ℂ | 0 < z.re}
hgd : DiffContOnCl ℂ g {z : ℂ | 0 < z.re}
hfexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hgexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) g fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun (x : ℝ) ↦ ‖f (↑x : ℂ) - g (↑x : ℂ)‖
hfim : ∃ (C : ℝ), ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hgim : ∃ (C : ℝ), ∀ (x : ℝ), ‖g ((↑x : ℂ) * I)‖ ≤ C
⊢ ∃ (C : ℝ), ∀ (x : ℝ), ‖(f - g) ((↑x : ℂ) * I)‖ ≤ C
have refine_2 : ∀ (Cf : ℝ) (hCf : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ Cf), ∃ (C : ℝ), ∀ (x : ℝ), ‖(f - g) ((↑x : ℂ) * I)‖ ≤ C
Tactic: rcases hfim with ⟨Cf, hCf⟩
Cleared hypotheses: hfim