awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
hfcts : ContinuousAt (update (β := fun (a : ℂ) ↦ ℂ) (f ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (f ∘ invQParam h))) 0
a y : ℂ
hy : y ≠ 0
⊢ update (β := fun (a : ℂ) ↦ ℂ) ((a • f) ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) ((a • f) ∘ invQParam h)) y =
    (a • update (β := fun (a : ℂ) ↦ ℂ) (f ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (f ∘ invQParam h))) y

Tactic:
simp [hy]
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
hfcts : ContinuousAt (cuspFunction h f) 0
⊢ cuspFunction h (-f) = -cuspFunction h f

Tactic:
simpa using cuspFunction_smul hfcts (-1)

Premises used: Function.Periodic.cuspFunction_smul, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f g : ℂ → ℂ
hfcts : ContinuousAt (cuspFunction h f) 0
hgcts : ContinuousAt (cuspFunction h g) 0
h₁ :
  ∀ (y : ℂ),
    update (β := fun (a : ℂ) ↦ ℂ) ((f + g) ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) ((f + g) ∘ invQParam h)) y =
      (update (β := fun (a : ℂ) ↦ ℂ) (f ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (f ∘ invQParam h)) +
          update (β := fun (a : ℂ) ↦ ℂ) (g ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (g ∘ invQParam h)))
        y
⊢ update (β := fun (a : ℂ) ↦ ℂ) ((f + g) ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) ((f + g) ∘ invQParam h)) =
    update (β := fun (a : ℂ) ↦ ℂ) (f ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (f ∘ invQParam h)) +
      update (β := fun (a : ℂ) ↦ ℂ) (g ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (g ∘ invQParam h))

Tactic:
ext y
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f g : ℂ → ℂ
hfcts : ContinuousAt (cuspFunction h f) 0
hgcts : ContinuousAt (cuspFunction h g) 0
y : ℂ
h₁ :
  ∀ (hy : y ≠ 0),
    update (β := fun (a : ℂ) ↦ ℂ) ((f + g) ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) ((f + g) ∘ invQParam h)) y =
      (update (β := fun (a : ℂ) ↦ ℂ) (f ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (f ∘ invQParam h)) +
          update (β := fun (a : ℂ) ↦ ℂ) (g ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (g ∘ invQParam h)))
        y
h₂ :
  update (β := fun (a : ℂ) ↦ ℂ) ((f + g) ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) ((f + g) ∘ invQParam h)) 0 =
    (update (β := fun (a : ℂ) ↦ ℂ) (f ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (f ∘ invQParam h)) +
        update (β := fun (a : ℂ) ↦ ℂ) (g ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (g ∘ invQParam h)))
      0
⊢ update (β := fun (a : ℂ) ↦ ℂ) ((f + g) ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) ((f + g) ∘ invQParam h)) y =
    (update (β := fun (a : ℂ) ↦ ℂ) (f ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (f ∘ invQParam h)) +
        update (β := fun (a : ℂ) ↦ ℂ) (g ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (g ∘ invQParam h)))
      y

Tactic:
obtain hy | rfl := ne_or_eq y 0

Premises used: ne_or_eq, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f g : ℂ → ℂ
hfcts : ContinuousAt (cuspFunction h f) 0
hgcts : ContinuousAt (cuspFunction h g) 0
y : ℂ
hy : y ≠ 0
⊢ update (β := fun (a : ℂ) ↦ ℂ) ((f + g) ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) ((f + g) ∘ invQParam h)) y =
    (update (β := fun (a : ℂ) ↦ ℂ) (f ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (f ∘ invQParam h)) +
        update (β := fun (a : ℂ) ↦ ℂ) (g ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (g ∘ invQParam h)))
      y

Tactic:
simp [hy]
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f g : ℂ → ℂ
hfcts : ContinuousAt (cuspFunction h f) 0
hgcts : ContinuousAt (cuspFunction h g) 0
⊢ update (β := fun (a : ℂ) ↦ ℂ) ((f + g) ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) ((f + g) ∘ invQParam h)) 0 =
    (update (β := fun (a : ℂ) ↦ ℂ) (f ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (f ∘ invQParam h)) +
        update (β := fun (a : ℂ) ↦ ℂ) (g ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (g ∘ invQParam h)))
      0

Tactic:
simpa using (tendsto_nhds_limUnder ⟨_, tendsto_nhds_zero hfcts⟩).add
      (tendsto_nhds_limUnder ⟨_, tendsto_nhds_zero hgcts⟩) |>.limUnder_eq

Premises used: Function.Periodic.tendsto_nhds_zero, tendsto_nhds_limUnder, Filter.Tendsto.add, Exists.intro, Filter.Tendsto.limUnder_eq
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f g : ℂ → ℂ
hfcts : ContinuousAt (cuspFunction h f) 0
hgcts : ContinuousAt (cuspFunction h g) 0
⊢ ContinuousAt (cuspFunction h (-g)) 0

Tactic:
simp [cuspFunction_neg, hgcts]

Premises used: Function.Periodic.cuspFunction_neg
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f g : ℂ → ℂ
hfcts : ContinuousAt (cuspFunction h f) 0
hgcts : ContinuousAt (cuspFunction h g) 0
⊢ cuspFunction h (f - g) = cuspFunction h f - cuspFunction h g

Tactic:
simpa [sub_eq_add_neg, ← cuspFunction_neg hgcts]
    using cuspFunction_add hfcts (by simp [cuspFunction_neg, hgcts])

Premises used: sub_eq_add_neg, Function.Periodic.cuspFunction_neg, Function.Periodic.cuspFunction_add
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
hBf : ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) l f fun (z : ℂ) ↦ expR (B * expR (c * |u z|))
hBg : ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) l g fun (z : ℂ) ↦ expR (B * expR (c * |u z|))
c₁ c₂ B₁ B₂ : ℝ
hc : c₁ ≤ c₂
hB₀ : 0 ≤ B₂
hB : B₁ ≤ B₂
z : ℂ
simp : expR (B₁ * expR (c₁ * |u z|)) ≤ expR (B₂ * expR (c₂ * |u z|))
⊢ ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖

Tactic:
simp only [Real.norm_eq_abs, Real.abs_exp]

Premises used: Real.norm_eq_abs, Real.abs_exp
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
hBf : ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) l f fun (z : ℂ) ↦ expR (B * expR (c * |u z|))
hBg : ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) l g fun (z : ℂ) ↦ expR (B * expR (c * |u z|))
c₁ c₂ B₁ B₂ : ℝ
hc : c₁ ≤ c₂
hB₀ : 0 ≤ B₂
hB : B₁ ≤ B₂
z : ℂ
a₁ : 0 ≤ expR (c₁ * |u z|)
a₂ : 0 ≤ B₂
a₃ : 0 ≤ |u z|
⊢ expR (B₁ * expR (c₁ * |u z|)) ≤ expR (B₂ * expR (c₂ * |u z|))

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
hBf : ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) l f fun (z : ℂ) ↦ expR (B * expR (c * |u z|))
hBg : ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) l g fun (z : ℂ) ↦ expR (B * expR (c * |u z|))
⊢ ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖

Tactic:
have : ∀ {c₁ c₂ B₁ B₂}, c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ z,
      ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖ := fun hc hB₀ hB z ↦ by
    simp only [Real.norm_eq_abs, Real.abs_exp]; gcongr
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
hBf : ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) l f fun (z : ℂ) ↦ expR (B * expR (c * |u z|))
hBg : ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) l g fun (z : ℂ) ↦ expR (B * expR (c * |u z|))
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖
rcases :
  ∀ (cf : ℝ) (hcf : cf < a) (Bf : ℝ) (hOf : IsBigO (F := ℝ) l f fun (z : ℂ) ↦ expR (Bf * expR (cf * |u z|))),
    ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) l (f - g) fun (z : ℂ) ↦ expR (B * expR (c * |u z|))
⊢ ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) l (f - g) fun (z : ℂ) ↦ expR (B * expR (c * |u z|))

Tactic:
rcases hBf with ⟨cf, hcf, Bf, hOf⟩
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
hBg : ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) l g fun (z : ℂ) ↦ expR (B * expR (c * |u z|))
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : IsBigO (F := ℝ) l f fun (z : ℂ) ↦ expR (Bf * expR (cf * |u z|))
rcases :
  ∀ (cg : ℝ) (hcg : cg < a) (Bg : ℝ) (hOg : IsBigO (F := ℝ) l g fun (z : ℂ) ↦ expR (Bg * expR (cg * |u z|))),
    ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) l (f - g) fun (z : ℂ) ↦ expR (B * expR (c * |u z|))
⊢ ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) l (f - g) fun (z : ℂ) ↦ expR (B * expR (c * |u z|))

Tactic:
rcases hBg with ⟨cg, hcg, Bg, hOg⟩
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : IsBigO (F := ℝ) l f fun (z : ℂ) ↦ expR (Bf * expR (cf * |u z|))
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : IsBigO (F := ℝ) l g fun (z : ℂ) ↦ expR (Bg * expR (cg * |u z|))
⊢ ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) l (f - g) fun (z : ℂ) ↦ expR (B * expR (c * |u z|))

Tactic:
⟨max cf cg, max_lt hcf hcg, max 0 (max Bf Bg), ?_⟩

Premises used: max_lt, Max.max, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : IsBigO (F := ℝ) l f fun (z : ℂ) ↦ expR (Bf * expR (cf * |u z|))
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : IsBigO (F := ℝ) l g fun (z : ℂ) ↦ expR (Bg * expR (cg * |u z|))
refine : IsBigO (F := ℝ) l (f - g) fun (z : ℂ) ↦ expR (max 0 (max Bf Bg) * expR (max cf cg * |u z|))
⊢ ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) l (f - g) fun (z : ℂ) ↦ expR (B * expR (c * |u z|))

Tactic:
refine ⟨max cf cg, max_lt hcf hcg, max 0 (max Bf Bg), ?_⟩
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : IsBigO (F := ℝ) l f fun (z : ℂ) ↦ expR (Bf * expR (cf * |u z|))
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : IsBigO (F := ℝ) l g fun (z : ℂ) ↦ expR (Bg * expR (cg * |u z|))
⊢ IsBigO (F := ℝ) l (f - g) fun (z : ℂ) ↦ expR (max 0 (max Bf Bg) * expR (max cf cg * |u z|))

Tactic:
(hOf.trans_le <| this ?_ ?_ ?_).sub (hOg.trans_le <| this ?_ ?_ ?_)

Premises used: Asymptotics.IsBigO.sub, Asymptotics.IsBigO.trans_le
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : IsBigO (F := ℝ) l f fun (z : ℂ) ↦ expR (Bf * expR (cf * |u z|))
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : IsBigO (F := ℝ) l g fun (z : ℂ) ↦ expR (Bg * expR (cg * |u z|))
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)
refine_6 : Bg ≤ max 0 (max Bf Bg)
⊢ IsBigO (F := ℝ) l (f - g) fun (z : ℂ) ↦ expR (max 0 (max Bf Bg) * expR (max cf cg * |u z|))

Tactic:
refine (hOf.trans_le <| this ?_ ?_ ?_).sub (hOg.trans_le <| this ?_ ?_ ?_)

Premises used: Asymptotics.IsBigO.sub, Asymptotics.IsBigO.trans_le
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : IsBigO (F := ℝ) l f fun (z : ℂ) ↦ expR (Bf * expR (cf * |u z|))
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : IsBigO (F := ℝ) l g fun (z : ℂ) ↦ expR (Bg * expR (cg * |u z|))
⊢ cf ≤ max cf cg

Tactic:
le_max_left _ _

Premises used: le_max_left
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : IsBigO (F := ℝ) l f fun (z : ℂ) ↦ expR (Bf * expR (cf * |u z|))
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : IsBigO (F := ℝ) l g fun (z : ℂ) ↦ expR (Bg * expR (cg * |u z|))
⊢ 0 ≤ max 0 (max Bf Bg)

Tactic:
le_max_left _ _

Premises used: le_max_left
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : IsBigO (F := ℝ) l f fun (z : ℂ) ↦ expR (Bf * expR (cf * |u z|))
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : IsBigO (F := ℝ) l g fun (z : ℂ) ↦ expR (Bg * expR (cg * |u z|))
⊢ Bf ≤ max 0 (max Bf Bg)

Tactic:
(le_max_left _ _).trans (le_max_right _ _)

Premises used: le_max_right, LE.le.trans, le_max_left
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : IsBigO (F := ℝ) l f fun (z : ℂ) ↦ expR (Bf * expR (cf * |u z|))
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : IsBigO (F := ℝ) l g fun (z : ℂ) ↦ expR (Bg * expR (cg * |u z|))
⊢ cg ≤ max cf cg

Tactic:
le_max_right _ _

Premises used: le_max_right
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : IsBigO (F := ℝ) l f fun (z : ℂ) ↦ expR (Bf * expR (cf * |u z|))
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : IsBigO (F := ℝ) l g fun (z : ℂ) ↦ expR (Bg * expR (cg * |u z|))
⊢ Bg ≤ max 0 (max Bf Bg)

Tactic:
(le_max_right _ _).trans (le_max_right _ _)

Premises used: le_max_right, LE.le.trans
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : IsBigO (F := ℝ) l f fun (z : ℂ) ↦ expR (Bf * expR (cf * |u z|))
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : IsBigO (F := ℝ) l g fun (z : ℂ) ↦ expR (Bg * expR (cg * |u z|))
⊢ cf ≤ max cf cg

Tactic:
exacts [le_max_left _ _, le_max_left _ _, (le_max_left _ _).trans (le_max_right _ _),
    le_max_right _ _, le_max_left _ _, (le_max_right _ _).trans (le_max_right _ _)]

Premises used: le_max_right, LE.le.trans, le_max_left
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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₁ c₂ B₁ B₂ : ℝ
hc : c₁ ≤ c₂
hB₀ : 0 ≤ B₂
hB : B₁ ≤ B₂
h : ∀ (z : ℂ) (hz : 1 ≤ ‖z‖), ‖expR (B₁ * ‖z‖ ^ c₁)‖ ≤ expR (B₂ * ‖z‖ ^ c₂)
⊢ (cobounded ℂ ⊓ l).EventuallyLE (β := ℝ) (fun (x : ℂ) ↦ ‖expR (B₁ * ‖x‖ ^ c₁)‖) fun (z : ℂ) ↦ expR (B₂ * ‖z‖ ^ c₂)

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
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₁ c₂ B₁ B₂ : ℝ
hc : c₁ ≤ c₂
hB₀ : 0 ≤ B₂
hB : B₁ ≤ B₂
z : ℂ
hz : 1 ≤ ‖z‖
h : expR (B₁ * ‖z‖ ^ c₁) ≤ expR (B₂ * ‖z‖ ^ c₂)
⊢ ‖expR (B₁ * ‖z‖ ^ c₁)‖ ≤ expR (B₂ * ‖z‖ ^ c₂)

Tactic:
simp only [Real.norm_eq_abs, Real.abs_exp]

Premises used: Real.norm_eq_abs, Real.abs_exp
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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₁ c₂ B₁ B₂ : ℝ
hc : c₁ ≤ c₂
hB₀ : 0 ≤ B₂
hB : B₁ ≤ B₂
z : ℂ
hz : 1 ≤ ‖z‖
h : 0 ≤ ‖z‖ ^ c₁
h₁ : 0 ≤ B₂
h₂ : 1 ≤ ‖z‖
⊢ expR (B₁ * ‖z‖ ^ c₁) ≤ expR (B₂ * ‖z‖ ^ c₂)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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₁ 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
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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₂)
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)
⊢ ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ l) (f - g) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)

Tactic:
rcases hBf with ⟨cf, hcf, Bf, hOf⟩
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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)
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)
⊢ ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ l) (f - g) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)

Tactic:
rcases hBg with ⟨cg, hcg, Bg, hOg⟩
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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)

Tactic:
⟨max cf cg, max_lt hcf hcg, max 0 (max Bf Bg), ?_⟩

Premises used: max_lt, Max.max, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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 : IsBigO (F := ℝ) (cobounded ℂ ⊓ l) (f - g) fun (z : ℂ) ↦ expR (max 0 (max Bf Bg) * ‖z‖ ^ max cf cg)
⊢ ∃ c < a, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ l) (f - g) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)

Tactic:
refine ⟨max cf cg, max_lt hcf hcg, max 0 (max Bf Bg), ?_⟩
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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)

Tactic:
(hOf.trans <| this ?_ ?_ ?_).sub (hOg.trans <| this ?_ ?_ ?_)

Premises used: Asymptotics.IsBigO.sub, Asymptotics.IsBigO.trans
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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)
refine_6 : Bg ≤ max 0 (max Bf Bg)
⊢ IsBigO (F := ℝ) (cobounded ℂ ⊓ l) (f - g) fun (z : ℂ) ↦ expR (max 0 (max Bf Bg) * ‖z‖ ^ max cf cg)

Tactic:
refine (hOf.trans <| this ?_ ?_ ?_).sub (hOg.trans <| this ?_ ?_ ?_)

Premises used: Asymptotics.IsBigO.sub, Asymptotics.IsBigO.trans
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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)
⊢ cf ≤ max cf cg

Tactic:
le_max_left _ _

Premises used: le_max_left
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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)
⊢ 0 ≤ max 0 (max Bf Bg)

Tactic:
le_max_left _ _

Premises used: le_max_left