Proving complexity bounds

Stream: new members

[Meyer Zinn]

I have a simple proof for an introductory computer science problem, which is simply showing that f(n)=n^2 is little-oh of g(n)=n^3 (since the limit as n tends to infinity of f(n)/g(n) is zero). However, I'm having trouble understanding how filters (and limits generally) work in Lean.

So far, I think I've been able to state the problem as

noncomputable def f : ℕ → ℝ := λ n, n ^ (2:ℤ)
noncomputable def g : ℕ → ℝ := λ n, n ^ (3:ℤ)
example : is_o f g filter.at_top := by sorry

(if I understand how asymptotics work. I chose to use integer exponents to be able to use fpow, but I don't know if that was the right move). I've also been able to do some manipulations to show that, when n \ne 0, f(n)/g(n)=1/(↑n) (for f g: nat -> real). How do I tie these together to show that the limit of 1/x tends to zero, and that implies little oh?

[Floris van Doorn]

The result docs#tendsto.inv_tendsto_zero (and the surrounding results) will be useful for this

[Floris van Doorn]

Oh, didn't mean that one. It is this result: docs#tendsto_inv_at_top_zero

[Meyer Zinn]

Floris van Doorn said:

Oh, didn't mean that one. It is this result: docs#tendsto_inv_at_top_zero

I'll take a look, thanks for the pointer!

[Meyer Zinn]

I guess now I'm a little confused by how to prove that the limit of f(n)/g(n) is the same as the limit of n^(-1). I shouldn't need to consider what actually happens at n=0 since that's the entire point of a limit, but the following strategy does not work to show equivalence:

have f_div_g_eq_x_inv : ∀ n, f n / g n = 1 / n := begin
        intro n,
        rw [f, g],
        simp,
        rw div_eq_mul_inv,
        rw ← inv_fpow,
        rw ← fpow_neg_one,
        rw ← fpow_mul,
        have neg_three : (-1 : ℤ) * 3 = -3 := by ring,
        rw neg_three,
        rw ← fpow_add,
        have two_minus_three : (2 : ℤ) + (-3) = -1 := by ring,
        rw two_minus_three,
        -- need to prove `\u n \ne 0`
    end,

I could amend the lemma to be \forall (n \ne 0) (or similar), but I return to the issue of not knowing how to interface with the limit definition.

[Floris van Doorn]

• About not knowing the interface: one way is to search for theorems (such as via https://leanprover-community.github.io/mathlib_docs/find/tendsto_congr) using our #naming conventions and then browsing results near the ones that look useful.
• You should be able to use prove the equality for all n, since division by 0 is defined to be 0. You could start the proof with by_cases hn : n = 0 and simp [hn] can simplify the fractions away in the case that n = 0.
• There should also be a congruence lemma for tendsto that allows you to only show the equality for "sufficiently large" n. I couldn't find such a result myself, though, so maybe it doesn't exist yet.

[Anatole Dedecker]

It should be docs#filter.tendsto_congr'

[Anatole Dedecker]

Oh and you might be interested by a result I proved in #4979 : https://github.com/leanprover-community/mathlib/pull/4979/files#diff-7adbc7098d121dfb6c1742ffe2994f62b43d80d894716e85a8e9260d670d5d7cR45