# Zulip Chat Archive

## Stream: new members

### Topic: Specializing filters to sequences

#### Jalex Stark (Mar 03 2020 at 19:53):

I am trying to show that the big oh relation defined in analysis.asymptotics is the same as the one I know as a working computer scientist. The hope would be to use my definition for proving some ``atomic'' inequalities like

\forall \eps : \R, \eps > 0 \i (\lamdba n, log n) is_o (\lambda n, n^\eps)

and then use the abstract API in mathlib for facts like "is_o is a partial order"

import tactic import data.nat.basic import analysis.complex.exponential import analysis.asymptotics noncomputable theory open_locale classical def is_O' (f g : ℝ → ℝ) : Prop := asymptotics.is_O f g (filter.at_top) def is_O (f g : ℝ → ℝ) : Prop := ∃ c N : ℕ, ∀ x : ℝ , (N:ℝ) ≤ x → f x ≤ c * g x theorem is_O_eq_is_O' (f g : ℝ → ℝ ) : is_O f g → is_O' f g := begin rw [is_O, is_O', asymptotics.is_O], intro, cases a with c a, cases a with N a, use c, refine asymptotics.is_O_with_of_le' filter.at_top _, end

#### Yury G. Kudryashov (Mar 03 2020 at 19:57):

I'd first `simp only [is_O', asymptotics.is_O, filter.mem_at_top_sets]`

#### Jalex Stark (Mar 03 2020 at 20:00):

That brings me to `lean is_O f g → (∃ (c : ℝ), asymptotics.is_O_with c f g filter.at_top)`

#### Yury G. Kudryashov (Mar 03 2020 at 20:02):

BTW, why do you want `C N : nat`

?

#### Jalex Stark (Mar 03 2020 at 20:02):

That's just how a computer scientist would state it. The arguments are the same with c N : \R

#### Yury G. Kudryashov (Mar 03 2020 at 20:03):

import analysis.asymptotics open filter open_locale filter lemma is_O_iff {f g : ℝ → ℝ} : asymptotics.is_O f g at_top ↔ ∃ (c N : ℝ), ∀ x : ℝ , N ≤ x → abs (f x) ≤ c * abs (g x) := by simp only [asymptotics.is_O, asymptotics.is_O_with, eventually_at_top, real.norm_eq_abs]

#### Jalex Stark (Mar 03 2020 at 20:03):

The computer scientist also wants the functions to be `\N \to \N `

but that seems like more work

#### Jalex Stark (Mar 03 2020 at 20:04):

hmm I have open_locale filter but it says unknown identifier 'eventually_at_top'

#### Yury G. Kudryashov (Mar 03 2020 at 20:05):

Fixed.

#### Jalex Stark (Mar 03 2020 at 20:05):

Awesome, thanks!

#### Yury G. Kudryashov (Mar 03 2020 at 20:09):

More generally:

lemma is_O_at_top_iff {α : Type*} [lattice.semilattice_sup α] [nonempty α] {E : Type*} [has_norm E] {f g : α → E} : asymptotics.is_O f g at_top ↔ ∃ c N, ∀ x : α, N ≤ x → ∥f x∥ ≤ c * ∥g x∥ := by simp only [asymptotics.is_O, asymptotics.is_O_with, eventually_at_top]

Feel free to prove a similar fact about `is_o`

, and PR both of them.

Last updated: May 12 2021 at 23:13 UTC