awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hAB : ∀ i ∈ s, IsBigOWith (C i) l (A i) (B i)
hs : s.Nonempty
inr :
  ∀ (hAB : ∀ i ∈ s, ∀ᶠ (x : α) in l, ‖A i x‖ ≤ C i * ‖B i x‖),
    ∀ᶠ (x : α) in l, norm.{u_6} (E := E') (∑ i ∈ s, A i x) ≤ sSup (C '' (↑s : Set ι)) * norm (E := ℝ) (∑ i ∈ s, ‖B i x‖)
⊢ IsBigOWith.{u_1, u_6, 0} (E := E') (F := ℝ) (sSup (C '' (↑s : Set ι))) l (fun (H : α) ↦ ∑ i ∈ s, A i H) fun (H : α) ↦
    ∑ i ∈ s, ‖B i H‖

Tactic:
simp only [IsBigOWith_def] at *

Premises used: Asymptotics.IsBigOWith_def
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hs : s.Nonempty
hAB : ∀ i ∈ s, ∀ᶠ (x : α) in l, ‖A i x‖ ≤ C i * ‖B i x‖
h :
  ∀ (x : α) (hx : ∀ i ∈ s, ‖A i x‖ ≤ C i * ‖B i x‖),
    norm.{u_6} (E := E') (∑ i ∈ s, A i x) ≤ sSup (C '' (↑s : Set ι)) * norm (E := ℝ) (∑ i ∈ s, ‖B i x‖)
⊢ ∀ᶠ (x : α) in l, norm.{u_6} (E := E') (∑ i ∈ s, A i x) ≤ sSup (C '' (↑s : Set ι)) * norm (E := ℝ) (∑ i ∈ s, ‖B i x‖)

Tactic:
filter_upwards [(eventually_all_finset s).mpr hAB]
    with x hx

Premises used: Iff.mpr, Filter.eventually_all_finset
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hs : s.Nonempty
hAB : ∀ i ∈ s, ∀ᶠ (x : α) in l, ‖A i x‖ ≤ C i * ‖B i x‖
x : α
hx : ∀ i ∈ s, ‖A i x‖ ≤ C i * ‖B i x‖
⊢ norm.{u_6} (E := E') (∑ i ∈ s, A i x) ≤ ∑ i ∈ s, ‖A i x‖

Tactic:
norm_sum_le ..

Premises used: norm_sum_le
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hs : s.Nonempty
hAB : ∀ i ∈ s, ∀ᶠ (x : α) in l, ‖A i x‖ ≤ C i * ‖B i x‖
x : α
hx : ∀ i ∈ s, ‖A i x‖ ≤ C i * ‖B i x‖
⊢ LE.le (α := ℝ) (∑ i ∈ s, ‖A i x‖) (∑ i ∈ s, C i * ‖B i x‖)

Tactic:
Finset.sum_le_sum (fun j hj ↦ hx j hj)

Premises used: Finset.sum_le_sum
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hs : s.Nonempty
hAB : ∀ i ∈ s, ∀ᶠ (x : α) in l, ‖A i x‖ ≤ C i * ‖B i x‖
x : α
hx : ∀ i ∈ s, ‖A i x‖ ≤ C i * ‖B i x‖
⊢ LE.le (α := ℝ) (∑ i ∈ s, C i * ‖B i x‖) (∑ i ∈ s, sSup (C '' (↑s : Set ι)) * ‖B i x‖)

Tactic:
Finset.sum_le_sum ?_

Premises used: Finset.sum_le_sum
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hs : s.Nonempty
hAB : ∀ i ∈ s, ∀ᶠ (x : α) in l, ‖A i x‖ ≤ C i * ‖B i x‖
x : α
hx : ∀ i ∈ s, ‖A i x‖ ≤ C i * ‖B i x‖
refine : ∀ i ∈ s, C i * ‖B i x‖ ≤ sSup (C '' (↑s : Set ι)) * ‖B i x‖
⊢ LE.le (α := ℝ) (∑ i ∈ s, C i * ‖B i x‖) (∑ i ∈ s, sSup (C '' (↑s : Set ι)) * ‖B i x‖)

Tactic:
refine Finset.sum_le_sum ?_

Premises used: Finset.sum_le_sum
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hs : s.Nonempty
hAB : ∀ i ∈ s, ∀ᶠ (x : α) in l, ‖A i x‖ ≤ C i * ‖B i x‖
x : α
hx : ∀ i ∈ s, ‖A i x‖ ≤ C i * ‖B i x‖
j : ι
hj : j ∈ s
hbc : C j ≤ sSup (C '' (↑s : Set ι))
⊢ C j * ‖B j x‖ ≤ sSup (C '' (↑s : Set ι)) * ‖B j x‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hs : s.Nonempty
hAB : ∀ i ∈ s, ∀ᶠ (x : α) in l, ‖A i x‖ ≤ C i * ‖B i x‖
x : α
hx : ∀ i ∈ s, ‖A i x‖ ≤ C i * ‖B i x‖
j : ι
hj : j ∈ s
hbc : ∃ b ∈ s, C j ≤ C b
⊢ C j ≤ sSup (C '' (↑s : Set ι))

Tactic:
rw [← s.sup'_eq_csSup_image hs, Finset.le_sup'_iff]

Premises used: Finset.le_sup'_iff, Finset.sup'_eq_csSup_image
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hs : s.Nonempty
hAB : ∀ i ∈ s, ∀ᶠ (x : α) in l, ‖A i x‖ ≤ C i * ‖B i x‖
x : α
hx : ∀ i ∈ s, ‖A i x‖ ≤ C i * ‖B i x‖
j : ι
hj : j ∈ s
w : ι
h : j ∈ s ∧ C j ≤ C j
⊢ ∃ b ∈ s, C j ≤ C b

Tactic:
use j
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hs : s.Nonempty
hAB : ∀ i ∈ s, ∀ᶠ (x : α) in l, ‖A i x‖ ≤ C i * ‖B i x‖
x : α
hx : ∀ i ∈ s, ‖A i x‖ ≤ C i * ‖B i x‖
⊢ ∑ i ∈ s, sSup (C '' (↑s : Set ι)) * ‖B i x‖ = sSup (C '' (↑s : Set ι)) * ∑ i ∈ s, ‖B i x‖

Tactic:
(Finset.mul_sum ..).symm

Premises used: Finset.mul_sum, Eq.symm
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hs : s.Nonempty
hAB : ∀ i ∈ s, ∀ᶠ (x : α) in l, ‖A i x‖ ≤ C i * ‖B i x‖
x : α
hx : ∀ i ∈ s, ‖A i x‖ ≤ C i * ‖B i x‖
e_a : ∑ i ∈ s, ‖B i x‖ = norm (E := ℝ) (∑ i ∈ s, ‖B i x‖)
⊢ sSup (C '' (↑s : Set ι)) * ∑ i ∈ s, ‖B i x‖ = sSup (C '' (↑s : Set ι)) * norm (E := ℝ) (∑ i ∈ s, ‖B i x‖)

Tactic:
congr
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hs : s.Nonempty
hAB : ∀ i ∈ s, ∀ᶠ (x : α) in l, ‖A i x‖ ≤ C i * ‖B i x‖
x : α
hx : ∀ i ∈ s, ‖A i x‖ ≤ C i * ‖B i x‖
e_a e_a₁ : Eq (α := ℝ) (∑ i ∈ s, ‖B i x‖) (∑ i ∈ s, ‖B i x‖)
⊢ ∑ i ∈ s, ‖B i x‖ = norm (E := ℝ) (∑ i ∈ s, ‖B i x‖)

Tactic:
rw [Real.norm_of_nonneg (Finset.sum_nonneg (fun _ _ ↦ norm_nonneg _))]

Premises used: Finset.sum_nonneg, norm_nonneg, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hs : s.Nonempty
hAB : ∀ i ∈ s, ∀ᶠ (x : α) in l, ‖A i x‖ ≤ C i * ‖B i x‖
x : α
hx : ∀ i ∈ s, ‖A i x‖ ≤ C i * ‖B i x‖
i : LE.le (α := ℝ) (∑ i ∈ s, C i * ‖B i x‖) (∑ i ∈ s, sSup (C '' (↑s : Set ι)) * ‖B i x‖)
i₁ : sSup (C '' (↑s : Set ι)) * ∑ i ∈ s, ‖B i x‖ = sSup (C '' (↑s : Set ι)) * norm (E := ℝ) (∑ i ∈ s, ‖B i x‖)
⊢ norm.{u_6} (E := E') (∑ i ∈ s, A i x) ≤ sSup (C '' (↑s : Set ι)) * norm (E := ℝ) (∑ i ∈ s, ‖B i x‖)

Tactic:
calc
    ‖∑ i ∈ s, A i x‖ ≤ ∑ i ∈ s, ‖A i x‖ := norm_sum_le ..
    _ ≤ ∑ i ∈ s, C i * ‖B i x‖ := Finset.sum_le_sum (fun j hj ↦ hx j hj)
    _ ≤ ∑ i ∈ s, sSup (C '' s) * ‖B i x‖ := by
        refine Finset.sum_le_sum ?_
        intro j hj; gcongr
        rw [← s.sup'_eq_csSup_image hs, Finset.le_sup'_iff]; use j
    _ = sSup (C '' s) * ∑ i ∈ s, ‖B i x‖ := (Finset.mul_sum ..).symm
    _ = sSup (C '' s) * ‖∑ i ∈ s, ‖B i x‖‖ := by
      congr; rw [Real.norm_of_nonneg (Finset.sum_nonneg (fun _ _ ↦ norm_nonneg _))]

Premises used: Finset.mul_sum, SetLike.coe, Set.image, Finset.sum_le_sum, Eq.symm, norm_sum_le, SupSet.sSup
-- Module: Mathlib.Analysis.Asymptotics.Defs
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
simp :
  ∀ (hAB : ∀ i ∈ s, ∃ (c : ℝ), IsBigOWith c l (A i) (B i)),
    ∃ (c : ℝ),
      IsBigOWith.{u_1, u_6, 0} (E := E') (F := ℝ) c l (fun (H : α) ↦ ∑ i ∈ s, A i H) fun (H : α) ↦ ∑ i ∈ s, ‖B i H‖
⊢ IsBigO.{u_1, u_6, 0} (E := E') (F := ℝ) l (fun (H : α) ↦ ∑ i ∈ s, A i H) fun (H : α) ↦ ∑ i ∈ s, ‖B i H‖

Tactic:
simp only [IsBigO_def] at *

Premises used: Asymptotics.IsBigO_def
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
s : Finset ι
B : ι → α → ℝ
hAB : ∀ i ∈ s, ∃ (c : ℝ), IsBigOWith c l (A i) (B i)
choose! :
  ∀ (C : (i : ι) → ℝ) (hC : ∀ i ∈ s, IsBigOWith (C i) l (A i) (B i)),
    ∃ (c : ℝ),
      IsBigOWith.{u_1, u_6, 0} (E := E') (F := ℝ) c l (fun (H : α) ↦ ∑ i ∈ s, A i H) fun (H : α) ↦ ∑ i ∈ s, ‖B i H‖
⊢ ∃ (c : ℝ),
    IsBigOWith.{u_1, u_6, 0} (E := E') (F := ℝ) c l (fun (H : α) ↦ ∑ i ∈ s, A i H) fun (H : α) ↦ ∑ i ∈ s, ‖B i H‖

Tactic:
choose! C hC using hAB
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
s : Finset ι
B : ι → α → ℝ
C : (i : ι) → ℝ
hC : ∀ i ∈ s, IsBigOWith (C i) l (A i) (B i)
⊢ ∃ (c : ℝ),
    IsBigOWith.{u_1, u_6, 0} (E := E') (F := ℝ) c l (fun (H : α) ↦ ∑ i ∈ s, A i H) fun (H : α) ↦ ∑ i ∈ s, ‖B i H‖

Tactic:
⟨_, IsBigOWith.sum_congr hC⟩

Premises used: Asymptotics.IsBigOWith.sum_congr, Exists.intro
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
s : Finset ι
B : ι → α → ℝ
C : (i : ι) → ℝ
hC : ∀ i ∈ s, IsBigOWith (C i) l (A i) (B i)
⊢ ∃ (c : ℝ),
    IsBigOWith.{u_1, u_6, 0} (E := E') (F := ℝ) c l (fun (H : α) ↦ ∑ i ∈ s, A i H) fun (H : α) ↦ ∑ i ∈ s, ‖B i H‖

Tactic:
exact ⟨_, IsBigOWith.sum_congr hC⟩
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
s : Finset ι
B : ι → α → ℝ
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:
simp [isLittleO_zero]

Premises used: Asymptotics.isLittleO_zero
-- Module: Mathlib.Analysis.Asymptotics.Defs
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
cons :
  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‖
⊢ 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:
simp_rw [Finset.sum_cons]

Premises used: Finset.sum_cons
-- Module: Mathlib.Analysis.Asymptotics.Defs
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
⊢ i ∈ Finset.cons i s his

Tactic:
simp
-- Module: Mathlib.Analysis.Asymptotics.Defs
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
j : ι
hj : j ∈ s
⊢ j ∈ Finset.cons i s his

Tactic:
simp [hj]
-- Module: Mathlib.Analysis.Asymptotics.Defs
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‖

Tactic:
Eventually.of_forall fun H ↦ congr_arg (‖B i H‖ + ·) ?_

Premises used: Norm.norm, Filter.EventuallyEq, Filter.Eventually.of_forall, congr_arg, HAdd.hAdd
-- Module: Mathlib.Analysis.Asymptotics.Defs
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
refine : ∀ (H : α), norm (E := ℝ) (∑ j ∈ s, ‖B j H‖) = ∑ j ∈ s, ‖B j H‖
⊢ 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:
refine Eventually.of_forall fun H ↦ congr_arg (‖B i H‖ + ·) ?_

Premises used: Norm.norm, Filter.Eventually.of_forall, congr_arg, HAdd.hAdd
-- Module: Mathlib.Analysis.Asymptotics.Defs
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
H : α
⊢ norm (E := ℝ) (∑ j ∈ s, ‖B j H‖) = ∑ j ∈ s, ‖B j H‖

Tactic:
Real.norm_of_nonneg (Finset.sum_nonneg fun _ _ => norm_nonneg _)

Premises used: Finset.sum_nonneg, norm_nonneg, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.Asymptotics.Defs
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
H : α
⊢ norm (E := ℝ) (∑ j ∈ s, ‖B j H‖) = ∑ j ∈ s, ‖B j H‖

Tactic:
exact Real.norm_of_nonneg (Finset.sum_nonneg fun _ _ => norm_nonneg _)

Premises used: Finset.sum_nonneg, norm_nonneg, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.Asymptotics.Defs
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
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‖
⊢ 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‖

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 _)

Premises used: Norm.norm, HAdd.hAdd, Asymptotics.IsLittleO.add_add, Finset.sum
-- Module: Mathlib.Analysis.Asymptotics.Defs
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‖
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‖
⊢ IsLittleO.{u_1, u_6, 0} (E := E') (F := ℝ) l (fun (H : α) ↦ ∑ i ∈ s, A i H) fun (H : α) ↦ ∑ i ∈ s, ‖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 _)

Premises used: Finset.sum_cons, Asymptotics.isLittleO_zero
-- Module: Mathlib.Analysis.Asymptotics.Defs
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)
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‖)
⊢ 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 [IsBigOWith_def] at *

Premises used: Asymptotics.IsBigOWith_def
-- Module: Mathlib.Analysis.Asymptotics.Defs
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‖
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‖)
⊢ ∀ᶠ (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

Premises used: Filter.eventually_prod_iff, Iff.mp
-- Module: Mathlib.Analysis.Asymptotics.Defs
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 : ∀ (H : α) (hH : s₂ H), norm.{u_6} (E := E') (∑ j ∈ i H, A j H) ≤ C * norm (E := ℝ) (∑ j ∈ i H, ‖B j H‖)
⊢ ∀ᶠ (x : α) in l, norm.{u_6} (E := E') (∑ j ∈ i x, A j x) ≤ C * norm (E := ℝ) (∑ j ∈ i x, ‖B j x‖)

Tactic:
filter_upwards [hs₂] with H hH
-- Module: Mathlib.Analysis.Asymptotics.Defs
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) ≤ ∑ j ∈ i H, ‖A j H‖

Tactic:
norm_sum_le ..

Premises used: norm_sum_le
-- Module: Mathlib.Analysis.Asymptotics.Defs
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
⊢ LE.le (α := ℝ) (∑ j ∈ i H, ‖A j H‖) (∑ j ∈ i H, C * ‖B j H‖)

Tactic:
Finset.sum_le_sum fun j _ => hbound (Filter.eventually_top.mp hs₁ j) hH

Premises used: Filter.eventually_top, Iff.mp, Finset.sum_le_sum
-- Module: Mathlib.Analysis.Asymptotics.Defs
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, C * ‖B j H‖ = C * ∑ j ∈ i H, ‖B j H‖

Tactic:
(Finset.mul_sum ..).symm

Premises used: Finset.mul_sum, Eq.symm
-- Module: Mathlib.Analysis.Asymptotics.Defs
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
e_a : ∑ j ∈ i H, ‖B j H‖ = norm (E := ℝ) (∑ j ∈ i H, ‖B j H‖)
⊢ C * ∑ j ∈ i H, ‖B j H‖ = C * norm (E := ℝ) (∑ j ∈ i H, ‖B j H‖)

Tactic:
congr
-- Module: Mathlib.Analysis.Asymptotics.Defs
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
e_a e_a₁ : Eq (α := ℝ) (∑ j ∈ i H, ‖B j H‖) (∑ i ∈ i H, ‖B i H‖)
⊢ ∑ j ∈ i H, ‖B j H‖ = norm (E := ℝ) (∑ j ∈ i H, ‖B j H‖)

Tactic:
rw [Real.norm_of_nonneg (Finset.sum_nonneg (fun _ _ ↦ norm_nonneg _))]

Premises used: Finset.sum_nonneg, norm_nonneg, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.Asymptotics.Defs
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 : C * ∑ j ∈ i H, ‖B j H‖ = C * norm (E := ℝ) (∑ j ∈ i H, ‖B j H‖)
⊢ norm.{u_6} (E := E') (∑ j ∈ i H, A 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 _))]

Premises used: Finset.mul_sum, Filter.eventually_top, Iff.mp, Finset.sum_le_sum, Eq.symm, norm_sum_le
-- Module: Mathlib.Analysis.Asymptotics.Defs
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
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‖
⊢ 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‖

Tactic:
simp only [IsBigO_def]

Premises used: Asymptotics.IsBigO_def