Mathlib.Dynamics.FixedPoints.Basic

Function.isFixedPt_id theorem

(x : α) : IsFixedPt id x

Full source

/-- Every point is a fixed point of `id`. -/
theorem isFixedPt_id (x : α) : IsFixedPt id x :=
  (rfl :)

Every point is a fixed point of the identity function

Informal description

For any element $x$ in a type $\alpha$, the identity function $\mathrm{id}$ satisfies $\mathrm{id}(x) = x$, meaning every point is a fixed point of the identity function.

Function.forall_isFixedPt_iff theorem

: (∀ x, IsFixedPt f x) ↔ f = id

Full source

/-- A function fixes every point iff it is the identity. -/
@[simp] theorem forall_isFixedPt_iff : (∀ x, IsFixedPt f x) ↔ f = id :=
  ⟨funext, fun h ↦ h ▸ isFixedPt_id⟩

Characterization of the Identity Function via Fixed Points

Informal description

A function $f : \alpha \to \alpha$ satisfies $f(x) = x$ for all $x \in \alpha$ if and only if $f$ is the identity function.

Function.IsFixedPt.decidable instance

[h : DecidableEq α] {f : α → α} {x : α} : Decidable (IsFixedPt f x)

Full source

instance decidable [h : DecidableEq α] {f : α → α} {x : α} : Decidable (IsFixedPt f x) :=
  h (f x) x

Decidability of Fixed Points for Functions on Types with Decidable Equality

Informal description

For any type $\alpha$ with decidable equality, given a function $f : \alpha \to \alpha$ and a point $x \in \alpha$, it is decidable whether $x$ is a fixed point of $f$ (i.e., whether $f(x) = x$).

Function.IsFixedPt.eq theorem

(hf : IsFixedPt f x) : f x = x

Full source

/-- If `x` is a fixed point of `f`, then `f x = x`. This is useful, e.g., for `rw` or `simp`. -/
protected theorem eq (hf : IsFixedPt f x) : f x = x :=
  hf

Fixed Point Property: $f(x) = x$

Informal description

If $x$ is a fixed point of a function $f : \alpha \to \alpha$, then $f(x) = x$.

Function.IsFixedPt.comp theorem

(hf : IsFixedPt f x) (hg : IsFixedPt g x) : IsFixedPt (f ∘ g) x

Full source

/-- If `x` is a fixed point of `f` and `g`, then it is a fixed point of `f ∘ g`. -/
protected theorem comp (hf : IsFixedPt f x) (hg : IsFixedPt g x) : IsFixedPt (f ∘ g) x :=
  calc
    f (g x) = f x := congr_arg f hg
    _ = x := hf

Fixed Point Preservation under Function Composition

Informal description

If $x$ is a fixed point of both functions $f$ and $g$ (i.e., $f(x) = x$ and $g(x) = x$), then $x$ is also a fixed point of their composition $f \circ g$ (i.e., $(f \circ g)(x) = x$).

Function.IsFixedPt.iterate theorem

(hf : IsFixedPt f x) (n : ℕ) : IsFixedPt f^[n] x

Full source

/-- If `x` is a fixed point of `f`, then it is a fixed point of `f^[n]`. -/
protected theorem iterate (hf : IsFixedPt f x) (n : ℕ) : IsFixedPt f^[n] x :=
  iterate_fixed hf n

Fixed Points are Preserved Under Iteration: $f^{[n]}(x) = x$ when $f(x) = x$

Informal description

If $x$ is a fixed point of a function $f \colon \alpha \to \alpha$ (i.e., $f(x) = x$), then for any natural number $n$, the $n$-th iterate $f^{[n]}(x)$ also equals $x$.

Function.IsFixedPt.left_of_comp theorem

(hfg : IsFixedPt (f ∘ g) x) (hg : IsFixedPt g x) : IsFixedPt f x

Full source

/-- If `x` is a fixed point of `f ∘ g` and `g`, then it is a fixed point of `f`. -/
theorem left_of_comp (hfg : IsFixedPt (f ∘ g) x) (hg : IsFixedPt g x) : IsFixedPt f x :=
  calc
    f x = f (g x) := congr_arg f hg.symm
    _ = x := hfg

Fixed point property under composition

Informal description

Let $f$ and $g$ be functions from a type $\alpha$ to itself. If $x$ is a fixed point of the composition $f \circ g$ (i.e., $(f \circ g)(x) = x$) and $x$ is also a fixed point of $g$ (i.e., $g(x) = x$), then $x$ is a fixed point of $f$ (i.e., $f(x) = x$).

Function.IsFixedPt.to_leftInverse theorem

(hf : IsFixedPt f x) (h : LeftInverse g f) : IsFixedPt g x

Full source

/-- If `x` is a fixed point of `f` and `g` is a left inverse of `f`, then `x` is a fixed
point of `g`. -/
theorem to_leftInverse (hf : IsFixedPt f x) (h : LeftInverse g f) : IsFixedPt g x :=
  calc
    g x = g (f x) := congr_arg g hf.symm
    _ = x := h x

Fixed point property under left inverse

Informal description

Let $f : \alpha \to \alpha$ be a function with a fixed point $x \in \alpha$ (i.e., $f(x) = x$). If $g : \alpha \to \alpha$ is a left inverse of $f$ (i.e., $g \circ f = \text{id}$), then $x$ is also a fixed point of $g$ (i.e., $g(x) = x$).

Function.IsFixedPt.map theorem

{x : α} (hx : IsFixedPt fa x) {g : α → β} (h : Semiconj g fa fb) : IsFixedPt fb (g x)

Full source

/-- If `g` (semi)conjugates `fa` to `fb`, then it sends fixed points of `fa` to fixed points
of `fb`. -/
protected theorem map {x : α} (hx : IsFixedPt fa x) {g : α → β} (h : Semiconj g fa fb) :
    IsFixedPt fb (g x) :=
  calc
    fb (g x) = g (fa x) := (h.eq x).symm
    _ = g x := congr_arg g hx

Semiconjugate Functions Preserve Fixed Points

Informal description

Let $f_a : \alpha \to \alpha$ and $f_b : \beta \to \beta$ be functions, and let $g : \alpha \to \beta$ be a function that semiconjugates $f_a$ to $f_b$ (i.e., $g \circ f_a = f_b \circ g$). If $x \in \alpha$ is a fixed point of $f_a$ (i.e., $f_a(x) = x$), then $g(x)$ is a fixed point of $f_b$ (i.e., $f_b(g(x)) = g(x)$).

Function.IsFixedPt.apply theorem

{x : α} (hx : IsFixedPt f x) : IsFixedPt f (f x)

Full source

protected theorem apply {x : α} (hx : IsFixedPt f x) : IsFixedPt f (f x) := by convert hx

Fixed Point Preservation under Function Application

Informal description

If $x$ is a fixed point of a function $f : \alpha \to \alpha$ (i.e., $f(x) = x$), then $f(x)$ is also a fixed point of $f$ (i.e., $f(f(x)) = f(x)$).

Function.IsFixedPt.preimage_iterate theorem

{s : Set α} (h : IsFixedPt (Set.preimage f) s) (n : ℕ) : IsFixedPt (Set.preimage f^[n]) s

Full source

theorem preimage_iterate {s : Set α} (h : IsFixedPt (Set.preimage f) s) (n : ℕ) :
    IsFixedPt (Set.preimage f^[n]) s := by
  rw [Set.preimage_iterate_eq]
  exact h.iterate n

Fixed Points of Preimage Operation are Preserved Under Iteration: $(f^{[n]})^{-1}(s) = s$ when $f^{-1}(s) = s$

Informal description

For any set $s \subseteq \alpha$, if $s$ is a fixed point of the preimage operation under $f$ (i.e., $f^{-1}(s) = s$), then for any natural number $n$, $s$ is also a fixed point of the preimage operation under the $n$-th iterate $f^{[n]}$ (i.e., $(f^{[n]})^{-1}(s) = s$).

Function.IsFixedPt.image_iterate theorem

{s : Set α} (h : IsFixedPt (Set.image f) s) (n : ℕ) : IsFixedPt (Set.image f^[n]) s

Full source

lemma image_iterate {s : Set α} (h : IsFixedPt (Set.image f) s) (n : ℕ) :
    IsFixedPt (Set.image f^[n]) s :=
  Set.image_iterate_eq ▸ h.iterate n

Fixed Points of Image Operation are Preserved Under Iteration: $f^{[n]}(s) = s$ when $f(s) = s$

Informal description

For any set $s \subseteq \alpha$, if $s$ is a fixed point of the image operation under $f$ (i.e., $f(s) = s$), then for any natural number $n$, $s$ is also a fixed point of the image operation under the $n$-th iterate $f^{[n]}$ (i.e., $f^{[n]}(s) = s$).

Function.IsFixedPt.equiv_symm theorem

(h : IsFixedPt e x) : IsFixedPt e.symm x

Full source

protected theorem equiv_symm (h : IsFixedPt e x) : IsFixedPt e.symm x :=
  h.to_leftInverse e.leftInverse_symm

Fixed Points are Preserved Under Equivalence Inverses: $e^{-1}(x) = x$ when $e(x) = x$

Informal description

Let $e : \alpha \simeq \alpha$ be an equivalence (bijection) on a type $\alpha$, and let $x \in \alpha$ be a fixed point of $e$ (i.e., $e(x) = x$). Then $x$ is also a fixed point of the inverse equivalence $e^{-1}$ (i.e., $e^{-1}(x) = x$).

Function.IsFixedPt.perm_inv theorem

(h : IsFixedPt e x) : IsFixedPt (⇑e⁻¹) x

Full source

protected theorem perm_inv (h : IsFixedPt e x) : IsFixedPt (⇑e⁻¹) x :=
  h.equiv_symm

Fixed Points are Preserved Under Permutation Inverses: $e^{-1}(x) = x$ when $e(x) = x$

Informal description

Let $e$ be a permutation of a type $\alpha$ and let $x \in \alpha$ be a fixed point of $e$ (i.e., $e(x) = x$). Then $x$ is also a fixed point of the inverse permutation $e^{-1}$ (i.e., $e^{-1}(x) = x$).

Function.IsFixedPt.perm_pow theorem

(h : IsFixedPt e x) (n : ℕ) : IsFixedPt (⇑(e ^ n)) x

Full source

protected theorem perm_pow (h : IsFixedPt e x) (n : ℕ) : IsFixedPt (⇑(e ^ n)) x := h.iterate _

Fixed Points are Preserved Under Permutation Powers: $e^n(x) = x$ when $e(x) = x$

Informal description

Let $e$ be a permutation of a type $\alpha$ and let $x \in \alpha$ be a fixed point of $e$ (i.e., $e(x) = x$). Then for any natural number $n$, the point $x$ is also a fixed point of the $n$-th power of $e$, i.e., $e^n(x) = x$.

Function.IsFixedPt.perm_zpow theorem

(h : IsFixedPt e x) : ∀ n : ℤ, IsFixedPt (⇑(e ^ n)) x

Full source

protected theorem perm_zpow (h : IsFixedPt e x) : ∀ n : ℤ, IsFixedPt (⇑(e ^ n)) x
  | Int.ofNat _ => h.perm_pow _
  | Int.negSucc n => (h.perm_pow <| n + 1).perm_inv

Fixed Points are Preserved Under Integer Powers of Permutations: $e^n(x) = x$ when $e(x) = x$

Informal description

Let $e$ be a permutation of a type $\alpha$ and let $x \in \alpha$ be a fixed point of $e$ (i.e., $e(x) = x$). Then for any integer $n$, the point $x$ is also a fixed point of the $n$-th power of $e$, i.e., $e^n(x) = x$.

Function.Injective.isFixedPt_apply_iff theorem

(hf : Injective f) {x : α} : IsFixedPt f (f x) ↔ IsFixedPt f x

Full source

@[simp]
theorem Injective.isFixedPt_apply_iff (hf : Injective f) {x : α} :
    IsFixedPtIsFixedPt f (f x) ↔ IsFixedPt f x :=
  ⟨fun h => hf h.eq, IsFixedPt.apply⟩

Fixed Point Criterion for Injective Functions: $f(f(x)) = f(x) \leftrightarrow f(x) = x$

Informal description

For an injective function $f : \alpha \to \alpha$ and any $x \in \alpha$, the point $f(x)$ is a fixed point of $f$ if and only if $x$ is a fixed point of $f$. In other words, $f(f(x)) = f(x) \leftrightarrow f(x) = x$.

Function.fixedPoints definition

(f : α → α) : Set α

Full source

/-- The set of fixed points of a map `f : α → α`. -/
def fixedPoints (f : α → α) : Set α :=
  { x : α | IsFixedPt f x }

Fixed points of a function

Informal description

The set of fixed points of a function $ f : \alpha \to \alpha $ is the collection of all elements $ x \in \alpha $ such that $ f(x) = x $.

Function.fixedPoints.decidable instance

[DecidableEq α] (f : α → α) (x : α) : Decidable (x ∈ fixedPoints f)

Full source

instance fixedPoints.decidable [DecidableEq α] (f : α → α) (x : α) :
    Decidable (x ∈ fixedPoints f) :=
  IsFixedPt.decidable

Decidability of Fixed Points for Functions on Types with Decidable Equality

Informal description

For any type $\alpha$ with decidable equality, given a function $f : \alpha \to \alpha$ and an element $x \in \alpha$, it is decidable whether $x$ is a fixed point of $f$ (i.e., whether $f(x) = x$).

Function.mem_fixedPoints theorem

: x ∈ fixedPoints f ↔ IsFixedPt f x

Full source

@[simp]
theorem mem_fixedPoints : x ∈ fixedPoints fx ∈ fixedPoints f ↔ IsFixedPt f x :=
  Iff.rfl

Characterization of Fixed Points: $x \in \text{fixedPoints}(f) \leftrightarrow f(x) = x$

Informal description

An element $x$ belongs to the set of fixed points of a function $f : \alpha \to \alpha$ if and only if $x$ is a fixed point of $f$, i.e., $f(x) = x$.

Function.mem_fixedPoints_iff theorem

{α : Type*} {f : α → α} {x : α} : x ∈ fixedPoints f ↔ f x = x

Full source

theorem mem_fixedPoints_iff {α : Type*} {f : α → α} {x : α} : x ∈ fixedPoints fx ∈ fixedPoints f ↔ f x = x := by
  rfl

Characterization of Fixed Points: $x \in \text{fixedPoints}(f) \leftrightarrow f(x) = x$

Informal description

For any function $f : \alpha \to \alpha$ and any element $x \in \alpha$, $x$ belongs to the set of fixed points of $f$ if and only if $f(x) = x$.

Function.fixedPoints_id theorem

: fixedPoints (@id α) = Set.univ

Full source

@[simp]
theorem fixedPoints_id : fixedPoints (@id α) = Set.univ :=
  Set.ext fun _ => by simpa using isFixedPt_id _

Fixed Points of Identity Function are Universal Set

Informal description

The set of fixed points of the identity function $\mathrm{id} : \alpha \to \alpha$ is equal to the universal set on $\alpha$, i.e., $\mathrm{fixedPoints}(\mathrm{id}) = \mathrm{univ}$.

Function.fixedPoints_subset_range theorem

: fixedPoints f ⊆ Set.range f

Full source

theorem fixedPoints_subset_range : fixedPointsfixedPoints f ⊆ Set.range f := fun x hx => ⟨x, hx⟩

Fixed Points are Contained in the Range of a Function

Informal description

For any function $f : \alpha \to \alpha$, the set of fixed points of $f$ is a subset of the range of $f$, i.e., $\mathrm{fixedPoints}(f) \subseteq \mathrm{range}(f)$.

Function.Semiconj.mapsTo_fixedPoints theorem

{g : α → β} (h : Semiconj g fa fb) : Set.MapsTo g (fixedPoints fa) (fixedPoints fb)

Full source

/-- If `g` semiconjugates `fa` to `fb`, then it sends fixed points of `fa` to fixed points
of `fb`. -/
theorem Semiconj.mapsTo_fixedPoints {g : α → β} (h : Semiconj g fa fb) :
    Set.MapsTo g (fixedPoints fa) (fixedPoints fb) := fun _ hx => hx.map h

Semiconjugate Functions Preserve Fixed Points

Informal description

If a function $g : \alpha \to \beta$ semiconjugates $f_a : \alpha \to \alpha$ to $f_b : \beta \to \beta$ (i.e., $g \circ f_a = f_b \circ g$), then $g$ maps every fixed point of $f_a$ to a fixed point of $f_b$. In other words, for any $x \in \alpha$ such that $f_a(x) = x$, we have $f_b(g(x)) = g(x)$.

Function.invOn_fixedPoints_comp theorem

(f : α → β) (g : β → α) : Set.InvOn f g (fixedPoints <| f ∘ g) (fixedPoints <| g ∘ f)

Full source

/-- Any two maps `f : α → β` and `g : β → α` are inverse of each other on the sets of fixed points
of `f ∘ g` and `g ∘ f`, respectively. -/
theorem invOn_fixedPoints_comp (f : α → β) (g : β → α) :
    Set.InvOn f g (fixedPoints <| f ∘ g) (fixedPoints <| g ∘ f) :=
  ⟨fun _ => id, fun _ => id⟩

Inverse Property on Fixed Points of Composed Functions

Informal description

For any two functions $f : \alpha \to \beta$ and $g : \beta \to \alpha$, the function $f$ is a left inverse of $g$ on the fixed points of $f \circ g$ (i.e., $f(g(y)) = y$ for all $y \in \text{Fix}(f \circ g)$), and $g$ is a left inverse of $f$ on the fixed points of $g \circ f$ (i.e., $g(f(x)) = x$ for all $x \in \text{Fix}(g \circ f)$).

Function.mapsTo_fixedPoints_comp theorem

(f : α → β) (g : β → α) : Set.MapsTo f (fixedPoints <| g ∘ f) (fixedPoints <| f ∘ g)

Full source

/-- Any map `f` sends fixed points of `g ∘ f` to fixed points of `f ∘ g`. -/
theorem mapsTo_fixedPoints_comp (f : α → β) (g : β → α) :
    Set.MapsTo f (fixedPoints <| g ∘ f) (fixedPoints <| f ∘ g) := fun _ hx => hx.map fun _ => rfl

Fixed Points Mapping under Composition: $f(\text{Fix}(g \circ f)) \subseteq \text{Fix}(f \circ g)$

Informal description

For any functions $f : \alpha \to \beta$ and $g : \beta \to \alpha$, the image under $f$ of the fixed points of $g \circ f$ is contained in the fixed points of $f \circ g$. In other words, if $x$ is a fixed point of $g \circ f$ (i.e., $g(f(x)) = x$), then $f(x)$ is a fixed point of $f \circ g$ (i.e., $f(g(f(x))) = f(x)$).

Function.bijOn_fixedPoints_comp theorem

(f : α → β) (g : β → α) : Set.BijOn g (fixedPoints <| f ∘ g) (fixedPoints <| g ∘ f)

Full source

/-- Given two maps `f : α → β` and `g : β → α`, `g` is a bijective map between the fixed points
of `f ∘ g` and the fixed points of `g ∘ f`. The inverse map is `f`, see `invOn_fixedPoints_comp`. -/
theorem bijOn_fixedPoints_comp (f : α → β) (g : β → α) :
    Set.BijOn g (fixedPoints <| f ∘ g) (fixedPoints <| g ∘ f) :=
  (invOn_fixedPoints_comp f g).bijOn (mapsTo_fixedPoints_comp g f) (mapsTo_fixedPoints_comp f g)

Bijection Between Fixed Points of Composed Functions: $g \colon \text{Fix}(f \circ g) \leftrightarrow \text{Fix}(g \circ f)$

Informal description

For any functions $f \colon \alpha \to \beta$ and $g \colon \beta \to \alpha$, the function $g$ is a bijection between the fixed points of $f \circ g$ and the fixed points of $g \circ f$. Specifically, $g$ maps the set $\{y \in \beta \mid f(g(y)) = y\}$ bijectively onto the set $\{x \in \alpha \mid g(f(x)) = x\}$.

Function.Commute.invOn_fixedPoints_comp theorem

(h : Commute f g) : Set.InvOn f g (fixedPoints <| f ∘ g) (fixedPoints <| f ∘ g)

Full source

/-- If self-maps `f` and `g` commute, then they are inverse of each other on the set of fixed points
of `f ∘ g`. This is a particular case of `Function.invOn_fixedPoints_comp`. -/
theorem Commute.invOn_fixedPoints_comp (h : Commute f g) :
    Set.InvOn f g (fixedPoints <| f ∘ g) (fixedPoints <| f ∘ g) := by
  simpa only [h.comp_eq] using Function.invOn_fixedPoints_comp f g

Inverse Property on Fixed Points for Commuting Functions

Informal description

If two self-maps $f, g : \alpha \to \alpha$ commute (i.e., $f \circ g = g \circ f$), then they are inverses of each other on the set of fixed points of $f \circ g$. That is, for all $x$ in the fixed points of $f \circ g$, we have $f(g(x)) = x$ and $g(f(x)) = x$.

Function.Commute.left_bijOn_fixedPoints_comp theorem

(h : Commute f g) : Set.BijOn f (fixedPoints <| f ∘ g) (fixedPoints <| f ∘ g)

Full source

/-- If self-maps `f` and `g` commute, then `f` is bijective on the set of fixed points of `f ∘ g`.
This is a particular case of `Function.bijOn_fixedPoints_comp`. -/
theorem Commute.left_bijOn_fixedPoints_comp (h : Commute f g) :
    Set.BijOn f (fixedPoints <| f ∘ g) (fixedPoints <| f ∘ g) := by
  simpa only [h.comp_eq] using bijOn_fixedPoints_comp g f

Bijectivity of $f$ on Fixed Points of $f \circ g$ for Commuting $f$ and $g$

Informal description

If two self-maps $f, g \colon \alpha \to \alpha$ commute (i.e., $f \circ g = g \circ f$), then $f$ is bijective on the set of fixed points of $f \circ g$. That is, $f$ restricts to a bijection from $\{x \in \alpha \mid f(g(x)) = x\}$ to itself.

Function.Commute.right_bijOn_fixedPoints_comp theorem

(h : Commute f g) : Set.BijOn g (fixedPoints <| f ∘ g) (fixedPoints <| f ∘ g)

Full source

/-- If self-maps `f` and `g` commute, then `g` is bijective on the set of fixed points of `f ∘ g`.
This is a particular case of `Function.bijOn_fixedPoints_comp`. -/
theorem Commute.right_bijOn_fixedPoints_comp (h : Commute f g) :
    Set.BijOn g (fixedPoints <| f ∘ g) (fixedPoints <| f ∘ g) := by
  simpa only [h.comp_eq] using bijOn_fixedPoints_comp f g

Bijectivity of $g$ on Fixed Points of Commuting $f \circ g$

Informal description

If two self-maps $f, g \colon \alpha \to \alpha$ commute (i.e., $f \circ g = g \circ f$), then $g$ is bijective from the set of fixed points of $f \circ g$ to itself. That is, $g$ maps $\{x \in \alpha \mid f(g(x)) = x\}$ bijectively onto itself.

Tags