awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
c : ℝ
f : α → E
g : α → F
s : Set α
⊢ IsBigOWith c (𝓟 s) f g ↔ ∀ x ∈ s, ‖f x‖ ≤ c * ‖g x‖
have rw : (∀ᶠ (x : α) in 𝓟 s, ‖f x‖ ≤ c * ‖g x‖) ↔ ∀ x ∈ s, ‖f x‖ ≤ c * ‖g x‖
Tactic: rw [IsBigOWith_def, eventually_principal]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
c : ℝ
f : α → E
g : α → F
s : Set α
rw : (∀ᶠ (x : α) in 𝓟 s, ‖f x‖ ≤ c * ‖g x‖) ↔ ∀ x ∈ s, ‖f x‖ ≤ c * ‖g x‖
⊢ IsBigOWith c (𝓟 s) f g ↔ ∀ x ∈ s, ‖f x‖ ≤ c * ‖g x‖
have rw₁ : (∀ x ∈ s, ‖f x‖ ≤ c * ‖g x‖) ↔ ∀ x ∈ s, ‖f x‖ ≤ c * ‖g x‖
Tactic: rw [IsBigOWith_def, eventually_principal]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
s : Set α
⊢ f =O[𝓟 s] g ↔ ∃ (c : ℝ), ∀ x ∈ s, ‖f x‖ ≤ c * ‖g x‖
have simp_rw : (∃ (c : ℝ), ∀ᶠ (x : α) in 𝓟 s, ‖f x‖ ≤ c * ‖g x‖) ↔ ∃ (c : ℝ), ∀ x ∈ s, ‖f x‖ ≤ c * ‖g x‖
Tactic: simp_rw [isBigO_iff, eventually_principal]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst : SeminormedAddCommGroup F'
inst_1 : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
⊢ f'' =o[𝓟 s] g' ↔ ∀ x ∈ s, f'' x = 0
have refine_1 : ∀ (h : f'' =o[𝓟 s] g') (x : α) (hx : x ∈ s), ‖f'' x‖ ≤ 0
Tactic: refine ⟨fun h x hx ↦ norm_le_zero_iff.1 ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst : SeminormedAddCommGroup F'
inst_1 : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
refine_1 : ∀ (h : f'' =o[𝓟 s] g') (x : α) (hx : x ∈ s), ‖f'' x‖ ≤ 0
⊢ f'' =o[𝓟 s] g' ↔ ∀ x ∈ s, f'' x = 0
have refine_2 : ∀ (h : ∀ x ∈ s, f'' x = 0), f'' =o[𝓟 s] g'
Tactic: refine ⟨fun h x hx ↦ norm_le_zero_iff.1 ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (hypothesis)
Goal:
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst : SeminormedAddCommGroup F'
inst_1 : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
h : f'' =o[𝓟 s] g'
x : α
hx : x ∈ s
⊢ ‖f'' x‖ ≤ 0
have h₁ : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in 𝓟 s, ‖f'' x‖ ≤ c * ‖g' x‖
Tactic: simp only [isLittleO_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (hypothesis)
Goal:
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst : SeminormedAddCommGroup F'
inst_1 : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
x : α
hx : x ∈ s
h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in 𝓟 s, ‖f'' x‖ ≤ c * ‖g' x‖
⊢ ‖f'' x‖ ≤ 0
have this : Tendsto (β := ℝ) (fun (c : ℝ) ↦ c * ‖g' x‖) (𝓝[>] 0) (𝓝 0)
Tactic: have : Tendsto (fun c : ℝ => c * ‖g' x‖) (𝓝[>] 0) (𝓝 0) :=
      ((continuous_id.mul continuous_const).tendsto' _ _ (zero_mul _)).mono_left
        inf_le_left
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst : SeminormedAddCommGroup F'
inst_1 : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
x : α
hx : x ∈ s
h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in 𝓟 s, ‖f'' x‖ ≤ c * ‖g' x‖
this : Tendsto (β := ℝ) (fun (c : ℝ) ↦ c * ‖g' x‖) (𝓝[>] 0) (𝓝 0)
⊢ ‖f'' x‖ ≤ 0
have refine_1 : EventuallyLE (β := ℝ) (𝓝[>] 0) (fun (x_1 : ℝ) ↦ ‖f'' x‖) fun (c : ℝ) ↦ c * ‖g' x‖
Tactic: apply le_of_tendsto_of_tendsto tendsto_const_nhds this
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst : SeminormedAddCommGroup F'
inst_1 : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
x : α
hx : x ∈ s
h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in 𝓟 s, ‖f'' x‖ ≤ c * ‖g' x‖
this : Tendsto (β := ℝ) (fun (c : ℝ) ↦ c * ‖g' x‖) (𝓝[>] 0) (𝓝 0)
⊢ EventuallyLE (β := ℝ) (𝓝[>] 0) (fun (x_1 : ℝ) ↦ ‖f'' x‖) fun (c : ℝ) ↦ c * ‖g' x‖
have apply : ∀ (c : ℝ) (hc : Membership.mem (γ := Set ℝ) (Ioi 0) c),
  LE.le (α := ℝ) ((fun (x_1 : ℝ) ↦ ‖f'' x‖) c) ((fun (c : ℝ) ↦ c * ‖g' x‖) c)
Tactic: apply eventually_nhdsWithin_iff.2 (Eventually.of_forall (fun c hc ↦ ?_))
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst : SeminormedAddCommGroup F'
inst_1 : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
h : ∀ x ∈ s, f'' x = 0
⊢ f'' =o[𝓟 s] g'
have apply : (fun (_x : α) ↦ 0) =ᶠ[𝓟 s] f''
Tactic: apply (isLittleO_zero g' _).congr' ?_ EventuallyEq.rfl
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
c : ℝ
f : α → E
g : α → F
⊢ IsBigOWith c ⊤ f g ↔ ∀ (x : α), ‖f x‖ ≤ c * ‖g x‖
have rw : (∀ᶠ (x : α) in ⊤, ‖f x‖ ≤ c * ‖g x‖) ↔ ∀ (x : α), ‖f x‖ ≤ c * ‖g x‖
Tactic: rw [IsBigOWith_def, eventually_top]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
c : ℝ
f : α → E
g : α → F
rw : (∀ᶠ (x : α) in ⊤, ‖f x‖ ≤ c * ‖g x‖) ↔ ∀ (x : α), ‖f x‖ ≤ c * ‖g x‖
⊢ IsBigOWith c ⊤ f g ↔ ∀ (x : α), ‖f x‖ ≤ c * ‖g x‖
have rw₁ : (∀ (x : α), ‖f x‖ ≤ c * ‖g x‖) ↔ ∀ (x : α), ‖f x‖ ≤ c * ‖g x‖
Tactic: rw [IsBigOWith_def, eventually_top]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
⊢ f =O[⊤] g ↔ ∃ (C : ℝ), ∀ (x : α), ‖f x‖ ≤ C * ‖g x‖
have simp_rw : (∃ (c : ℝ), ∀ᶠ (x : α) in ⊤, ‖f x‖ ≤ c * ‖g x‖) ↔ ∃ (C : ℝ), ∀ (x : α), ‖f x‖ ≤ C * ‖g x‖
Tactic: simp_rw [isBigO_iff, eventually_top]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
inst_2 : One F
inst_3 : NormOneClass F
inst_4 : TopologicalSpace α
a : α
⊢ (IsBigO.{u_1, u_3, u_4} (F := F) (𝓝[≠] a) f fun (x : α) ↦ 1) ↔ IsBigO.{u_1, u_3, u_4} (F := F) (𝓝 a) f fun (x : α) ↦ 1
have refine : ∀ (h : IsBigO.{u_1, u_3, u_4} (F := F) (𝓝[≠] a) f fun (x : α) ↦ 1),
  IsBigO.{u_1, u_3, u_4} (F := F) (𝓝 a) f fun (x : α) ↦ 1
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ h.mono nhdsWithin_le_nhds⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
inst_2 : One F
inst_3 : NormOneClass F
inst_4 : TopologicalSpace α
a : α
h : IsBigO.{u_1, u_3, u_4} (F := F) (𝓝[≠] a) f fun (x : α) ↦ 1
⊢ IsBigO.{u_1, u_3, u_4} (F := F) (𝓝 a) f fun (x : α) ↦ 1
have simp : ∀ (h : ∃ (b : ℝ), ∀ᶠ (a : α) in 𝓝[≠] a, ‖f a‖ ≤ b), ∃ (b : ℝ), ∀ᶠ (a : α) in 𝓝 a, ‖f a‖ ≤ b
Tactic: simp only [isBigO_one_iff, IsBoundedUnder, IsBounded, eventually_map] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
inst_2 : One F
inst_3 : NormOneClass F
inst_4 : TopologicalSpace α
a : α
h : ∃ (b : ℝ), ∀ᶠ (a : α) in 𝓝[≠] a, ‖f a‖ ≤ b
⊢ ∃ (b : ℝ), ∀ᶠ (a : α) in 𝓝 a, ‖f a‖ ≤ b
have obtain : ∀ (c : ℝ) (hc : ∀ᶠ (a : α) in 𝓝[≠] a, ‖f a‖ ≤ c), ∃ (b : ℝ), ∀ᶠ (a : α) in 𝓝 a, ‖f a‖ ≤ b
Tactic: obtain ⟨c, hc⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
inst_2 : One F
inst_3 : NormOneClass F
inst_4 : TopologicalSpace α
a : α
c : ℝ
hc : ∀ᶠ (a : α) in 𝓝[≠] a, ‖f a‖ ≤ c
⊢ ∃ (b : ℝ), ∀ᶠ (a : α) in 𝓝 a, ‖f a‖ ≤ b
have h : ∀ᶠ (a_1 : α) in 𝓝 a, ‖f a_1‖ ≤ max c ‖f a‖
Tactic: use max c ‖f a‖
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
inst_2 : One F
inst_3 : NormOneClass F
inst_4 : TopologicalSpace α
a : α
c : ℝ
hc : ∀ᶠ (a : α) in 𝓝[≠] a, ‖f a‖ ≤ c
⊢ ∀ᶠ (a_1 : α) in 𝓝 a, ‖f a_1‖ ≤ max c ‖f a‖
have h : ∀ (b : α) (hb : Membership.mem (γ := Set α) {a}ᶜ b → ‖f b‖ ≤ c), ‖f b‖ ≤ max c ‖f a‖
Tactic: filter_upwards [eventually_nhdsWithin_iff.mp hc] with b hb
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
inst_2 : One F
inst_3 : NormOneClass F
inst_4 : TopologicalSpace α
a : α
c : ℝ
hc : ∀ᶠ (a : α) in 𝓝[≠] a, ‖f a‖ ≤ c
b : α
hb : Membership.mem (γ := Set α) {a}ᶜ b → ‖f b‖ ≤ c
⊢ ‖f b‖ ≤ max c ‖f a‖
have h : ∀ (hc : ∀ᶠ (a : α) in 𝓝[≠] b, ‖f a‖ ≤ c) (hb : Membership.mem (γ := Set α) {b}ᶜ b → ‖f b‖ ≤ c), ‖f b‖ ≤ max c ‖f b‖
Tactic: rcases eq_or_ne b a with rfl | hb'
Cleared hypotheses: a, hc, hb
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
inst_2 : One F
inst_3 : NormOneClass F
inst_4 : TopologicalSpace α
a : α
c : ℝ
hc : ∀ᶠ (a : α) in 𝓝[≠] a, ‖f a‖ ≤ c
b : α
hb : Membership.mem (γ := Set α) {a}ᶜ b → ‖f b‖ ≤ c
h : ∀ (hc : ∀ᶠ (a : α) in 𝓝[≠] b, ‖f a‖ ≤ c) (hb : Membership.mem (γ := Set α) {b}ᶜ b → ‖f b‖ ≤ c), ‖f b‖ ≤ max c ‖f b‖
⊢ ‖f b‖ ≤ max c ‖f a‖
have h₁ : ∀ (hb' : b ≠ a), ‖f b‖ ≤ max c ‖f a‖
Tactic: rcases eq_or_ne b a with rfl | hb'
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
f'' : α → E''
l : Filter α
c : F''
⊢ (IsBigO.{u_1, u_9, u_10} (F := F'') l f'' fun (_x : α) ↦ c) ↔
    (c = 0 → f'' =ᶠ[l] 0) ∧ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖f'' x‖
have refine : ((c = 0 → f'' =ᶠ[l] 0) ∧ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖f'' x‖) →
  IsBigO.{u_1, u_9, u_10} (F := F'') l f'' fun (_x : α) ↦ c
Tactic: refine ⟨fun h => ⟨fun hc => isBigO_zero_right_iff.1 (by rwa [← hc]), h.isBoundedUnder_le⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
f'' : α → E''
l : Filter α
c : F''
hcf : c = 0 → f'' =ᶠ[l] 0
hf : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖f'' x‖
⊢ IsBigO.{u_1, u_9, u_10} (F := F'') l f'' fun (_x : α) ↦ c
have inl : ∀ (hc : c = 0), IsBigO.{u_1, u_9, u_10} (F := F'') l f'' fun (_x : α) ↦ c
Tactic: rcases eq_or_ne c 0 with (hc | hc)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
f'' : α → E''
l : Filter α
c : F''
hcf : c = 0 → f'' =ᶠ[l] 0
hf : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖f'' x‖
inl : ∀ (hc : c = 0), IsBigO.{u_1, u_9, u_10} (F := F'') l f'' fun (_x : α) ↦ c
⊢ IsBigO.{u_1, u_9, u_10} (F := F'') l f'' fun (_x : α) ↦ c
have inr : ∀ (hc : c ≠ 0), IsBigO.{u_1, u_9, u_10} (F := F'') l f'' fun (_x : α) ↦ c
Tactic: rcases eq_or_ne c 0 with (hc | hc)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
E : Type u_3
F'' : Type u_10
inst : Norm E
inst_1 : NormedAddCommGroup F''
f : α → E
g'' : α → F''
l : Filter α
h : ∀ᶠ (x : α) in l, g'' x ≠ 0
⊢ f =O[l] g'' ↔ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖f x‖ / ‖g'' x‖
have simp : (∃ (c : ℝ), ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g'' x‖) ↔ ∃ (b : ℝ), ∀ᶠ (a : α) in l, ‖f a‖ / ‖g'' a‖ ≤ b
Tactic: simp only [isBigO_iff, IsBoundedUnder, IsBounded, eventually_map]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
E' : Type u_6
E'' : Type u_9
inst : SeminormedAddCommGroup E'
inst_1 : NormedAddCommGroup E''
f' : α → E'
l : Filter α
c : E''
hc : c ≠ 0
⊢ IsBigO.{u_1, u_9, u_6} (E := E'') l (fun (_x : α) ↦ c) f' ↔ ∃ (b : ℝ), 0 < b ∧ ∀ᶠ (x : α) in l, b ≤ ‖f' x‖
have mp : IsBigO.{u_1, u_9, u_6} (E := E'') l (fun (_x : α) ↦ c) f' → ∃ (b : ℝ), 0 < b ∧ ∀ᶠ (x : α) in l, b ≤ ‖f' x‖
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
E' : Type u_6
E'' : Type u_9
inst : SeminormedAddCommGroup E'
inst_1 : NormedAddCommGroup E''
f' : α → E'
l : Filter α
c : E''
hc : c ≠ 0
mp : IsBigO.{u_1, u_9, u_6} (E := E'') l (fun (_x : α) ↦ c) f' → ∃ (b : ℝ), 0 < b ∧ ∀ᶠ (x : α) in l, b ≤ ‖f' x‖
⊢ IsBigO.{u_1, u_9, u_6} (E := E'') l (fun (_x : α) ↦ c) f' ↔ ∃ (b : ℝ), 0 < b ∧ ∀ᶠ (x : α) in l, b ≤ ‖f' x‖
have mpr : (∃ (b : ℝ), 0 < b ∧ ∀ᶠ (x : α) in l, b ≤ ‖f' x‖) → IsBigO.{u_1, u_9, u_6} (E := E'') l (fun (_x : α) ↦ c) f'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
E' : Type u_6
E'' : Type u_9
inst : SeminormedAddCommGroup E'
inst_1 : NormedAddCommGroup E''
f' : α → E'
l : Filter α
c : E''
hc : c ≠ 0
h : IsBigO.{u_1, u_9, u_6} (E := E'') l (fun (_x : α) ↦ c) f'
⊢ ∃ (b : ℝ), 0 < b ∧ ∀ᶠ (x : α) in l, b ≤ ‖f' x‖
have mp : ∀ (C : ℝ) (hC₀ : C > 0) (hC : IsBigOWith.{u_1, u_9, u_6} (E := E'') C l (fun (_x : α) ↦ c) f'),
  ∃ (b : ℝ), 0 < b ∧ ∀ᶠ (x : α) in l, b ≤ ‖f' x‖
Tactic: rcases h.exists_pos with ⟨C, hC₀, hC⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
E' : Type u_6
E'' : Type u_9
inst : SeminormedAddCommGroup E'
inst_1 : NormedAddCommGroup E''
f' : α → E'
l : Filter α
c : E''
hc : c ≠ 0
h : IsBigO.{u_1, u_9, u_6} (E := E'') l (fun (_x : α) ↦ c) f'
C : ℝ
hC₀ : C > 0
hC : IsBigOWith.{u_1, u_9, u_6} (E := E'') C l (fun (_x : α) ↦ c) f'
⊢ ∃ (b : ℝ), 0 < b ∧ ∀ᶠ (x : α) in l, b ≤ ‖f' x‖
have mp : ∀ᶠ (x : α) in l, ‖c‖ / C ≤ ‖f' x‖
Tactic: refine ⟨‖c‖ / C, div_pos (norm_pos_iff.2 hc) hC₀, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
E' : Type u_6
E'' : Type u_9
inst : SeminormedAddCommGroup E'
inst_1 : NormedAddCommGroup E''
f' : α → E'
l : Filter α
c : E''
hc : c ≠ 0
b : ℝ
hb₀ : 0 < b
hb : ∀ᶠ (x : α) in l, b ≤ ‖f' x‖
⊢ IsBigO.{u_1, u_9, u_6} (E := E'') l (fun (_x : α) ↦ c) f'
have mpr : ∀ (x : α) (hx : b ≤ ‖f' x‖), ‖c‖ ≤ ‖c‖ / b * ‖f' x‖
Tactic: refine IsBigO.of_bound (‖c‖ / b) (hb.mono fun x hx => ?_)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
E' : Type u_6
E'' : Type u_9
inst : SeminormedAddCommGroup E'
inst_1 : NormedAddCommGroup E''
f' : α → E'
l : Filter α
c : E''
hc : c ≠ 0
b : ℝ
hb₀ : 0 < b
hb : ∀ᶠ (x : α) in l, b ≤ ‖f' x‖
x : α
hx : b ≤ ‖f' x‖
⊢ ‖c‖ ≤ ‖c‖ / b * ‖f' x‖
have mpr : ‖c‖ ≤ ‖c‖ * (‖f' x‖ / b)
Tactic: rw [div_mul_eq_mul_div, mul_div_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst : SeminormedRing R
inst_1 : NormedDivisionRing 𝕜
l : Filter α
f : α → 𝕜
g : α → R
n : ℕ
hn : n ≠ 0
h : (f ^ n) =O[l] (g ^ n)
⊢ f =O[l] g
have rcases : ∀ (C : ℝ) (_hC₀ : C > 0) (hC : IsBigOWith C l (f ^ n) (g ^ n)), f =O[l] g
Tactic: rcases h.exists_pos with ⟨C, _hC₀, hC⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst : SeminormedRing R
inst_1 : NormedDivisionRing 𝕜
l : Filter α
f : α → 𝕜
g : α → R
n : ℕ
hn : n ≠ 0
h : (f ^ n) =O[l] (g ^ n)
C : ℝ
_hC₀ : C > 0
hC : IsBigOWith C l (f ^ n) (g ^ n)
⊢ f =O[l] g
have obtain : ∀ (c : ℝ) (hc₀ : 0 ≤ c) (hc : C ≤ c ^ n), f =O[l] g
Tactic: obtain ⟨c : ℝ, hc₀ : 0 ≤ c, hc : C ≤ c ^ n⟩ :=
    ((eventually_ge_atTop _).and <| (tendsto_pow_atTop hn).eventually_ge_atTop C).exists
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
l : Filter α
f : α → ℝ
hf : 1 ≤ᶠ[l] f
m n : ℕ
h : n ≤ m
⊢ (f ^ n) =O[l] (f ^ m)
have rw : ∃ (c : ℝ), IsBigOWith c l (f ^ n) (f ^ m)
Tactic: rw [IsBigO_def]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
l : Filter α
f : α → ℝ
hf : 1 ≤ᶠ[l] f
m n : ℕ
h : n ≤ m
⊢ ∃ (c : ℝ), IsBigOWith c l (f ^ n) (f ^ m)
have refine : IsBigOWith 1 l (f ^ n) (f ^ m)
Tactic: refine ⟨1, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
l : Filter α
f : α → ℝ
hf : 1 ≤ᶠ[l] f
m n : ℕ
h : n ≤ m
⊢ IsBigOWith 1 l (f ^ n) (f ^ m)
have rw : ∀ᶠ (x : α) in l, ‖(f ^ n) x‖ ≤ 1 * ‖(f ^ m) x‖
Tactic: rw [IsBigOWith_def]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (hypothesis)
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
𝕜 : Type u_15
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
inst_2 : NormedDivisionRing 𝕜
g : α → F
f' : α → E'
l : Filter α
inst_3 : Module 𝕜 E'
inst_4 : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
⊢ IsBigO.{u_1, u_6, u_4} (E := E') l (fun (x : α) ↦ c • f' x) g ↔ f' =O[l] g
have cne0 : ‖c‖ ≠ 0
Tactic: have cne0 : ‖c‖ ≠ 0 := norm_ne_zero_iff.mpr hc
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
𝕜 : Type u_15
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
inst_2 : NormedDivisionRing 𝕜
g : α → F
f' : α → E'
l : Filter α
inst_3 : Module 𝕜 E'
inst_4 : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ IsBigO.{u_1, u_6, u_4} (E := E') l (fun (x : α) ↦ c • f' x) g ↔ f' =O[l] g
have rw : IsBigO (E := ℝ) l (fun (x : α) ↦ ‖c • f' x‖) g ↔ f' =O[l] g
Tactic: rw [← isBigO_norm_left]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
𝕜 : Type u_15
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
inst_2 : NormedDivisionRing 𝕜
g : α → F
f' : α → E'
l : Filter α
inst_3 : Module 𝕜 E'
inst_4 : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ IsBigO (E := ℝ) l (fun (x : α) ↦ ‖c • f' x‖) g ↔ f' =O[l] g
have simp : IsBigO (E := ℝ) l (fun (x : α) ↦ ‖c‖ * ‖f' x‖) g ↔ f' =O[l] g
Tactic: simp only [norm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
𝕜 : Type u_15
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
inst_2 : NormedDivisionRing 𝕜
g : α → F
f' : α → E'
l : Filter α
inst_3 : Module 𝕜 E'
inst_4 : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ IsBigO (E := ℝ) l (fun (x : α) ↦ ‖c‖ * ‖f' x‖) g ↔ f' =O[l] g
have rw : IsBigO (E := ℝ) l (fun (x : α) ↦ ‖f' x‖) g ↔ f' =O[l] g
Tactic: rw [isBigO_const_mul_left_iff cne0, isBigO_norm_left]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
𝕜 : Type u_15
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
inst_2 : NormedDivisionRing 𝕜
g : α → F
f' : α → E'
l : Filter α
inst_3 : Module 𝕜 E'
inst_4 : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
rw : IsBigO (E := ℝ) l (fun (x : α) ↦ ‖f' x‖) g ↔ f' =O[l] g
⊢ IsBigO (E := ℝ) l (fun (x : α) ↦ ‖c‖ * ‖f' x‖) g ↔ f' =O[l] g
have rw₁ : f' =O[l] g ↔ f' =O[l] g
Tactic: rw [isBigO_const_mul_left_iff cne0, isBigO_norm_left]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (hypothesis)
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
𝕜 : Type u_15
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
inst_2 : NormedDivisionRing 𝕜
g : α → F
f' : α → E'
l : Filter α
inst_3 : Module 𝕜 E'
inst_4 : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
⊢ IsLittleO.{u_1, u_6, u_4} (E := E') l (fun (x : α) ↦ c • f' x) g ↔ f' =o[l] g
have cne0 : ‖c‖ ≠ 0
Tactic: have cne0 : ‖c‖ ≠ 0 := norm_ne_zero_iff.mpr hc
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
𝕜 : Type u_15
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
inst_2 : NormedDivisionRing 𝕜
g : α → F
f' : α → E'
l : Filter α
inst_3 : Module 𝕜 E'
inst_4 : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ IsLittleO.{u_1, u_6, u_4} (E := E') l (fun (x : α) ↦ c • f' x) g ↔ f' =o[l] g
have rw : IsLittleO (E := ℝ) l (fun (x : α) ↦ ‖c • f' x‖) g ↔ f' =o[l] g
Tactic: rw [← isLittleO_norm_left]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
𝕜 : Type u_15
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
inst_2 : NormedDivisionRing 𝕜
g : α → F
f' : α → E'
l : Filter α
inst_3 : Module 𝕜 E'
inst_4 : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ IsLittleO (E := ℝ) l (fun (x : α) ↦ ‖c • f' x‖) g ↔ f' =o[l] g
have simp : IsLittleO (E := ℝ) l (fun (x : α) ↦ ‖c‖ * ‖f' x‖) g ↔ f' =o[l] g
Tactic: simp only [norm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
𝕜 : Type u_15
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
inst_2 : NormedDivisionRing 𝕜
g : α → F
f' : α → E'
l : Filter α
inst_3 : Module 𝕜 E'
inst_4 : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ IsLittleO (E := ℝ) l (fun (x : α) ↦ ‖c‖ * ‖f' x‖) g ↔ f' =o[l] g
have rw : IsLittleO (E := ℝ) l (fun (x : α) ↦ ‖f' x‖) g ↔ f' =o[l] g
Tactic: rw [isLittleO_const_mul_left_iff cne0, isLittleO_norm_left]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
𝕜 : Type u_15
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
inst_2 : NormedDivisionRing 𝕜
g : α → F
f' : α → E'
l : Filter α
inst_3 : Module 𝕜 E'
inst_4 : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
rw : IsLittleO (E := ℝ) l (fun (x : α) ↦ ‖f' x‖) g ↔ f' =o[l] g
⊢ IsLittleO (E := ℝ) l (fun (x : α) ↦ ‖c‖ * ‖f' x‖) g ↔ f' =o[l] g
have rw₁ : f' =o[l] g ↔ f' =o[l] g
Tactic: rw [isLittleO_const_mul_left_iff cne0, isLittleO_norm_left]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (hypothesis)
Goal:
α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst : Norm E
inst_1 : SeminormedAddCommGroup E'
inst_2 : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst_3 : Module 𝕜 E'
inst_4 : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
⊢ (IsBigO.{u_1, u_3, u_6} (F := E') l f fun (x : α) ↦ c • f' x) ↔ f =O[l] f'
have cne0 : ‖c‖ ≠ 0
Tactic: have cne0 : ‖c‖ ≠ 0 := norm_ne_zero_iff.mpr hc
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst : Norm E
inst_1 : SeminormedAddCommGroup E'
inst_2 : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst_3 : Module 𝕜 E'
inst_4 : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (IsBigO.{u_1, u_3, u_6} (F := E') l f fun (x : α) ↦ c • f' x) ↔ f =O[l] f'
have rw : (IsBigO (F := ℝ) l f fun (x : α) ↦ ‖c • f' x‖) ↔ f =O[l] f'
Tactic: rw [← isBigO_norm_right]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst : Norm E
inst_1 : SeminormedAddCommGroup E'
inst_2 : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst_3 : Module 𝕜 E'
inst_4 : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (IsBigO (F := ℝ) l f fun (x : α) ↦ ‖c • f' x‖) ↔ f =O[l] f'
have simp : (IsBigO (F := ℝ) l f fun (x : α) ↦ ‖c‖ * ‖f' x‖) ↔ f =O[l] f'
Tactic: simp only [norm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst : Norm E
inst_1 : SeminormedAddCommGroup E'
inst_2 : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst_3 : Module 𝕜 E'
inst_4 : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (IsBigO (F := ℝ) l f fun (x : α) ↦ ‖c‖ * ‖f' x‖) ↔ f =O[l] f'
have rw : (IsBigO (F := ℝ) l f fun (x : α) ↦ ‖f' x‖) ↔ f =O[l] f'
Tactic: rw [isBigO_const_mul_right_iff cne0, isBigO_norm_right]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (goal)
Goal:
α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst : Norm E
inst_1 : SeminormedAddCommGroup E'
inst_2 : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst_3 : Module 𝕜 E'
inst_4 : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
rw : (IsBigO (F := ℝ) l f fun (x : α) ↦ ‖f' x‖) ↔ f =O[l] f'
⊢ (IsBigO (F := ℝ) l f fun (x : α) ↦ ‖c‖ * ‖f' x‖) ↔ f =O[l] f'
have rw₁ : f =O[l] f' ↔ f =O[l] f'
Tactic: rw [isBigO_const_mul_right_iff cne0, isBigO_norm_right]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Lemmas (hypothesis)
Goal:
α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst : Norm E
inst_1 : SeminormedAddCommGroup E'
inst_2 : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst_3 : Module 𝕜 E'
inst_4 : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
⊢ (IsLittleO.{u_1, u_3, u_6} (F := E') l f fun (x : α) ↦ c • f' x) ↔ f =o[l] f'
have cne0 : ‖c‖ ≠ 0
Tactic: have cne0 : ‖c‖ ≠ 0 := norm_ne_zero_iff.mpr hc