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 :=
rw [is_O, is_O', asymptotics.is_O],
cases a with c a,
cases a with N a,
use c,
refine asymptotics.is_O_with_of_le' filter.at_top _,

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


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