Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Degree of an almost everywhere constant function

view this post on Zulip Email Gateway (Oct 15 2020 at 14:42):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,

in certain applications (most prominently polynomials) almost everywhere
constant functions nat => 'a play a critical role, and any almost
everywhere constant function can be assigned a degree, i. e. the highest
n such that for any higher n the function is constant.

Is there any stand-alone formalizsation of this concept?

Cheers,
Florian
signature.asc

view this post on Zulip Email Gateway (Oct 15 2020 at 14:47):

From: Manuel Eberl <eberlm@in.tum.de>
The only thing I am aware of is HOL-Library.Poly_Mapping, which you are
probably aware of, seeing as it has your name at the top.

Manuel
signature.asc

Last updated: Jan 04 2025 at 20:18 UTC