awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
s_1 : Finset ι
B : ι → α → ℝ
i : ι
s : Finset ι
his : i ∉ s
h :
  ∀ (hAB : ∀ i ∈ s, A i =o[l] B i),
    IsLittleO.{u_1, u_6, 0} (E := E') (F := ℝ) l (fun (H : α) ↦ ∑ i ∈ s, A i H) fun (H : α) ↦ ∑ i ∈ s, ‖B i H‖
hAB : ∀ i_1 ∈ Finset.cons i s his, A i_1 =o[l] B i_1
⊢ l.EventuallyEq (β := ℝ) (fun (H : α) ↦ ‖B i H‖ + norm (E := ℝ) (∑ j ∈ s, ‖B j H‖)) fun (H : α) ↦
    ‖B i H‖ + ∑ j ∈ s, ‖B j H‖
have refine : ∀ (H : α), norm (E := ℝ) (∑ j ∈ s, ‖B j H‖) = ∑ j ∈ s, ‖B j H‖
Tactic: refine Eventually.of_forall fun H ↦ congr_arg (‖B i H‖ + ·) ?_
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
s_1 : Finset ι
B : ι → α → ℝ
i : ι
s : Finset ι
his : i ∉ s
h :
  ∀ (hAB : ∀ i ∈ s, A i =o[l] B i),
    IsLittleO.{u_1, u_6, 0} (E := E') (F := ℝ) l (fun (H : α) ↦ ∑ i ∈ s, A i H) fun (H : α) ↦ ∑ i ∈ s, ‖B i H‖
hAB : ∀ i_1 ∈ Finset.cons i s his, A i_1 =o[l] B i_1
⊢ IsLittleO.{u_1, u_6, 0} (E := E') (F := ℝ) l (fun (H : α) ↦ A i H + ∑ i ∈ s, A i H) fun (H : α) ↦
    ‖B i H‖ + ∑ i ∈ s, ‖B i H‖
have calc : l.EventuallyEq (β := ℝ) (fun (H : α) ↦ ‖B i H‖ + norm (E := ℝ) (∑ j ∈ s, ‖B j H‖)) fun (H : α) ↦
  ‖B i H‖ + ∑ j ∈ s, ‖B j H‖
Tactic: calc (fun H => A i H + ∑ j ∈ s, A j H)
      =o[l] fun H => ‖B i H‖ + ‖∑ j ∈ s, ‖B j H‖‖ :=
          (hAB i (by simp)).add_add (h (fun j hj => hAB j (by simp [hj])))
    _ =ᶠ[l] fun H => ‖B i H‖ + ∑ j ∈ s, ‖B j H‖ := by
        refine Eventually.of_forall fun H ↦ congr_arg (‖B i H‖ + ·) ?_
        exact Real.norm_of_nonneg (Finset.sum_nonneg fun _ _ => norm_nonneg _)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
s : Finset ι
B : ι → α → ℝ
hAB : ∀ i ∈ s, A i =o[l] B i
⊢ IsLittleO.{u_1, u_6, 0} (E := E') (F := ℝ) l (fun (H : α) ↦ ∑ i ∈ s, A i H) fun (H : α) ↦ ∑ i ∈ s, ‖B i H‖
have empty : ∀ (hAB : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → A i =o[l] B i),
  IsLittleO.{u_1, u_6, 0} (E := E') (F := ℝ) l (fun (H : α) ↦ ∑ i ∈ ∅, A i H) fun (H : α) ↦ ∑ i ∈ ∅, ‖B i H‖
Tactic: induction s using Finset.cons_induction with
  | empty => simp [isLittleO_zero]
  | cons i s his h =>
  simp_rw [Finset.sum_cons]
  calc (fun H => A i H + ∑ j ∈ s, A j H)
      =o[l] fun H => ‖B i H‖ + ‖∑ j ∈ s, ‖B j H‖‖ :=
          (hAB i (by simp)).add_add (h (fun j hj => hAB j (by simp [hj])))
    _ =ᶠ[l] fun H => ‖B i H‖ + ∑ j ∈ s, ‖B j H‖ := by
        refine Eventually.of_forall fun H ↦ congr_arg (‖B i H‖ + ·) ?_
        exact Real.norm_of_nonneg (Finset.sum_nonneg fun _ _ => norm_nonneg _)
Cleared hypotheses: hAB
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
s : Finset ι
B : ι → α → ℝ
hAB : ∀ i ∈ s, A i =o[l] B i
empty :
  ∀ (hAB : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → A i =o[l] B i),
    IsLittleO.{u_1, u_6, 0} (E := E') (F := ℝ) l (fun (H : α) ↦ ∑ i ∈ ∅, A i H) fun (H : α) ↦ ∑ i ∈ ∅, ‖B i H‖
⊢ IsLittleO.{u_1, u_6, 0} (E := E') (F := ℝ) l (fun (H : α) ↦ ∑ i ∈ s, A i H) fun (H : α) ↦ ∑ i ∈ s, ‖B i H‖
have cons : ∀ (i : ι) (s : Finset ι) (his : i ∉ s)
  (h :
    ∀ (hAB : ∀ i ∈ s, A i =o[l] B i),
      IsLittleO.{u_1, u_6, 0} (E := E') (F := ℝ) l (fun (H : α) ↦ ∑ i ∈ s, A i H) fun (H : α) ↦ ∑ i ∈ s, ‖B i H‖)
  (hAB : ∀ i_1 ∈ Finset.cons i s his, A i_1 =o[l] B i_1),
  IsLittleO.{u_1, u_6, 0} (E := E') (F := ℝ) l (fun (H : α) ↦ ∑ i ∈ Finset.cons i s his, A i H) fun (H : α) ↦
    ∑ i ∈ Finset.cons i s his, ‖B i H‖
Tactic: induction s using Finset.cons_induction with
  | empty => simp [isLittleO_zero]
  | cons i s his h =>
  simp_rw [Finset.sum_cons]
  calc (fun H => A i H + ∑ j ∈ s, A j H)
      =o[l] fun H => ‖B i H‖ + ‖∑ j ∈ s, ‖B j H‖‖ :=
          (hAB i (by simp)).add_add (h (fun j hj => hAB j (by simp [hj])))
    _ =ᶠ[l] fun H => ‖B i H‖ + ∑ j ∈ s, ‖B j H‖ := by
        refine Eventually.of_forall fun H ↦ congr_arg (‖B i H‖ + ·) ?_
        exact Real.norm_of_nonneg (Finset.sum_nonneg fun _ _ => norm_nonneg _)
Cleared hypotheses: hAB
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
B : ι → α → ℝ
C : ℝ
i : α → Finset ι
hAB : IsBigOWith C (SProd.sprod (α := Filter ι) ⊤ l) (Function.uncurry A) (Function.uncurry B)
⊢ IsBigOWith.{u_1, u_6, 0} (E := E') (F := ℝ) C l (fun (H : α) ↦ ∑ j ∈ i H, A j H) fun (H : α) ↦ ∑ j ∈ i H, ‖B j H‖
have simp : ∀ (hAB : ∀ᶠ (x : ι × α) in SProd.sprod (α := Filter ι) ⊤ l, ‖Function.uncurry A x‖ ≤ C * ‖Function.uncurry B x‖),
  ∀ᶠ (x : α) in l, norm.{u_6} (E := E') (∑ j ∈ i x, A j x) ≤ C * norm (E := ℝ) (∑ j ∈ i x, ‖B j x‖)
Tactic: simp only [IsBigOWith_def] at *
Cleared hypotheses: hAB
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
B : ι → α → ℝ
C : ℝ
i : α → Finset ι
hAB : ∀ᶠ (x : ι × α) in SProd.sprod (α := Filter ι) ⊤ l, ‖Function.uncurry A x‖ ≤ C * ‖Function.uncurry B x‖
⊢ ∀ᶠ (x : α) in l, norm.{u_6} (E := E') (∑ j ∈ i x, A j x) ≤ C * norm (E := ℝ) (∑ j ∈ i x, ‖B j x‖)
have obtain : ∀ (s₁ : ι → Prop) (hs₁ : ∀ᶠ (x : ι) in ⊤, s₁ x) (s₂ : α → Prop) (hs₂ : ∀ᶠ (y : α) in l, s₂ y)
  (hbound : ∀ {x : ι}, s₁ x → ∀ {y : α}, s₂ y → ‖Function.uncurry A (x, y)‖ ≤ C * ‖Function.uncurry B (x, y)‖),
  ∀ᶠ (x : α) in l, norm.{u_6} (E := E') (∑ j ∈ i x, A j x) ≤ C * norm (E := ℝ) (∑ j ∈ i x, ‖B j x‖)
Tactic: obtain ⟨s₁, hs₁, s₂, hs₂, hbound⟩ := Filter.eventually_prod_iff.mp hAB
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
B : ι → α → ℝ
C : ℝ
i : α → Finset ι
hAB : ∀ᶠ (x : ι × α) in SProd.sprod (α := Filter ι) ⊤ l, ‖Function.uncurry A x‖ ≤ C * ‖Function.uncurry B x‖
s₁ : ι → Prop
hs₁ : ∀ᶠ (x : ι) in ⊤, s₁ x
s₂ : α → Prop
hs₂ : ∀ᶠ (y : α) in l, s₂ y
hbound : ∀ {x : ι}, s₁ x → ∀ {y : α}, s₂ y → ‖Function.uncurry A (x, y)‖ ≤ C * ‖Function.uncurry B (x, y)‖
⊢ ∀ᶠ (x : α) in l, norm.{u_6} (E := E') (∑ j ∈ i x, A j x) ≤ C * norm (E := ℝ) (∑ j ∈ i x, ‖B j x‖)
have h : ∀ (H : α) (hH : s₂ H), norm.{u_6} (E := E') (∑ j ∈ i H, A j H) ≤ C * norm (E := ℝ) (∑ j ∈ i H, ‖B j H‖)
Tactic: filter_upwards [hs₂] with H hH
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
B : ι → α → ℝ
C : ℝ
i : α → Finset ι
hAB : ∀ᶠ (x : ι × α) in SProd.sprod (α := Filter ι) ⊤ l, ‖Function.uncurry A x‖ ≤ C * ‖Function.uncurry B x‖
s₁ : ι → Prop
hs₁ : ∀ᶠ (x : ι) in ⊤, s₁ x
s₂ : α → Prop
hs₂ : ∀ᶠ (y : α) in l, s₂ y
hbound : ∀ {x : ι}, s₁ x → ∀ {y : α}, s₂ y → ‖Function.uncurry A (x, y)‖ ≤ C * ‖Function.uncurry B (x, y)‖
H : α
hH : s₂ H
⊢ C * ∑ j ∈ i H, ‖B j H‖ = C * norm (E := ℝ) (∑ j ∈ i H, ‖B j H‖)
have e_a : ∑ j ∈ i H, ‖B j H‖ = norm (E := ℝ) (∑ j ∈ i H, ‖B j H‖)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
B : ι → α → ℝ
C : ℝ
i : α → Finset ι
hAB : ∀ᶠ (x : ι × α) in SProd.sprod (α := Filter ι) ⊤ l, ‖Function.uncurry A x‖ ≤ C * ‖Function.uncurry B x‖
s₁ : ι → Prop
hs₁ : ∀ᶠ (x : ι) in ⊤, s₁ x
s₂ : α → Prop
hs₂ : ∀ᶠ (y : α) in l, s₂ y
hbound : ∀ {x : ι}, s₁ x → ∀ {y : α}, s₂ y → ‖Function.uncurry A (x, y)‖ ≤ C * ‖Function.uncurry B (x, y)‖
H : α
hH : s₂ H
⊢ ∑ j ∈ i H, ‖B j H‖ = norm (E := ℝ) (∑ j ∈ i H, ‖B j H‖)
have e_a : Eq (α := ℝ) (∑ j ∈ i H, ‖B j H‖) (∑ i ∈ i H, ‖B i H‖)
Tactic: rw [Real.norm_of_nonneg (Finset.sum_nonneg (fun _ _ ↦ norm_nonneg _))]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
B : ι → α → ℝ
C : ℝ
i : α → Finset ι
hAB : ∀ᶠ (x : ι × α) in SProd.sprod (α := Filter ι) ⊤ l, ‖Function.uncurry A x‖ ≤ C * ‖Function.uncurry B x‖
s₁ : ι → Prop
hs₁ : ∀ᶠ (x : ι) in ⊤, s₁ x
s₂ : α → Prop
hs₂ : ∀ᶠ (y : α) in l, s₂ y
hbound : ∀ {x : ι}, s₁ x → ∀ {y : α}, s₂ y → ‖Function.uncurry A (x, y)‖ ≤ C * ‖Function.uncurry B (x, y)‖
H : α
hH : s₂ H
⊢ norm.{u_6} (E := E') (∑ j ∈ i H, A j H) ≤ C * norm (E := ℝ) (∑ j ∈ i H, ‖B j H‖)
have j : C * ∑ j ∈ i H, ‖B j H‖ = C * norm (E := ℝ) (∑ j ∈ i H, ‖B j H‖)
Tactic: calc
    ‖∑ j ∈ i H, A j H‖ ≤ ∑ j ∈ i H, ‖A j H‖ := norm_sum_le ..
    _ ≤ ∑ j ∈ i H, C * ‖B j H‖ :=
        Finset.sum_le_sum fun j _ => hbound (Filter.eventually_top.mp hs₁ j) hH
    _ = C * ∑ j ∈ i H, ‖B j H‖ := (Finset.mul_sum ..).symm
    _ = C * ‖∑ j ∈ i H, ‖B j H‖‖ := by
        congr; rw [Real.norm_of_nonneg (Finset.sum_nonneg (fun _ _ ↦ norm_nonneg _))]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
B : ι → α → ℝ
i : α → Finset ι
hAB : Function.uncurry A =O[SProd.sprod (α := Filter ι) ⊤ l] Function.uncurry B
⊢ IsBigO.{u_1, u_6, 0} (E := E') (F := ℝ) l (fun (H : α) ↦ ∑ j ∈ i H, A j H) fun (H : α) ↦ ∑ j ∈ i H, ‖B j H‖
have simp : ∃ (c : ℝ),
  IsBigOWith.{u_1, u_6, 0} (E := E') (F := ℝ) c l (fun (H : α) ↦ ∑ j ∈ i H, A j H) fun (H : α) ↦ ∑ j ∈ i H, ‖B j H‖
Tactic: simp only [IsBigO_def]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
B : ι → α → ℝ
i : α → Finset ι
hAB : Function.uncurry A =O[SProd.sprod (α := Filter ι) ⊤ l] Function.uncurry B
⊢ ∃ (c : ℝ),
    IsBigOWith.{u_1, u_6, 0} (E := E') (F := ℝ) c l (fun (H : α) ↦ ∑ j ∈ i H, A j H) fun (H : α) ↦ ∑ j ∈ i H, ‖B j H‖
have obtain : ∀ (C : ℝ) (hC : IsBigOWith C (SProd.sprod (α := Filter ι) ⊤ l) (Function.uncurry A) (Function.uncurry B)),
  ∃ (c : ℝ),
    IsBigOWith.{u_1, u_6, 0} (E := E') (F := ℝ) c l (fun (H : α) ↦ ∑ j ∈ i H, A j H) fun (H : α) ↦ ∑ j ∈ i H, ‖B j H‖
Tactic: obtain ⟨C, hC⟩ := hAB.isBigOWith
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
B : ι → α → ℝ
i : α → Finset ι
hAB : Function.uncurry A =o[SProd.sprod (α := Filter ι) ⊤ l] Function.uncurry B
⊢ IsLittleO.{u_1, u_6, 0} (E := E') (F := ℝ) l (fun (H : α) ↦ ∑ j ∈ i H, A j H) fun (H : α) ↦ ∑ j ∈ i H, ‖B j H‖
have rw : ∀ (hAB : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (SProd.sprod (α := Filter ι) ⊤ l) (Function.uncurry A) (Function.uncurry B))
  ⦃c : ℝ⦄,
  0 < c →
    IsBigOWith.{u_1, u_6, 0} (E := E') (F := ℝ) c l (fun (H : α) ↦ ∑ j ∈ i H, A j H) fun (H : α) ↦ ∑ j ∈ i H, ‖B j H‖
Tactic: rw [isLittleO_iff_forall_isBigOWith] at *
Cleared hypotheses: hAB
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
h : ∃ᶠ (n : ℕ) in atTop, u n ≤ v n
n : ℕ
u_v : u n ≤ v n
⊢ (u n).log / (↑n : EReal) ≤ (v n).log / (↑n : EReal)
have h₁ : LE.le (α := EReal) 0 (↑n : EReal)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u : ℕ → ℝ≥0∞
a : EReal
⊢ expGrowthInf u ≤ a ↔ ∀ b > a, ∃ᶠ (n : ℕ) in atTop, u n ≤ (b * (↑n : EReal)).exp
have rw : (∀ y > a, ∃ᶠ (a : ℕ) in atTop, (u a).log / (↑a : EReal) ≤ y) ↔
  ∀ b > a, ∃ᶠ (n : ℕ) in atTop, u n ≤ (b * (↑n : EReal)).exp
Tactic: rw [expGrowthInf, liminf_le_iff']
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u : ℕ → ℝ≥0∞
a : EReal
⊢ (∀ y > a, ∃ᶠ (a : ℕ) in atTop, (u a).log / (↑a : EReal) ≤ y) ↔
    ∀ b > a, ∃ᶠ (n : ℕ) in atTop, u n ≤ (b * (↑n : EReal)).exp
have refine : ∀ b > a, ∀ n ≥ 1, (u n).log / (↑n : EReal) ≤ b ↔ u n ≤ (b * (↑n : EReal)).exp
Tactic: refine forall₂_congr fun b _ ↦ frequently_congr (eventually_atTop.2 ⟨1, fun n _ ↦ ?_⟩)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u : ℕ → ℝ≥0∞
a b : EReal
h : b > a
n : ℕ
h_1 : n ≥ 1
⊢ LT.lt (α := EReal) 0 (↑n : EReal)
have norm_cast : 0 < n
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u : ℕ → ℝ≥0∞
a b : EReal
h : b > a
n : ℕ
h_1 : n ≥ 1
⊢ (u n).log / (↑n : EReal) ≤ b ↔ u n ≤ (b * (↑n : EReal)).exp
have rw : (u n).log ≤ (b * (↑n : EReal)).exp.log ↔ u n ≤ (b * (↑n : EReal)).exp
Tactic: rw [div_le_iff_le_mul (by norm_cast) (natCast_ne_top n), ← log_exp (n * b), mul_comm _ b]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u : ℕ → ℝ≥0∞
a : EReal
⊢ a ≤ expGrowthInf u ↔ ∀ b < a, ∀ᶠ (n : ℕ) in atTop, (b * (↑n : EReal)).exp ≤ u n
have rw : (∀ y < a, ∀ᶠ (a : ℕ) in atTop, y ≤ (u a).log / (↑a : EReal)) ↔
  ∀ b < a, ∀ᶠ (n : ℕ) in atTop, (b * (↑n : EReal)).exp ≤ u n
Tactic: rw [expGrowthInf, le_liminf_iff']
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u : ℕ → ℝ≥0∞
a : EReal
⊢ (∀ y < a, ∀ᶠ (a : ℕ) in atTop, y ≤ (u a).log / (↑a : EReal)) ↔
    ∀ b < a, ∀ᶠ (n : ℕ) in atTop, (b * (↑n : EReal)).exp ≤ u n
have refine : ∀ b < a, ∀ n ≥ 1, b ≤ (u n).log / (↑n : EReal) ↔ (b * (↑n : EReal)).exp ≤ u n
Tactic: refine forall₂_congr fun b _ ↦ eventually_congr (eventually_atTop.2 ⟨1, fun n _ ↦ ?_⟩)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u : ℕ → ℝ≥0∞
a b : EReal
h : b < a
n : ℕ
h_1 : n ≥ 1
⊢ GT.gt (α := EReal) (↑n : EReal) 0
have norm_cast : 0 < n
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u : ℕ → ℝ≥0∞
a b : EReal
h : b < a
n : ℕ
h_1 : n ≥ 1
⊢ b ≤ (u n).log / (↑n : EReal) ↔ (b * (↑n : EReal)).exp ≤ u n
have nth_rw : (b * (↑n : EReal)).exp.log ≤ (u n).log ↔ (b * (↑n : EReal)).exp ≤ u n
Tactic: nth_rw 1 [le_div_iff_mul_le (by norm_cast) (natCast_ne_top n), ← log_exp (b * n)]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u : ℕ → ℝ≥0∞
a : EReal
⊢ expGrowthSup u ≤ a ↔ ∀ b > a, ∀ᶠ (n : ℕ) in atTop, u n ≤ (b * (↑n : EReal)).exp
have rw : (∀ y > a, ∀ᶠ (a : ℕ) in atTop, (u a).log / (↑a : EReal) ≤ y) ↔
  ∀ b > a, ∀ᶠ (n : ℕ) in atTop, u n ≤ (b * (↑n : EReal)).exp
Tactic: rw [expGrowthSup, limsup_le_iff']
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u : ℕ → ℝ≥0∞
a : EReal
⊢ (∀ y > a, ∀ᶠ (a : ℕ) in atTop, (u a).log / (↑a : EReal) ≤ y) ↔
    ∀ b > a, ∀ᶠ (n : ℕ) in atTop, u n ≤ (b * (↑n : EReal)).exp
have refine : ∀ b > a, ∀ n ≥ 1, (u n).log / (↑n : EReal) ≤ b ↔ u n ≤ (b * (↑n : EReal)).exp
Tactic: refine forall₂_congr fun b _ ↦ eventually_congr (eventually_atTop.2 ⟨1, fun n _ ↦ ?_⟩)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u : ℕ → ℝ≥0∞
a : EReal
⊢ a ≤ expGrowthSup u ↔ ∀ b < a, ∃ᶠ (n : ℕ) in atTop, (b * (↑n : EReal)).exp ≤ u n
have rw : (∀ y < a, ∃ᶠ (a : ℕ) in atTop, y ≤ (u a).log / (↑a : EReal)) ↔
  ∀ b < a, ∃ᶠ (n : ℕ) in atTop, (b * (↑n : EReal)).exp ≤ u n
Tactic: rw [expGrowthSup, le_limsup_iff']
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u : ℕ → ℝ≥0∞
a : EReal
⊢ (∀ y < a, ∃ᶠ (a : ℕ) in atTop, y ≤ (u a).log / (↑a : EReal)) ↔
    ∀ b < a, ∃ᶠ (n : ℕ) in atTop, (b * (↑n : EReal)).exp ≤ u n
have refine : ∀ b < a, ∀ n ≥ 1, b ≤ (u n).log / (↑n : EReal) ↔ (b * (↑n : EReal)).exp ≤ u n
Tactic: refine forall₂_congr fun b _ ↦ frequently_congr (eventually_atTop.2 ⟨1, fun n _ ↦ ?_⟩)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u : ℕ → ℝ≥0∞
a : EReal
h : ∃ᶠ (n : ℕ) in atTop, u n ≤ (a * (↑n : EReal)).exp
⊢ expGrowthInf u ≤ a
have apply : ∀ (c : EReal) (c_u : c > a) (n : ℕ) (hn : u n ≤ (a * (↑n : EReal)).exp), (a * (↑n : EReal)).exp ≤ (c * (↑n : EReal)).exp
Tactic: apply expGrowthInf_le_iff.2 fun c c_u ↦ h.mono fun n hn ↦ hn.trans ?_
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u : ℕ → ℝ≥0∞
a : EReal
h : ∃ᶠ (n : ℕ) in atTop, u n ≤ (a * (↑n : EReal)).exp
c : EReal
c_u : c > a
n : ℕ
hn : u n ≤ (a * (↑n : EReal)).exp
⊢ (a * (↑n : EReal)).exp ≤ (c * (↑n : EReal)).exp
have a₁ : LE.le (α := EReal) 0 (↑n : EReal)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u : ℕ → ℝ≥0∞
a : EReal
h : ∀ᶠ (n : ℕ) in atTop, (a * (↑n : EReal)).exp ≤ u n
c : EReal
c_u : c < a
n : ℕ
hn : (a * (↑n : EReal)).exp ≤ u n
⊢ (c * (↑n : EReal)).exp ≤ (a * (↑n : EReal)).exp
have a₁ : LE.le (α := EReal) 0 (↑n : EReal)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u : ℕ → ℝ≥0∞
a : EReal
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ (a * (↑n : EReal)).exp
c : EReal
c_u : c > a
n : ℕ
hn : u n ≤ (a * (↑n : EReal)).exp
⊢ (a * (↑n : EReal)).exp ≤ (c * (↑n : EReal)).exp
have a₁ : LE.le (α := EReal) 0 (↑n : EReal)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u : ℕ → ℝ≥0∞
a : EReal
h : ∃ᶠ (n : ℕ) in atTop, (a * (↑n : EReal)).exp ≤ u n
c : EReal
c_u : c < a
n : ℕ
hn : (a * (↑n : EReal)).exp ≤ u n
⊢ (c * (↑n : EReal)).exp ≤ (a * (↑n : EReal)).exp
have a₁ : LE.le (α := EReal) 0 (↑n : EReal)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
⊢ expGrowthSup 0 = ⊥
have rw : linearGrowthSup (log ∘ 0) = linearGrowthSup ⊥
Tactic: rw [← linearGrowthSup_bot, expGrowthSup_def]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
⊢ linearGrowthSup (log ∘ 0) = linearGrowthSup ⊥
have e_u : Eq (α := ℕ → EReal) (log ∘ 0) ⊥
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
⊢ Eq (α := ℕ → EReal) (log ∘ 0) ⊥
have e_u : ∀ (x : ℕ), (log ∘ 0) x = ⊥ x
Tactic: ext _
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
x : ℕ
⊢ (log ∘ 0) x = ⊥ x
have e_u : log (0 x) = ⊥ x
Tactic: rw [comp_apply, Pi.zero_apply, Pi.bot_apply, log_zero]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
x : ℕ
e_u : log (0 x) = ⊥ x
⊢ (log ∘ 0) x = ⊥ x
have e_u₁ : log 0 = ⊥ x
Tactic: rw [comp_apply, Pi.zero_apply, Pi.bot_apply, log_zero]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
x : ℕ
e_u : log (0 x) = ⊥ x
e_u₁ : log 0 = ⊥ x
⊢ (log ∘ 0) x = ⊥ x
have e_u₂ : log 0 = ⊥
Tactic: rw [comp_apply, Pi.zero_apply, Pi.bot_apply, log_zero]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
x : ℕ
e_u : log (0 x) = ⊥ x
e_u₁ : log 0 = ⊥ x
e_u₂ : log 0 = ⊥
⊢ (log ∘ 0) x = ⊥ x
have e_u₃ : Eq (α := EReal) ⊥ ⊥
Tactic: rw [comp_apply, Pi.zero_apply, Pi.bot_apply, log_zero]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
⊢ expGrowthInf 0 = ⊥
have apply : expGrowthInf 0 ≤ ⊥
Tactic: apply le_bot_iff.1
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
⊢ expGrowthInf 0 ≤ ⊥
have rw : expGrowthInf 0 ≤ expGrowthSup 0
Tactic: rw [← expGrowthSup_zero]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
⊢ expGrowthInf ⊤ = ⊤
have rw : linearGrowthInf (log ∘ ⊤) = linearGrowthInf ⊤
Tactic: rw [← linearGrowthInf_top, expGrowthInf_def]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
⊢ expGrowthSup ⊤ = ⊤
have apply : ⊤ ≤ expGrowthSup ⊤
Tactic: apply top_le_iff.1
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
⊢ ⊤ ≤ expGrowthSup ⊤
have rw : expGrowthInf ⊤ ≤ expGrowthSup ⊤
Tactic: rw [← expGrowthInf_top]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
b : ℝ≥0∞
⊢ (expGrowthInf fun (n : ℕ) ↦ b ^ n) = b.log
have rw : Eq (α := EReal) (liminf (fun (n : ℕ) ↦ (b ^ n).log / (↑n : EReal)) atTop) (liminf (fun (x : ℕ) ↦ b.log) atTop)
Tactic: rw [expGrowthInf, ← liminf_const (f := atTop (α := ℕ)) (log b)]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
b : ℝ≥0∞
⊢ Eq (α := EReal) (liminf (fun (n : ℕ) ↦ (b ^ n).log / (↑n : EReal)) atTop) (liminf (fun (x : ℕ) ↦ b.log) atTop)
have refine : ∀ (n : ℕ) (n_1 : n ≥ 1), (b ^ n).log / (↑n : EReal) = b.log
Tactic: refine liminf_congr (eventually_atTop.2 ⟨1, fun n n_1 ↦ ?_⟩)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
b : ℝ≥0∞
n : ℕ
n_1 : n ≥ 1
⊢ (b ^ n).log / (↑n : EReal) = b.log
have rw : (b ^ n).log = b.log * (↑n : EReal)
Tactic: rw [EReal.div_eq_iff (natCast_ne_bot n) (natCast_ne_top n)
    (zero_lt_one.trans_le (Nat.one_le_cast.2 n_1)).ne.symm, log_pow, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
b : ℝ≥0∞
n : ℕ
n_1 : n ≥ 1
rw : (b ^ n).log = b.log * (↑n : EReal)
⊢ (b ^ n).log / (↑n : EReal) = b.log
have rw₁ : (↑n : EReal) * b.log = b.log * (↑n : EReal)
Tactic: rw [EReal.div_eq_iff (natCast_ne_bot n) (natCast_ne_top n)
    (zero_lt_one.trans_le (Nat.one_le_cast.2 n_1)).ne.symm, log_pow, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
b : ℝ≥0∞
n : ℕ
n_1 : n ≥ 1
rw : (b ^ n).log = b.log * (↑n : EReal)
rw₁ : (↑n : EReal) * b.log = b.log * (↑n : EReal)
⊢ (b ^ n).log / (↑n : EReal) = b.log
have rw₂ : b.log * (↑n : EReal) = b.log * (↑n : EReal)
Tactic: rw [EReal.div_eq_iff (natCast_ne_bot n) (natCast_ne_top n)
    (zero_lt_one.trans_le (Nat.one_le_cast.2 n_1)).ne.symm, log_pow, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
b : ℝ≥0∞
⊢ (expGrowthSup fun (n : ℕ) ↦ b ^ n) = b.log
have rw : Eq (α := EReal) (limsup (fun (n : ℕ) ↦ (b ^ n).log / (↑n : EReal)) atTop) (limsup (fun (x : ℕ) ↦ b.log) atTop)
Tactic: rw [expGrowthSup, ← limsup_const (f := atTop (α := ℕ)) (log b)]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
b : ℝ≥0∞
⊢ Eq (α := EReal) (limsup (fun (n : ℕ) ↦ (b ^ n).log / (↑n : EReal)) atTop) (limsup (fun (x : ℕ) ↦ b.log) atTop)
have refine : ∀ (n : ℕ) (n_1 : n ≥ 1), (b ^ n).log / (↑n : EReal) = b.log
Tactic: refine limsup_congr (eventually_atTop.2 ⟨1, fun n n_1 ↦ ?_⟩)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
⊢ expGrowthInf u + expGrowthInf v ≤ expGrowthInf (u * v)
have refine : ∀ (n : ℕ),
  HAdd.hAdd (α := ℕ → EReal) (β := ℕ → EReal) (fun (n : ℕ) ↦ (u n).log / (↑n : EReal))
      (fun (n : ℕ) ↦ (v n).log / (↑n : EReal)) n =
    ((u * v) n).log / (↑n : EReal)
Tactic: refine le_liminf_add.trans_eq (liminf_congr (Eventually.of_forall fun n ↦ ?_))
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ HAdd.hAdd (α := ℕ → EReal) (β := ℕ → EReal) (fun (n : ℕ) ↦ (u n).log / (↑n : EReal))
      (fun (n : ℕ) ↦ (v n).log / (↑n : EReal)) n =
    ((u * v) n).log / (↑n : EReal)
have rw : (u n).log / (↑n : EReal) + (v n).log / (↑n : EReal) = ((u * v) n).log / (↑n : EReal)
Tactic: rw [Pi.add_apply, Pi.mul_apply, ← add_div_of_nonneg_right n.cast_nonneg', log_mul_add]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
n : ℕ
rw : (u n).log / (↑n : EReal) + (v n).log / (↑n : EReal) = ((u * v) n).log / (↑n : EReal)
⊢ HAdd.hAdd (α := ℕ → EReal) (β := ℕ → EReal) (fun (n : ℕ) ↦ (u n).log / (↑n : EReal))
      (fun (n : ℕ) ↦ (v n).log / (↑n : EReal)) n =
    ((u * v) n).log / (↑n : EReal)
have rw₁ : (u n).log / (↑n : EReal) + (v n).log / (↑n : EReal) = (u n * v n).log / (↑n : EReal)
Tactic: rw [Pi.add_apply, Pi.mul_apply, ← add_div_of_nonneg_right n.cast_nonneg', log_mul_add]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
n : ℕ
rw : (u n).log / (↑n : EReal) + (v n).log / (↑n : EReal) = ((u * v) n).log / (↑n : EReal)
rw₁ : (u n).log / (↑n : EReal) + (v n).log / (↑n : EReal) = (u n * v n).log / (↑n : EReal)
⊢ HAdd.hAdd (α := ℕ → EReal) (β := ℕ → EReal) (fun (n : ℕ) ↦ (u n).log / (↑n : EReal))
      (fun (n : ℕ) ↦ (v n).log / (↑n : EReal)) n =
    ((u * v) n).log / (↑n : EReal)
have rw₂ : ((u n).log + (v n).log) / (↑n : EReal) = (u n * v n).log / (↑n : EReal)
Tactic: rw [Pi.add_apply, Pi.mul_apply, ← add_div_of_nonneg_right n.cast_nonneg', log_mul_add]