Fixed point

Stream: Is there code for X?

[Patrick Johnson]

Do we have these?

def get_some {α : Type} [inhabited α] (P : α → Prop) : α :=
if h : ∃ (x : α), P x then h.some else default

def fixed {α : Type} [inhabited α] (f : α → α) (z : α) : α :=
get_some (λ (x : α), ∃ (n : ℕ), (f^[n]) z = x ∧ (f^[n + 1]) z = x)

[Floris van Doorn]

get_some is basically docs#classical.epsilon.

[Floris van Doorn]

I don't think the second definition exists, but there are some related notions in file#dynamics/fixed_points/basic.

[Patrick Johnson]

Ok then, I'd like to add the following two defs to function.iterate

def function.iterate_tendsto {α : Type*} (f : α → α) (z x : α) : Prop :=
∃ (n : ℕ), (f^[n]) z = x ∧ (f^[n + 1]) z = x

def function.iterate_limit {α : Type*} [inhabited α] (f : α → α) (z : α) : α :=
classical.epsilon (function.iterate_tendsto f z)

because I feel like they are useful, but apparently missing in mathlib. I would also prove few lemmas about them. Should I rename them to something else (or put them in dynamics/fixed_points instead)? Or is there any reason we don't want them in mathlib?

[Patrick Johnson]

An example usage is the digital root of a natural number.

[Eric Wieser]

For the digital root I would assume you could just use well-founded recursion