Email Gateway (Aug 22 2022 at 14:42): Email Gateway (Aug 22 2022 at 14:42):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
I'm currently working on some more automation for real limits. For that
purpose, I'd like to collect some ‘real-world problems’ from Isabelle users.
I am looking for problems involving the limit of functions of type "real
⇒ real" built from arithmetic (+-*/^), powr, sqrt, root, ln, exp, abs,
min, max as well as sin, cos, tan at finite points. Real parameters
(i.e. free variables of type "real") are also allowed.
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 14:42):From: David Cock <david.cock@inf.ethz.ch>
The pGCL formalisation in the AFP relies on limits in showing the
continuity of expectation transformers. The transformers are built from
linear combinations (*,+), infimum and least fixed point. The
non-recursive cases are in thys/pGCL/Continuity.thy, and the recursive
case (that a loop is equivalent to the limit of its iterates) is in
thys/pGCL/LoopInduction.thy. The proofs are long, but there's nothing
especially funky in there - it's mostly just dancing around not having
the extended reals.
David
Email Gateway (Aug 22 2022 at 14:42):From: Manuel Eberl <eberlm@in.tum.de>
I'm afraid these examples are too abstract. I can only work with
concrete functions, i.e. "the limit of λx::real. max x (exp x) / ln (min
(exp (-x)) (exp (-exp x)))".
Manuel
Email Gateway (Aug 22 2022 at 14:43):From: David Cock <david.cock@inf.ethz.ch>
Fair enough.
David
Last updated: Nov 21 2024 at 12:39 UTC