# Zulip Chat Archive

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