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],
        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`

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