Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Call for real limit problems


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Email Gateway (Aug 22 2022 at 14:43):

From: David Cock <david.cock@inf.ethz.ch>
Fair enough.

David


Last updated: Mar 28 2024 at 16:17 UTC