# Re: [isabelle] Using Formal_Power_Series.thy

```On Sun, Jul 29, 2012 at 7:04 PM, Mark Wassell <mpwassell at gmail.com> wrote:
> Hello,
>
> Based on Formal_Power_Series.thy (
> http://www.cl.cam.ac.uk/research/hvg/isabelle/dist/library/HOL/HOL-Library/Formal_Power_Series.html),
> I need to prove:
>
> lemma "((%k . X * (setsum (λ n. (fps_const (f\$n)) * (X^n)) {0..(k::nat)})))
> ---->  X * f"
>
> which of course is like fps_notation but with a factor of X.
>
> It would seem however that dist_fps_def doesn't have the right properties
> for me to pull out the X. I think I would need to have something like
>
> dist (X * (∑n = 0..n. fps_const (f \$ n) * X ^ n)) (X * f) < r   ==> dist
> ((∑n = 0..n. fps_const (f \$ n) * X ^ n))   f < r2
>
> where r  = r2 * X  i.e. dist has norm like properties and not just those of
> a metric space.
>
> Is there anyway to prove what I need to prove?

Hi Mark,

I was able to prove your lemma without too much trouble; there is no
problem with the definition of dist.

You might want to prove the following two lemmas, which I used in my proof:

lemma "0 < (r::real) ==> EX n. inverse (2 ^ n) < r"
lemma "ALL n<k. x \$ n = y \$ n ==> dist x y <= inverse (2 ^ k)"

> By the way, what I am really after is
>
> lemma "(X * (setsum (λ n. (fps_const (f\$n)) * (X^n)) {0..})) = X * f"
>
> but the definition of setsum gives 0 for sums over non-finite sets.

Instead of setsum, you probably want to use "suminf", which is defined
in Series.thy.

- Brian

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.