## Stream: new members

### Topic: Proving complexity bounds

#### Meyer Zinn (Nov 25 2020 at 04:22):

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 (Nov 25 2020 at 04:49):

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

#### Floris van Doorn (Nov 25 2020 at 04:50):

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

#### Meyer Zinn (Nov 25 2020 at 05:07):

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 (Nov 25 2020 at 05:19):

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 (Nov 25 2020 at 05:50):

• 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 (Nov 25 2020 at 06:58):

It should be docs#filter.tendsto_congr'

#### Anatole Dedecker (Nov 25 2020 at 08:14):

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

Last updated: May 13 2021 at 22:15 UTC