Adding big-O

Stream: Is there code for X?

[Gareth Ma]

Is there code for the following?

example {f g h : ℤ → ℝ} (hf : f =O[atTop] h) (hg : g =O[atTop] h) : (f + g) =O[atTop] h := by
  sorry

[Yaël Dillies]

docs#Asymptotics.IsBigO.add

[Gareth Ma]

wtf I swear when I tried hf.add 5 minutes ago it didn't work

[Gareth Ma]

Thanks sorry

[Jireh Loreaux]

@Gareth Ma You can also do the following, which fails to find anything because the terms are kind of eta-expanded (not exactly).

@loogle ⊢ (?f + ?g) =O[?l] ?h

[Jireh Loreaux]

@loogle ⊢ (?f + ?g) =O[?l] ?h

[loogle]

:shrug: nothing found

[Jireh Loreaux]

3rd hit:

@loogle HAdd.hAdd, ⊢ ?f =O[?l] ?h

[loogle]

:search: Asymptotics.IsLittleO.right_isBigO_add, Asymptotics.IsLittleO.right_isBigO_add', and 11 more

[Jireh Loreaux]

1st hit:

@loogle ⊢ (fun x ↦ ?f x + ?g x) =O[?l] ?h

[loogle]

:search: Asymptotics.IsBigO.add, Asymptotics.IsBigO.add_isLittleO, and 2 more