## 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'

Fixed.

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: Dec 20 2023 at 11:08 UTC