Email Gateway (Aug 19 2022 at 08:01): Email Gateway (Aug 19 2022 at 08:01):From: Mark Wassell <mpwassell@gmail.com>
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?
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.
Cheers
Mark
Email Gateway (Aug 19 2022 at 08:01):From: Brian Huffman <huffman@in.tum.de>
On Sun, Jul 29, 2012 at 7:04 PM, Mark Wassell <mpwassell@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 likedist (X * (∑n = 0..n. fps_const (f $ n) * X ^ n)) (X * f) < r ==> dist
((∑n = 0..n. fps_const (f $ n) * X ^ n)) f < r2where 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.
Last updated: Apr 18 2024 at 20:16 UTC