awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
hBf : ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ l) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hBg : ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ l) g fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
⊢ ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ l) (f - g) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
have this : ∀ {c₁ c₂ B₁ B₂ : ℝ},
  c₁ ≤ c₂ →
    0 ≤ B₂ →
      B₁ ≤ B₂ →
        IsBigO (E := ℝ) (F := ℝ) (cobounded ℂ ⊓ l) (fun (z : ℂ) ↦ expR (B₁ * ‖z‖ ^ c₁)) fun (z : ℂ) ↦
          expR (B₂ * ‖z‖ ^ c₂)
Tactic: have : ∀ {c₁ c₂ B₁ B₂ : ℝ}, c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ →
      (fun z : ℂ => expR (B₁ * ‖z‖ ^ c₁)) =O[cobounded ℂ ⊓ l]
        fun z => expR (B₂ * ‖z‖ ^ c₂) := fun hc hB₀ hB ↦ .of_norm_eventuallyLE <| by
    filter_upwards [(eventually_cobounded_le_norm 1).filter_mono inf_le_left] with z hz
    simp only [Real.norm_eq_abs, Real.abs_exp]
    gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
hBf : ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ l) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hBg : ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ l) g fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ →
      0 ≤ B₂ →
        B₁ ≤ B₂ →
          IsBigO (E := ℝ) (F := ℝ) (cobounded ℂ ⊓ l) (fun (z : ℂ) ↦ expR (B₁ * ‖z‖ ^ c₁)) fun (z : ℂ) ↦
            expR (B₂ * ‖z‖ ^ c₂)
⊢ ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ l) (f - g) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
have rcases : ∀ (cf : ℝ) (hcf : cf < a) (Bf : ℝ) (hOf : IsBigO (F := ℝ) (cobounded ℂ ⊓ l) f fun (z : ℂ) ↦ expR (Bf * ‖z‖ ^ cf)),
  ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ l) (f - g) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
Tactic: rcases hBf with ⟨cf, hcf, Bf, hOf⟩
Cleared hypotheses: hBf
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
hBg : ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ l) g fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ →
      0 ≤ B₂ →
        B₁ ≤ B₂ →
          IsBigO (E := ℝ) (F := ℝ) (cobounded ℂ ⊓ l) (fun (z : ℂ) ↦ expR (B₁ * ‖z‖ ^ c₁)) fun (z : ℂ) ↦
            expR (B₂ * ‖z‖ ^ c₂)
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : IsBigO (F := ℝ) (cobounded ℂ ⊓ l) f fun (z : ℂ) ↦ expR (Bf * ‖z‖ ^ cf)
⊢ ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ l) (f - g) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
have rcases : ∀ (cg : ℝ) (hcg : cg < a) (Bg : ℝ) (hOg : IsBigO (F := ℝ) (cobounded ℂ ⊓ l) g fun (z : ℂ) ↦ expR (Bg * ‖z‖ ^ cg)),
  ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ l) (f - g) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
Tactic: rcases hBg with ⟨cg, hcg, Bg, hOg⟩
Cleared hypotheses: hBg
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ →
      0 ≤ B₂ →
        B₁ ≤ B₂ →
          IsBigO (E := ℝ) (F := ℝ) (cobounded ℂ ⊓ l) (fun (z : ℂ) ↦ expR (B₁ * ‖z‖ ^ c₁)) fun (z : ℂ) ↦
            expR (B₂ * ‖z‖ ^ c₂)
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : IsBigO (F := ℝ) (cobounded ℂ ⊓ l) f fun (z : ℂ) ↦ expR (Bf * ‖z‖ ^ cf)
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : IsBigO (F := ℝ) (cobounded ℂ ⊓ l) g fun (z : ℂ) ↦ expR (Bg * ‖z‖ ^ cg)
⊢ ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ l) (f - g) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
have refine : IsBigO (F := ℝ) (cobounded ℂ ⊓ l) (f - g) fun (z : ℂ) ↦ expR (max 0 (max Bf Bg) * ‖z‖ ^ max cf cg)
Tactic: refine ⟨max cf cg, max_lt hcf hcg, max 0 (max Bf Bg), ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ →
      0 ≤ B₂ →
        B₁ ≤ B₂ →
          IsBigO (E := ℝ) (F := ℝ) (cobounded ℂ ⊓ l) (fun (z : ℂ) ↦ expR (B₁ * ‖z‖ ^ c₁)) fun (z : ℂ) ↦
            expR (B₂ * ‖z‖ ^ c₂)
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : IsBigO (F := ℝ) (cobounded ℂ ⊓ l) f fun (z : ℂ) ↦ expR (Bf * ‖z‖ ^ cf)
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : IsBigO (F := ℝ) (cobounded ℂ ⊓ l) g fun (z : ℂ) ↦ expR (Bg * ‖z‖ ^ cg)
⊢ IsBigO (F := ℝ) (cobounded ℂ ⊓ l) (f - g) fun (z : ℂ) ↦ expR (max 0 (max Bf Bg) * ‖z‖ ^ max cf cg)
have refine_1 : cf ≤ max cf cg
Tactic: refine (hOf.trans <| this ?_ ?_ ?_).sub (hOg.trans <| this ?_ ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ →
      0 ≤ B₂ →
        B₁ ≤ B₂ →
          IsBigO (E := ℝ) (F := ℝ) (cobounded ℂ ⊓ l) (fun (z : ℂ) ↦ expR (B₁ * ‖z‖ ^ c₁)) fun (z : ℂ) ↦
            expR (B₂ * ‖z‖ ^ c₂)
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : IsBigO (F := ℝ) (cobounded ℂ ⊓ l) f fun (z : ℂ) ↦ expR (Bf * ‖z‖ ^ cf)
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : IsBigO (F := ℝ) (cobounded ℂ ⊓ l) g fun (z : ℂ) ↦ expR (Bg * ‖z‖ ^ cg)
refine_1 : cf ≤ max cf cg
⊢ IsBigO (F := ℝ) (cobounded ℂ ⊓ l) (f - g) fun (z : ℂ) ↦ expR (max 0 (max Bf Bg) * ‖z‖ ^ max cf cg)
have refine_2 : 0 ≤ max 0 (max Bf Bg)
Tactic: refine (hOf.trans <| this ?_ ?_ ?_).sub (hOg.trans <| this ?_ ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ →
      0 ≤ B₂ →
        B₁ ≤ B₂ →
          IsBigO (E := ℝ) (F := ℝ) (cobounded ℂ ⊓ l) (fun (z : ℂ) ↦ expR (B₁ * ‖z‖ ^ c₁)) fun (z : ℂ) ↦
            expR (B₂ * ‖z‖ ^ c₂)
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : IsBigO (F := ℝ) (cobounded ℂ ⊓ l) f fun (z : ℂ) ↦ expR (Bf * ‖z‖ ^ cf)
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : IsBigO (F := ℝ) (cobounded ℂ ⊓ l) g fun (z : ℂ) ↦ expR (Bg * ‖z‖ ^ cg)
refine_1 : cf ≤ max cf cg
refine_2 : 0 ≤ max 0 (max Bf Bg)
⊢ IsBigO (F := ℝ) (cobounded ℂ ⊓ l) (f - g) fun (z : ℂ) ↦ expR (max 0 (max Bf Bg) * ‖z‖ ^ max cf cg)
have refine_3 : Bf ≤ max 0 (max Bf Bg)
Tactic: refine (hOf.trans <| this ?_ ?_ ?_).sub (hOg.trans <| this ?_ ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ →
      0 ≤ B₂ →
        B₁ ≤ B₂ →
          IsBigO (E := ℝ) (F := ℝ) (cobounded ℂ ⊓ l) (fun (z : ℂ) ↦ expR (B₁ * ‖z‖ ^ c₁)) fun (z : ℂ) ↦
            expR (B₂ * ‖z‖ ^ c₂)
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : IsBigO (F := ℝ) (cobounded ℂ ⊓ l) f fun (z : ℂ) ↦ expR (Bf * ‖z‖ ^ cf)
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : IsBigO (F := ℝ) (cobounded ℂ ⊓ l) g fun (z : ℂ) ↦ expR (Bg * ‖z‖ ^ cg)
refine_1 : cf ≤ max cf cg
refine_2 : 0 ≤ max 0 (max Bf Bg)
refine_3 : Bf ≤ max 0 (max Bf Bg)
⊢ IsBigO (F := ℝ) (cobounded ℂ ⊓ l) (f - g) fun (z : ℂ) ↦ expR (max 0 (max Bf Bg) * ‖z‖ ^ max cf cg)
have refine_4 : cg ≤ max cf cg
Tactic: refine (hOf.trans <| this ?_ ?_ ?_).sub (hOg.trans <| this ?_ ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ →
      0 ≤ B₂ →
        B₁ ≤ B₂ →
          IsBigO (E := ℝ) (F := ℝ) (cobounded ℂ ⊓ l) (fun (z : ℂ) ↦ expR (B₁ * ‖z‖ ^ c₁)) fun (z : ℂ) ↦
            expR (B₂ * ‖z‖ ^ c₂)
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : IsBigO (F := ℝ) (cobounded ℂ ⊓ l) f fun (z : ℂ) ↦ expR (Bf * ‖z‖ ^ cf)
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : IsBigO (F := ℝ) (cobounded ℂ ⊓ l) g fun (z : ℂ) ↦ expR (Bg * ‖z‖ ^ cg)
refine_1 : cf ≤ max cf cg
refine_2 : 0 ≤ max 0 (max Bf Bg)
refine_3 : Bf ≤ max 0 (max Bf Bg)
refine_4 : cg ≤ max cf cg
refine_5 : 0 ≤ max 0 (max Bf Bg)
⊢ IsBigO (F := ℝ) (cobounded ℂ ⊓ l) (f - g) fun (z : ℂ) ↦ expR (max 0 (max Bf Bg) * ‖z‖ ^ max cf cg)
have refine_6 : Bg ≤ max 0 (max Bf Bg)
Tactic: refine (hOf.trans <| this ?_ ?_ ?_).sub (hOg.trans <| this ?_ ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hza : a ≤ z.im
hzb : z.im ≤ b
⊢ ‖f z‖ ≤ C
have hza₁ : a = z.im ∨ a < z.im
Tactic: rw [le_iff_eq_or_lt] at hza hzb
Cleared hypotheses: hza, hzb
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hza : a ≤ z.im
hzb : z.im ≤ b
hza₁ : a = z.im ∨ a < z.im
⊢ ‖f z‖ ≤ C
have hzb₁ : z.im = b ∨ z.im < b
Tactic: rw [le_iff_eq_or_lt] at hza hzb
Cleared hypotheses: hza, hzb
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hza : a = z.im ∨ a < z.im
hzb : z.im = b ∨ z.im < b
⊢ ‖f z‖ ≤ C
have inl : ∀ (hza : a = z.im), ‖f z‖ ≤ C
Tactic: rcases hza with hza | hza
Cleared hypotheses: hza
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hza : a = z.im ∨ a < z.im
hzb : z.im = b ∨ z.im < b
inl : ∀ (hza : a = z.im), ‖f z‖ ≤ C
⊢ ‖f z‖ ≤ C
have inr : ∀ (hza : a < z.im), ‖f z‖ ≤ C
Tactic: rcases hza with hza | hza
Cleared hypotheses: hza
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hzb : z.im = b ∨ z.im < b
hza : a < z.im
⊢ ‖f z‖ ≤ C
have inr : ∀ (hzb : z.im = b), ‖f z‖ ≤ C
Tactic: rcases hzb with hzb | hzb
Cleared hypotheses: hzb
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hzb : z.im = b ∨ z.im < b
hza : a < z.im
inr : ∀ (hzb : z.im = b), ‖f z‖ ≤ C
⊢ ‖f z‖ ≤ C
have inr₁ : ∀ (hzb : z.im < b), ‖f z‖ ≤ C
Tactic: rcases hzb with hzb | hzb
Cleared hypotheses: hzb
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hza : a < z.im
hzb : z.im < b
⊢ ‖f z‖ ≤ C
have inr : ∀
  (this :
    ∀ {C : ℝ} (hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C) (hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C) (hC₀ : 0 < C),
      ‖f z‖ ≤ C)
  (hC₀ : ¬0 < C), ‖f z‖ ≤ C
Tactic: wlog hC₀ : 0 < C generalizing C
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hza : a < z.im
hzb : z.im < b
inr :
  ∀
    (this :
      ∀ {C : ℝ} (hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C) (hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C) (hC₀ : 0 < C),
        ‖f z‖ ≤ C)
    (hC₀ : ¬0 < C), ‖f z‖ ≤ C
⊢ ‖f z‖ ≤ C
have wlog : ∀ {C : ℝ} (hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C) (hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C) (hC₀ : 0 < C), ‖f z‖ ≤ C
Tactic: wlog hC₀ : 0 < C generalizing C
Cleared hypotheses: hle_a, hle_b
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hza : a < z.im
hzb : z.im < b
this :
  ∀ {C : ℝ} (hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C) (hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C) (hC₀ : 0 < C), ‖f z‖ ≤ C
hC₀ : ¬0 < C
⊢ ‖f z‖ ≤ C
have inr : ∀ (C' : ℝ) (hC' : C < C') (w : ℂ) (hw : w.im = a), ‖f w‖ ≤ C'
Tactic: refine le_of_forall_gt_imp_ge_of_dense fun C' hC' => this (fun w hw => ?_) (fun w hw => ?_) ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hza : a < z.im
hzb : z.im < b
this :
  ∀ {C : ℝ} (hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C) (hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C) (hC₀ : 0 < C), ‖f z‖ ≤ C
hC₀ : ¬0 < C
inr : ∀ (C' : ℝ) (hC' : C < C') (w : ℂ) (hw : w.im = a), ‖f w‖ ≤ C'
⊢ ‖f z‖ ≤ C
have inr₁ : ∀ (C' : ℝ) (hC' : C < C') (w : ℂ) (hw : w.im = b), ‖f w‖ ≤ C'
Tactic: refine le_of_forall_gt_imp_ge_of_dense fun C' hC' => this (fun w hw => ?_) (fun w hw => ?_) ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hza : a < z.im
hzb : z.im < b
this :
  ∀ {C : ℝ} (hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C) (hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C) (hC₀ : 0 < C), ‖f z‖ ≤ C
hC₀ : ¬0 < C
inr : ∀ (C' : ℝ) (hC' : C < C') (w : ℂ) (hw : w.im = a), ‖f w‖ ≤ C'
inr₁ : ∀ (C' : ℝ) (hC' : C < C') (w : ℂ) (hw : w.im = b), ‖f w‖ ≤ C'
⊢ ‖f z‖ ≤ C
have inr₂ : ∀ (C' : ℝ) (hC' : C < C'), 0 < C'
Tactic: refine le_of_forall_gt_imp_ge_of_dense fun C' hC' => this (fun w hw => ?_) (fun w hw => ?_) ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hza : a < z.im
hzb : z.im < b
this :
  ∀ {C : ℝ} (hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C) (hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C) (hC₀ : 0 < C), ‖f z‖ ≤ C
hC₀ : ¬0 < C
C' : ℝ
hC' : C < C'
⊢ 0 < C'
have inr : ((↑a : ℂ) * I).im = a
Tactic: refine ((norm_nonneg (f (a * I))).trans (hle_a _ ?_)).trans_lt hC'
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hza : a < z.im
hzb : z.im < b
this :
  ∀ {C : ℝ} (hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C) (hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C) (hC₀ : 0 < C), ‖f z‖ ≤ C
hC₀ : ¬0 < C
C' : ℝ
hC' : C < C'
⊢ ((↑a : ℂ) * I).im = a
have inr : (↑a : ℂ).re = a
Tactic: rw [mul_I_im, ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hza : a < z.im
hzb : z.im < b
this :
  ∀ {C : ℝ} (hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C) (hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C) (hC₀ : 0 < C), ‖f z‖ ≤ C
hC₀ : ¬0 < C
C' : ℝ
hC' : C < C'
inr : (↑a : ℂ).re = a
⊢ ((↑a : ℂ) * I).im = a
have inr₁ : a = a
Tactic: rw [mul_I_im, ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C_1 : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
hza : a < z.im
hzb : z.im < b
C : ℝ
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hC₀ : 0 < C
⊢ ‖f z‖ ≤ C
have obtain : ∀ (a b : ℝ) (hza : a - b < z.im) (hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C) (hzb : z.im < a + b)
  (hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C) (hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b)))
  (hB :
    ∃ c < π / (a + b - (a - b)),
      ∃ (B : ℝ),
        IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun (z : ℂ) ↦
          expR (B * expR (c * |z.re|))),
  ‖f z‖ ≤ C
Tactic: obtain ⟨a, b, rfl, rfl⟩ : ∃ a' b', a = a' - b' ∧ b = a' + b' :=
    ⟨(a + b) / 2, (b - a) / 2, by ring, by ring⟩
Cleared hypotheses: a, b, hfd, hB, hza, hzb, hle_a, hle_b
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C_1 : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hB :
  ∃ c < π / (a + b - (a - b)),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun (z : ℂ) ↦
        expR (B * expR (c * |z.re|))
⊢ ‖f z‖ ≤ C
have hab : a - b < a + b
Tactic: have hab : a - b < a + b := hza.trans hzb
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C_1 : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hB :
  ∃ c < π / (a + b - (a - b)),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun (z : ℂ) ↦
        expR (B * expR (c * |z.re|))
hab : a - b < a + b
⊢ ‖f z‖ ≤ C
have hb : 0 < b
Tactic: have hb : 0 < b := by simpa only [sub_eq_add_neg, add_lt_add_iff_left, neg_lt_self_iff] using hab
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C_1 : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hB :
  ∃ c < π / (a + b - (a - b)),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun (z : ℂ) ↦
        expR (B * expR (c * |z.re|))
hab : a - b < a + b
hb : 0 < b
⊢ ‖f z‖ ≤ C
have hB₁ : ∃ c < π / 2 / b,
  ∃ (B : ℝ),
    IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun (z : ℂ) ↦
      expR (B * expR (c * |z.re|))
Tactic: rw [add_sub_sub_cancel, ← two_mul, div_mul_eq_div_div] at hB
Cleared hypotheses: hB, hab, hb
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C_1 : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hB :
  ∃ c < π / 2 / b,
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun (z : ℂ) ↦
        expR (B * expR (c * |z.re|))
hab : a - b < a + b
hb : 0 < b
⊢ ‖f z‖ ≤ C
have hπb : 0 < π / 2 / b
Tactic: have hπb : 0 < π / 2 / b := div_pos Real.pi_div_two_pos hb
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C_1 : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hB :
  ∃ c < π / 2 / b,
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun (z : ℂ) ↦
        expR (B * expR (c * |z.re|))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
⊢ ‖f z‖ ≤ C
have rcases : ∀ (c : ℝ) (hc : c < π / 2 / b) (B : ℝ)
  (hO :
    IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun (z : ℂ) ↦
      expR (B * expR (c * |z.re|))),
  ‖f z‖ ≤ C
Tactic: rcases hB with ⟨c, hc, B, hO⟩
Cleared hypotheses: hB
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C_1 : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO :
  IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
⊢ ‖f z‖ ≤ C
have obtain : ∀ (d : ℝ) (hd : d < π / 2 / b) (hcd : c < d) (hd₀ : 0 < d), ‖f z‖ ≤ C
Tactic: obtain ⟨d, ⟨hcd, hd₀⟩, hd⟩ : ∃ d, (c < d ∧ 0 < d) ∧ d < π / 2 / b := by
    simpa only [max_lt_iff] using exists_between (max_lt hc hπb)