Zulip Chat Archive

Stream: new members

Topic: Incipient numerical analysis results


view this post on Zulip Dan Stanescu (Jul 25 2020 at 15:32):

I've made some progress towards formalizing the proof that the sequence approximating 2\sqrt{2} (say) generated by Newton's method converges. I used the sequence x0=2,xn+1=(xn2+2)/(2xn)x_0 = 2, x_{n+1} = (x_n^2 + 2)/(2*x_n). There are claims the ancient Sumerians knew of such and it appears in baby Rudin as an exercise (page 81). I've shown the sequence is bounded below, decreasing and also that a finite limit exists. I did that using mathlib tools, as opposed to using my own definitions of convergence etc, which was at times difficult but rewarding (at places I needed to switch to the increasing sequence sn=2xns_n = \sqrt{2} - x_n instead to use mathlib's definition of monotone). I'm at the last stage now, where I have to actually prove that the limit is 2\sqrt{2}. Rudin's suggested proof: given that the limit LL exists, get L=(1/2)(L+2/L)L = (1/2)*(L + 2 / L) from the recurrence relationship, whence LL. This is straightforward on paper, but (supposing I can prove L0L \ne 0) is it something that can be achieved solely with the tools in mathib? Can anyone advise me how to proceed here within this restriction? The code (which still needs some clean-up) is available here.

view this post on Zulip Bryan Gin-ge Chen (Jul 25 2020 at 15:34):

(deleted)

view this post on Zulip Patrick Massot (Jul 25 2020 at 16:21):

I'm not sure what is the obstacle here. Dan, do you want the following?

lemma dan_limit {u :   } {L : } {f :   } (hu : tendsto u at_top $ 𝓝 L)
(hf : continuous_at f L) (huf :  n, u (n+1) = f (u n)) : f L = L :=
begin
  have lim : tendsto (u  nat.succ) at_top (𝓝 L) :=
    (tendsto_add_at_top_iff_nat 1).mpr hu,
  rw show u  nat.succ = f  u, from funext huf at lim,
  exact tendsto_nhds_unique (tendsto.comp hf hu) lim
end

view this post on Zulip Patrick Massot (Jul 25 2020 at 16:24):

Or is the issue solving the equation on L?

view this post on Zulip Patrick Massot (Jul 25 2020 at 16:24):

(which is probably much harder :sad:)

view this post on Zulip Dan Stanescu (Jul 25 2020 at 16:26):

I didn't say there was an issue, I was just wondering whether this can be done with what we have. I'm not at all familiar with all the tools we have as of now.

@Patrick Massot Thanks Patrick! I'll try to use this and it may be that this completely solves the problem. If not, I'll come back for more help.

view this post on Zulip Jalex Stark (Jul 25 2020 at 16:29):

i'd guess the most efficient way to solve the equation is to manipulate it into a quadratic by hand with rw, and then I think the quadratic formula is already in mathlib

view this post on Zulip Patrick Massot (Jul 25 2020 at 16:36):

lemma dan_eqn {L : } (h : L = (L*L + 2)/(2*L)) (h' : 0 < L) : L = real.sqrt 2 :=
begin
  apply_fun (λ x, 2*L*x) at h,
  simp_rw mul_div_cancel' _ (ne_of_gt (by linarith) : 2*L  0) at h,
  apply_fun (λ x, x - L*L) at h,
  ring at h,
  symmetry,
  rwa real.sqrt_eq_iff_sqr_eq ; linarith
end

view this post on Zulip Dan Stanescu (Jul 25 2020 at 16:39):

And now I managed to get two lemmas with my name attached-:)
Wait, it's even better: my name prepended.

view this post on Zulip Patrick Massot (Jul 25 2020 at 16:40):

Actually only the second line is a bit ugly. Otherwise this is almost what you would do on paper. But really there should be a tactic doing it in one line.

view this post on Zulip Dan Stanescu (Jul 25 2020 at 22:47):

I finally have everything, so this little project is finished. However, I needed more than 25 lines of code to get the result below (I went all the way to showing false from at_top = ⊥ ). Very instructive, but now that I did can someone please show me a more reasonable proof of the following:

import analysis.specific_limits

open_locale topological_space
open filter

example (s :   ) (hs :  n : , 2 < s n) : ¬ (tendsto s at_top (𝓝 0)) :=
begin
   sorry,
end

view this post on Zulip Reid Barton (Jul 25 2020 at 23:31):

example (s :   ) (hs :  n : , 2 < s n) : ¬ (tendsto s at_top (𝓝 0)) :=
begin
  rw metric.tendsto_at_top,
  push_neg,
  refine 2, by norm_num, λ N, N, le_refl _, _⟩⟩,
  change 2  abs (s N - 0),
  refine le_trans _ (le_abs_self _),
  specialize hs N,
  linarith
end

view this post on Zulip Dan Stanescu (Jul 26 2020 at 00:35):

Twenty lines less, thanks @Reid Barton

view this post on Zulip Dan Stanescu (Jul 26 2020 at 15:45):

To wrap this up, is there anyone who thinks this should go somewhere in mathlib (possibly archive) upon clean-up and possibly generalization to a\sqrt{a} instead of 2\sqrt{2} only? It would probably be a nice little student project.

Thanks again to everyone!

view this post on Zulip Mario Carneiro (Jul 26 2020 at 15:59):

An alternative way to prove the tendsto statement is to observe that if it did then 0 would lie in the closure of Ioi 2, which is Ici 2

view this post on Zulip Mario Carneiro (Jul 26 2020 at 16:08):

example (s :   ) (hs :  n : , 2 < s n) : ¬ (tendsto s at_top (𝓝 0)) :=
begin
  have : (0:)  set.Ici (2 : ), { simp, norm_num },
  rw  closure_Ioi at this,
  exact λ h, this (mem_closure_of_tendsto h (eventually_of_forall hs)),
end

view this post on Zulip Alex J. Best (Jul 26 2020 at 16:19):

I think some version of this would be cool to have, how easily does what you have generalize to any convex function (is it even true that newtons method always converges for single variable convex functions)?

view this post on Zulip Mario Carneiro (Jul 26 2020 at 16:21):

well it has to be differentiable at least

view this post on Zulip Mario Carneiro (Jul 26 2020 at 16:22):

convergence of newton's method for arbitrary convex differentiable functions would be a cool result but probably has very little in common with Dan's proof

view this post on Zulip Dan Stanescu (Jul 26 2020 at 16:24):

I don't think the method will converge in general for a convex function, even if differentiable.

view this post on Zulip Dan Stanescu (Jul 26 2020 at 16:25):

The update rule is xn+1=xnf(xn)/f(xn)x_{n+1} = x_n - f(x_n) / f'(x_n).

view this post on Zulip Dan Stanescu (Jul 26 2020 at 16:26):

There's no guarantee the iterates won't hit a point where the first derivative is zero.

view this post on Zulip Kevin Buzzard (Jul 26 2020 at 16:27):

For continuous functions on the p-adic numbers, as long as x_0 is sufficiently close to the root (condition which depends on f(x_0) and f'(x_0)) then it always converges.

view this post on Zulip Dan Stanescu (Jul 26 2020 at 16:29):

My previous statements should be read as applying to real-valued functions of one real variable.


Last updated: May 18 2021 at 17:44 UTC