awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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

Tactic:
right_half_plane_of_tendsto_zero_on_real ((differentiable_exp.pow n).diffContOnCl.smul hd)
    ?_ ?_ (fun y => ?_) hz.le

Premises used: DiffContOnCl.smul, Differentiable.diffContOnCl, Differentiable.pow, Complex.differentiable_exp, PhragmenLindelof.right_half_plane_of_tendsto_zero_on_real, LT.lt.le
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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)
refine_3 : ∀ (y : ℝ), ‖g n ((↑y : ℂ) * I)‖ ≤ C
⊢ ‖g n z‖ ≤ C

Tactic:
refine right_half_plane_of_tendsto_zero_on_real ((differentiable_exp.pow n).diffContOnCl.smul hd)
    ?_ ?_ (fun y => ?_) hz.le

Premises used: DiffContOnCl.smul, Differentiable.diffContOnCl, Differentiable.pow, Complex.differentiable_exp, PhragmenLindelof.right_half_plane_of_tendsto_zero_on_real, LT.lt.le
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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 : ℝ) (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)
⊢ ∃ 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⟩
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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)

Tactic:
⟨max c 1, max_lt hc one_lt_two, n + max B 0, .of_norm_left ?_⟩

Premises used: Nat.cast, max_lt, HAdd.hAdd, Max.max, And.intro, Exists.intro, one_lt_two, OfNat.ofNat, Asymptotics.IsBigO.of_norm_left
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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)
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)
⊢ ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) (g n) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)

Tactic:
refine ⟨max c 1, max_lt hc one_lt_two, n + max B 0, .of_norm_left ?_⟩
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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)
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)
⊢ 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:
simp only [hg]
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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)

Tactic:
((isBigO_refl (fun z : ℂ => expR z.re ^ n) _).mul hO.norm_left).trans (.of_bound' ?_)

Premises used: Asymptotics.IsBigO.norm_left, Asymptotics.IsBigO.mul, Real.exp, Asymptotics.IsBigO.trans, Complex.re, HPow.hPow, Asymptotics.IsBigO.of_bound', Asymptotics.isBigO_refl
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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)
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)‖
⊢ 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:
refine ((isBigO_refl (fun z : ℂ => expR z.re ^ n) _).mul hO.norm_left).trans (.of_bound' ?_)

Premises used: Asymptotics.IsBigO.norm_left, Asymptotics.IsBigO.mul, Real.exp, Asymptotics.IsBigO.trans, Complex.re, HPow.hPow, Asymptotics.IsBigO.of_bound', Asymptotics.isBigO_refl
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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)
h : ∀ (z : ℂ) (hz : 1 ≤ ‖z‖), ‖expR z.re ^ n * expR (B * ‖z‖ ^ c)‖ ≤ ‖expR (((↑n : ℝ) + max B 0) * ‖z‖ ^ max c 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:
filter_upwards [(eventually_cobounded_le_norm 1).filter_mono inf_le_left] with z hz

Premises used: Filter.Eventually.filter_mono, eventually_cobounded_le_norm, inf_le_left, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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 : expR ((↑n : ℝ) * z.re + B * ‖z‖ ^ c) ≤ expR ((↑n : ℝ) * ‖z‖ ^ max c 1 + max B 0 * ‖z‖ ^ max c 1)
⊢ ‖expR z.re ^ n * expR (B * ‖z‖ ^ c)‖ ≤ ‖expR (((↑n : ℝ) + 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]

Premises used: add_mul, Real.exp_nat_mul, Real.exp_add, Real.norm_eq_abs, Real.abs_exp
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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
h₂ : c ≤ max c 1
⊢ expR ((↑n : ℝ) * z.re + B * ‖z‖ ^ c) ≤ expR ((↑n : ℝ) * ‖z‖ ^ max c 1 + max B 0 * ‖z‖ ^ max c 1)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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‖
⊢ z.re ≤ ‖z‖

Tactic:
re_le_norm _

Premises used: Complex.re_le_norm
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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‖
⊢ ‖z‖ = HPow.hPow (β := ℝ) ‖z‖ 1

Tactic:
(Real.rpow_one _).symm

Premises used: Real.rpow_one, Eq.symm
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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‖
⊢ HPow.hPow (β := ℝ) ‖z‖ 1 ≤ ‖z‖ ^ max c 1

Tactic:
Real.rpow_le_rpow_of_exponent_le hz (le_max_right _ _)

Premises used: le_max_right, Real.rpow_le_rpow_of_exponent_le
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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‖
⊢ z.re ≤ ‖z‖ ^ max c 1

Tactic:
calc
        z.re ≤ ‖z‖ := re_le_norm _
        _ = ‖z‖ ^ (1 : ℝ) := (Real.rpow_one _).symm
        _ ≤ ‖z‖ ^ max c 1 := Real.rpow_le_rpow_of_exponent_le hz (le_max_right _ _)

Premises used: le_max_right, Real.rpow_one, Complex.re, Complex.re_le_norm, Max.max, OfNat.ofNat, Eq.symm, Real.rpow_le_rpow_of_exponent_le
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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‖
⊢ B ≤ max B 0

Tactic:
le_max_left _ _

Premises used: le_max_left
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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‖
⊢ c ≤ max c 1

Tactic:
le_max_left _ _

Premises used: le_max_left
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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‖
⊢ B ≤ max B 0

Tactic:
exacts [le_max_left _ _, le_max_left _ _]

Premises used: le_max_left
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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_2 : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖g n (↑x : ℂ)‖) atTop (𝓝 0)
⊢ Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ g n (↑x : ℂ)) atTop (𝓝 0)

Tactic:
rw [tendsto_zero_iff_norm_tendsto_zero]

Premises used: tendsto_zero_iff_norm_tendsto_zero
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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_2 : Tendsto (β := ℝ) (fun (x : ℝ) ↦ expR (↑x : ℂ).re ^ n * ‖f (↑x : ℂ)‖) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖g n (↑x : ℂ)‖) atTop (𝓝 0)

Tactic:
simp only [hg]
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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 : ℝ) ↦ expR (↑x : ℂ).re ^ n * ‖f (↑x : ℂ)‖) atTop (𝓝 0)

Tactic:
hre n
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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 : ℝ) ↦ expR (↑x : ℂ).re ^ n * ‖f (↑x : ℂ)‖) atTop (𝓝 0)

Tactic:
exact hre n
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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 : ℝ
refine_3 : ‖f ((↑y : ℂ) * I)‖ ≤ C
⊢ ‖g n ((↑y : ℂ) * I)‖ ≤ C

Tactic:
rw [hg, re_ofReal_mul, I_re, mul_zero, Real.exp_zero, one_pow, one_mul]

Premises used: one_pow, Complex.I_re, MulZeroClass.mul_zero, Real.exp_zero, one_mul, Complex.re_ofReal_mul
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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 : ℝ
⊢ ‖f ((↑y : ℂ) * I)‖ ≤ C

Tactic:
hC y
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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 : ℝ
⊢ ‖f ((↑y : ℂ) * I)‖ ≤ C

Tactic:
exact hC y
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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
this : EqOn (f - g) 0 {z : ℂ | 0 ≤ z.re}
⊢ EqOn f g {z : ℂ | 0 ≤ z.re}

Tactic:
simpa only [EqOn, Pi.sub_apply, Pi.zero_apply, sub_eq_zero] using this

Premises used: sub_eq_zero, Pi.zero_apply, Set.EqOn, Pi.sub_apply
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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
suffices : EqOn (f - g) 0 {z : ℂ | 0 ≤ z.re}
⊢ EqOn f g {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
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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}

Tactic:
eq_zero_on_right_half_plane_of_superexponential_decay (hfd.sub hgd) ?_ hre ?_

Premises used: PhragmenLindelof.eq_zero_on_right_half_plane_of_superexponential_decay, DiffContOnCl.sub
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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)
refine_2 : ∃ (C : ℝ), ∀ (x : ℝ), ‖(f - g) ((↑x : ℂ) * I)‖ ≤ C
⊢ EqOn (f - g) 0 {z : ℂ | 0 ≤ z.re}

Tactic:
refine eq_zero_on_right_half_plane_of_superexponential_decay (hfd.sub hgd) ?_ hre ?_

Premises used: PhragmenLindelof.eq_zero_on_right_half_plane_of_superexponential_decay, DiffContOnCl.sub
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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 < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) (f - g) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)

Tactic:
isBigO_sub_exp_rpow hfexp hgexp

Premises used: PhragmenLindelof.isBigO_sub_exp_rpow