Specializing filters to sequences

Stream: new members

[Jalex Stark]

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]

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

[Jalex Stark]

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

[Yury G. Kudryashov]

BTW, why do you want C N : nat?

[Jalex Stark]

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

[Yury G. Kudryashov]

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]

The computer scientist also wants the functions to be \N \to \N but that seems like more work

[Jalex Stark]

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

[Yury G. Kudryashov]

Fixed.

[Jalex Stark]

Awesome, thanks!

[Yury G. Kudryashov]

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.