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
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 : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
⊢ ∀ {z : ℂ} (hz : 0 ≤ z.re), ‖f z‖ ≤ C
have obtain : ∀ (x₀ : ℝ) (hx₀ : 0 ≤ x₀) (hmax : ∀ (y : ℝ), 0 ≤ y → ‖f (↑y : ℂ)‖ ≤ ‖f (↑x₀ : ℂ)‖) {z : ℂ} (hz : 0 ≤ z.re), ‖f z‖ ≤ C
Tactic: obtain ⟨x₀, hx₀, hmax⟩ : ∃ x : ℝ, 0 ≤ x ∧ ∀ y : ℝ, 0 ≤ y → ‖f y‖ ≤ ‖f x‖ := by
    have hfc : ContinuousOn (fun x : ℝ => f x) (Ici 0) := by
      refine hd.continuousOn.comp continuous_ofReal.continuousOn fun x hx => ?_
      rwa [closure_setOf_lt_re]
    by_cases! h₀ : ∀ x : ℝ, 0 ≤ x → f x = 0
    · refine ⟨0, le_rfl, fun y hy => ?_⟩; rw [h₀ y hy, h₀ 0 le_rfl]
    rcases h₀ with ⟨x₀, hx₀, hne⟩
    have hlt : ‖(0 : E)‖ < ‖f x₀‖ := by rwa [norm_zero, norm_pos_iff]
    suffices ∀ᶠ x : ℝ in cocompact ℝ ⊓ 𝓟 (Ici 0), ‖f x‖ ≤ ‖f x₀‖ by
      simpa only [exists_prop] using hfc.norm.exists_isMaxOn' isClosed_Ici hx₀ this
    rw [cocompact_eq_atBot_atTop, inf_sup_right, (disjoint_atBot_principal_Ici (0 : ℝ)).eq_bot,
      bot_sup_eq]
    exact (hre.norm.eventually <| ge_mem_nhds hlt).filter_mono inf_le_left
-- 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
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 : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
hmax : ∀ (y : ℝ), 0 ≤ y → ‖f (↑y : ℂ)‖ ≤ ‖f (↑x₀ : ℂ)‖
⊢ ∀ {z : ℂ} (hz : 0 ≤ z.re), ‖f z‖ ≤ C
have inl : ∀ (h : ‖f (↑x₀ : ℂ)‖ ≤ C) {z : ℂ} (hz : 0 ≤ z.re), ‖f z‖ ≤ C
Tactic: rcases le_or_gt ‖f x₀‖ C with h | h
-- 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
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 : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
hmax : ∀ (y : ℝ), 0 ≤ y → ‖f (↑y : ℂ)‖ ≤ ‖f (↑x₀ : ℂ)‖
inl : ∀ (h : ‖f (↑x₀ : ℂ)‖ ≤ C) {z : ℂ} (hz : 0 ≤ z.re), ‖f z‖ ≤ C
⊢ ∀ {z : ℂ} (hz : 0 ≤ z.re), ‖f z‖ ≤ C
have inr : ∀ (h : C < ‖f (↑x₀ : ℂ)‖) {z : ℂ} (hz : 0 ≤ z.re), ‖f z‖ ≤ C
Tactic: rcases le_or_gt ‖f x₀‖ C with h | h
-- 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
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 : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
hmax : ∀ (y : ℝ), 0 ≤ y → ‖f (↑y : ℂ)‖ ≤ ‖f (↑x₀ : ℂ)‖
h : C < ‖f (↑x₀ : ℂ)‖
⊢ ∀ {z : ℂ} (hz : 0 ≤ z.re), ‖f z‖ ≤ C
have hmax₁ : IsMaxOn (norm ∘ f) {z : ℂ | 0 < z.re} (↑x₀ : ℂ)
Tactic: replace hmax : IsMaxOn (norm ∘ f) {z | 0 < z.re} x₀ := by
      rintro z (hz : 0 < z.re)
      simpa [max_eq_right h.le] using hle _ hmax _ hz.le
Cleared hypotheses: hmax
-- 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
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 : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
h : C < ‖f (↑x₀ : ℂ)‖
hmax : IsMaxOn (norm ∘ f) {z : ℂ | 0 < z.re} (↑x₀ : ℂ)
⊢ ‖f 0‖ = ‖f (↑x₀ : ℂ)‖
have apply : ball (↑x₀ : ℂ) (dist 0 (↑x₀ : ℂ)) ⊆ {z : ℂ | 0 < z.re}
Tactic: apply norm_eq_norm_of_isMaxOn_of_ball_subset hd hmax
-- 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
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 : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
h : C < ‖f (↑x₀ : ℂ)‖
hmax : IsMaxOn (norm ∘ f) {z : ℂ | 0 < z.re} (↑x₀ : ℂ)
z : ℂ
hz : z ∈ ball (↑x₀ : ℂ) (dist 0 (↑x₀ : ℂ))
⊢ Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.re} z
have hz₁ : ‖z - (↑x₀ : ℂ)‖ < x₀
Tactic: rw [mem_ball, dist_zero_left, dist_eq, Complex.norm_of_nonneg hx₀] at hz
Cleared hypotheses: hz
-- 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
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 : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
h : C < ‖f (↑x₀ : ℂ)‖
hmax : IsMaxOn (norm ∘ f) {z : ℂ | 0 < z.re} (↑x₀ : ℂ)
z : ℂ
hz : ‖z - (↑x₀ : ℂ)‖ < x₀
⊢ 0 < z.re
have contrapose! : ∀ (hz : z.re ≤ 0), x₀ ≤ ‖z - (↑x₀ : ℂ)‖
Tactic: contrapose! hz
Cleared hypotheses: hz
-- 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
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 : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
h : C < ‖f (↑x₀ : ℂ)‖
hmax : IsMaxOn (norm ∘ f) {z : ℂ | 0 < z.re} (↑x₀ : ℂ)
z : ℂ
hz : z.re ≤ 0
⊢ |x₀ - z.re| = |(z - (↑x₀ : ℂ)).re|
have rw : |x₀ - z.re| = |z.re - (↑x₀ : ℂ).re|
Tactic: rw [sub_re, ofReal_re, _root_.abs_sub_comm]
-- 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
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 : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
h : C < ‖f (↑x₀ : ℂ)‖
hmax : IsMaxOn (norm ∘ f) {z : ℂ | 0 < z.re} (↑x₀ : ℂ)
z : ℂ
hz : z.re ≤ 0
rw : |x₀ - z.re| = |z.re - (↑x₀ : ℂ).re|
⊢ |x₀ - z.re| = |(z - (↑x₀ : ℂ)).re|
have rw₁ : |x₀ - z.re| = |z.re - x₀|
Tactic: rw [sub_re, ofReal_re, _root_.abs_sub_comm]
-- 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
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 : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
h : C < ‖f (↑x₀ : ℂ)‖
hmax : IsMaxOn (norm ∘ f) {z : ℂ | 0 < z.re} (↑x₀ : ℂ)
z : ℂ
hz : z.re ≤ 0
rw : |x₀ - z.re| = |z.re - (↑x₀ : ℂ).re|
rw₁ : |x₀ - z.re| = |z.re - x₀|
⊢ |x₀ - z.re| = |(z - (↑x₀ : ℂ)).re|
have rw₂ : |z.re - x₀| = |z.re - x₀|
Tactic: rw [sub_re, ofReal_re, _root_.abs_sub_comm]
-- 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
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 : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
h : C < ‖f (↑x₀ : ℂ)‖
hmax : IsMaxOn (norm ∘ f) {z : ℂ | 0 < z.re} (↑x₀ : ℂ)
z : ℂ
hz : z.re ≤ 0
⊢ x₀ ≤ ‖z - (↑x₀ : ℂ)‖
have x₁ : |x₀ - z.re| = |(z - (↑x₀ : ℂ)).re|
Tactic: calc
        x₀ ≤ x₀ - z.re := (le_sub_self_iff _).2 hz
        _ ≤ |x₀ - z.re| := le_abs_self _
        _ = |(z - x₀).re| := by rw [sub_re, ofReal_re, _root_.abs_sub_comm]
        _ ≤ ‖z - x₀‖ := abs_re_le_norm _
-- 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
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 : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
h : C < ‖f (↑x₀ : ℂ)‖
hmax : IsMaxOn (norm ∘ f) {z : ℂ | 0 < z.re} (↑x₀ : ℂ)
⊢ ∀ {z : ℂ} (hz : 0 ≤ z.re), ‖f z‖ ≤ C
have this : ‖f 0‖ = ‖f (↑x₀ : ℂ)‖
Tactic: have : ‖f 0‖ = ‖f x₀‖ := by
      apply norm_eq_norm_of_isMaxOn_of_ball_subset hd hmax
      -- move to a lemma?
      intro z hz
      rw [mem_ball, dist_zero_left, dist_eq, Complex.norm_of_nonneg hx₀] at hz
      rw [mem_setOf_eq]
      contrapose! hz
      calc
        x₀ ≤ x₀ - z.re := (le_sub_self_iff _).2 hz
        _ ≤ |x₀ - z.re| := le_abs_self _
        _ = |(z - x₀).re| := by rw [sub_re, ofReal_re, _root_.abs_sub_comm]
        _ ≤ ‖z - x₀‖ := abs_re_le_norm _
-- 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
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 : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
h : C < ‖f (↑x₀ : ℂ)‖
hmax : IsMaxOn (norm ∘ f) {z : ℂ | 0 < z.re} (↑x₀ : ℂ)
this : ‖f 0‖ = ‖f (↑x₀ : ℂ)‖
⊢ ∀ {z : ℂ} (hz : 0 ≤ z.re), ‖f z‖ ≤ C
have inr : ‖f 0‖ ≤ C
Tactic: refine (h.not_ge <| this ▸ ?_).elim
-- 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 : ℂ
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 : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hz : 0 ≤ z.re
this : ∀ᶠ (ε : ℝ) in 𝓝[<] 0, ‖cexp ((↑ε : ℂ) * z) • f z‖ ≤ C
⊢ ‖f z‖ ≤ C
have refine : Tendsto (fun (c : ℝ) ↦ ‖cexp ((↑c : ℂ) * z) • f z‖) (𝓝 0) (𝓝 ‖f z‖)
Tactic: refine le_of_tendsto (Tendsto.mono_left ?_ nhdsWithin_le_nhds) this
-- 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 : ℂ
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 : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hz : 0 ≤ z.re
⊢ ‖f z‖ ≤ C
have suffices : ∀ᶠ (ε : ℝ) in 𝓝[<] 0, ‖cexp ((↑ε : ℂ) * z) • f z‖ ≤ C
Tactic: suffices ∀ᶠ ε : ℝ in 𝓝[<] 0, ‖exp (ε * z) • f z‖ ≤ C by
    refine le_of_tendsto (Tendsto.mono_left ?_ nhdsWithin_le_nhds) this
    exact Continuous.tendsto' (by fun_prop) _ _ (by simp)
-- 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 : ℂ
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 : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hz : 0 ≤ z.re
⊢ ∀ᶠ (ε : ℝ) in 𝓝[<] 0, ‖cexp ((↑ε : ℂ) * z) • f z‖ ≤ C
have h : ∀ (ε : ℝ) (ε₀ : Membership.mem (γ := Set ℝ) (Iio 0) ε), ‖cexp ((↑ε : ℂ) * z) • f z‖ ≤ C
Tactic: filter_upwards [self_mem_nhdsWithin] with ε ε₀
-- 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 : ℂ
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 : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : Membership.mem (γ := Set ℝ) (Iio 0) ε
⊢ ‖cexp ((↑ε : ℂ) * z) • f z‖ ≤ C
have ε₁ : ε < 0
Tactic: change ε < 0 at ε₀
Cleared hypotheses: ε₀
-- 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 : ℂ
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 : 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
⊢ ‖g z‖ ≤ C
have hd₁ : DiffContOnCl ℂ g {z : ℂ | 0 < z.re}
Tactic: replace hd : DiffContOnCl ℂ g {z : ℂ | 0 < z.re} :=
    (differentiable_id.const_mul _).cexp.diffContOnCl.smul hd
Cleared hypotheses: hd
-- 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 : ℂ
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_1.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun (z : ℂ) ↦ cexp ((↑ε : ℂ) * z) • f z
hd : DiffContOnCl ℂ g {z : ℂ | 0 < z.re}
z : ℂ
⊢ ‖g z‖ = expR (ε * z.re) * ‖f z‖
have rw : ‖cexp ((↑ε : ℂ) * z)‖ * ‖f z‖ = expR (ε * z.re) * ‖f z‖
Tactic: rw [norm_smul, norm_exp, re_ofReal_mul]
-- 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 : ℂ
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_1.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun (z : ℂ) ↦ cexp ((↑ε : ℂ) * z) • f z
hd : DiffContOnCl ℂ g {z : ℂ | 0 < z.re}
z : ℂ
rw : ‖cexp ((↑ε : ℂ) * z)‖ * ‖f z‖ = expR (ε * z.re) * ‖f z‖
⊢ ‖g z‖ = expR (ε * z.re) * ‖f z‖
have rw₁ : expR ((↑ε : ℂ) * z).re * ‖f z‖ = expR (ε * z.re) * ‖f z‖
Tactic: rw [norm_smul, norm_exp, re_ofReal_mul]
-- 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 : ℂ
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_1.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun (z : ℂ) ↦ cexp ((↑ε : ℂ) * z) • f z
hd : DiffContOnCl ℂ g {z : ℂ | 0 < z.re}
z : ℂ
rw : ‖cexp ((↑ε : ℂ) * z)‖ * ‖f z‖ = expR (ε * z.re) * ‖f z‖
rw₁ : expR ((↑ε : ℂ) * z).re * ‖f z‖ = expR (ε * z.re) * ‖f z‖
⊢ ‖g z‖ = expR (ε * z.re) * ‖f z‖
have rw₂ : expR (ε * z.re) * ‖f z‖ = expR (ε * z.re) * ‖f z‖
Tactic: rw [norm_smul, norm_exp, re_ofReal_mul]
-- 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}
⊢ ‖g z‖ ≤ C
have hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
Tactic: have hgn : ∀ z, ‖g z‖ = expR (ε * z.re) * ‖f z‖ := fun z ↦ by
    rw [norm_smul, norm_exp, re_ofReal_mul]
-- 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‖
⊢ ‖g z‖ ≤ C
have h : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) g fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
Tactic: refine right_half_plane_of_tendsto_zero_on_real hd ?_ ?_ (fun y => ?_) hz
-- 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‖
h : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) g fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
⊢ ‖g z‖ ≤ C
have h₁ : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ g (↑x : ℂ)) atTop (𝓝 0)
Tactic: refine right_half_plane_of_tendsto_zero_on_real hd ?_ ?_ (fun y => ?_) hz
-- 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‖
h : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) g fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
h₁ : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ g (↑x : ℂ)) atTop (𝓝 0)
⊢ ‖g z‖ ≤ C
have h₂ : ∀ (y : ℝ), ‖g ((↑y : ℂ) * I)‖ ≤ C
Tactic: refine right_half_plane_of_tendsto_zero_on_real hd ?_ ?_ (fun y => ?_) hz
-- 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‖
⊢ ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) g fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
have h : ∀ (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 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
C : ℝ
f : ℂ → E
z : ℂ
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‖
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 fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
have h : ∀ᶠ (x : ℂ) in cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}, ‖g x‖ ≤ ‖f x‖
Tactic: refine ⟨c, hc, B, .trans (.of_bound' ?_) hO⟩
-- 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 : ℂ
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‖
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}, ‖g x‖ ≤ ‖f x‖
have h : ∀ (z : ℂ) (hz : Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.re} z), ‖g z‖ ≤ ‖f z‖
Tactic: refine eventually_inf_principal.2 <| Eventually.of_forall fun z hz => ?_
-- 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
⊢ ‖g z‖ ≤ ‖f z‖
have h : expR (ε * z.re) * ‖f z‖ ≤ ‖f z‖
Tactic: rw [hgn]