search

lawrencecpaulson / lawrencecpaulson.github.io

the blog "Machine Logic"
12 stars 0 forks source link

https://lawrencecpaulson.github.io/2022/01/12/Proving-the-obvious.html #8

Open utterances-bot opened 2 years ago

utterances-bot commented 2 years ago

Machine Logic

https://lawrencecpaulson.github.io/2022/01/12/Proving-the-obvious.html

cplaursen commented 2 years ago

Hi, I managed to prove the field_derivative_lim_unique lemma.


lemma field_derivative_lim_unique:
  assumes f: "(f has_field_derivative df) (at z)"
      and s: "s ⇢ 0"  "⋀n. s n ≠ 0" 
      and a: "(λn. (f (z + s n) - f z) / s n) ⇢ a"
    shows "df = a"
proof -
  from f have "((λk. (f (z + k) - f z) / k) ⤏ df) (at 0)"
    by (rule DERIV_D)
  then have "((λn. (f (z + s n) - f z) / s n) ⇢ df)"
    using LIMSEQ_SEQ_conv1[where a = 0 and l = df] s by blast
  then show ?thesis
    using a by (rule LIMSEQ_unique)
qed
lawrencecpaulson commented 2 years ago

This is a really slick proof, using a theorem (LIMSEQ_SEQ_conv) that relates a limit at a particular point a with a series that converges to that point, so it's about the composition of limits. It would be great if sledgehammer could find proofs like this, and it may even be possible in the foreseeable future. Your proof will appear in the next release. Many thanks!