mathlib3 documentation

dynamics.fixed_points.basic

Fixed points of a self-map #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define

We also prove some simple lemmas about is_fixed_pt and ∘, iterate, and semiconj.

Tags #

fixed point

source
def function.is_fixed_pt {α : Type u} (f : α → α) (x : α) :
Prop

A point x is a fixed point of f : α → α if f x = x.

Equations
Instances for function.is_fixed_pt
source
theorem function.is_fixed_pt_id {α : Type u} (x : α) :
function.is_fixed_pt id x

Every point is a fixed point of id.

source
@[protected, instance]
def function.is_fixed_pt.decidable {α : Type u} [h : decidable_eq α] {f : α → α} {x : α} :
decidable (function.is_fixed_pt f x)
Equations
source
@[protected]
theorem function.is_fixed_pt.eq {α : Type u} {f : α → α} {x : α} (hf : function.is_fixed_pt f x) :
f x = x

If x is a fixed point of f, then f x = x. This is useful, e.g., for rw or simp.

source
@[protected]
theorem function.is_fixed_pt.comp {α : Type u} {f g : α → α} {x : α} (hf : function.is_fixed_pt f x) (hg : function.is_fixed_pt g x) :
function.is_fixed_pt (f ∘ g) x

If x is a fixed point of f and g, then it is a fixed point of f ∘ g.

source
@[protected]
theorem function.is_fixed_pt.iterate {α : Type u} {f : α → α} {x : α} (hf : function.is_fixed_pt f x) (n : ℕ) :
function.is_fixed_pt f^[n] x

If x is a fixed point of f, then it is a fixed point of f^[n].

source
theorem function.is_fixed_pt.left_of_comp {α : Type u} {f g : α → α} {x : α} (hfg : function.is_fixed_pt (f ∘ g) x) (hg : function.is_fixed_pt g x) :
function.is_fixed_pt f x

If x is a fixed point of f ∘ g and g, then it is a fixed point of f.

source
theorem function.is_fixed_pt.to_left_inverse {α : Type u} {f g : α → α} {x : α} (hf : function.is_fixed_pt f x) (h : function.left_inverse g f) :
function.is_fixed_pt g x

If x is a fixed point of f and g is a left inverse of f, then x is a fixed point of g.

source
@[protected]
theorem function.is_fixed_pt.map {α : Type u} {β : Type v} {fa : α → α} {fb : β → β} {x : α} (hx : function.is_fixed_pt fa x) {g : α → β} (h : function.semiconj g fa fb) :
function.is_fixed_pt fb (g x)

If g (semi)conjugates fa to fb, then it sends fixed points of fa to fixed points of fb.

source
@[protected]
theorem function.is_fixed_pt.apply {α : Type u} {f : α → α} {x : α} (hx : function.is_fixed_pt f x) :
function.is_fixed_pt f (f x)
source
theorem function.is_fixed_pt.preimage_iterate {α : Type u} {f : α → α} {s : set α} (h : function.is_fixed_pt (set.preimage f) s) (n : ℕ) :
function.is_fixed_pt (set.preimage f^[n]) s
source
@[protected]
theorem function.is_fixed_pt.equiv_symm {α : Type u} {x : α} {e : equiv.perm α} (h : function.is_fixed_pt ⇑e x) :
function.is_fixed_pt ⇑(equiv.symm e) x
source
@[protected]
theorem function.is_fixed_pt.perm_inv {α : Type u} {x : α} {e : equiv.perm α} (h : function.is_fixed_pt ⇑e x) :
function.is_fixed_pt ⇑e⁻¹ x
source
@[protected]
theorem function.is_fixed_pt.perm_pow {α : Type u} {x : α} {e : equiv.perm α} (h : function.is_fixed_pt ⇑e x) (n : ℕ) :
function.is_fixed_pt ⇑(e ^ n) x
source
@[protected]
theorem function.is_fixed_pt.perm_zpow {α : Type u} {x : α} {e : equiv.perm α} (h : function.is_fixed_pt ⇑e x) (n : ℤ) :
function.is_fixed_pt ⇑(e ^ n) x
source
@[simp]
theorem function.injective.is_fixed_pt_apply_iff {α : Type u} {f : α → α} (hf : function.injective f) {x : α} :
function.is_fixed_pt f (f x) ↔ function.is_fixed_pt f x
source
def function.fixed_points {α : Type u} (f : α → α) :
set α

The set of fixed points of a map f : α → α.

Equations
Instances for ↥function.fixed_points
source
@[protected, instance]
def function.fixed_points.decidable {α : Type u} [decidable_eq α] (f : α → α) (x : α) :
decidable (x ∈ function.fixed_points f)
Equations
source
@[simp]
theorem function.mem_fixed_points {α : Type u} {f : α → α} {x : α} :
x ∈ function.fixed_points f ↔ function.is_fixed_pt f x
source
theorem function.mem_fixed_points_iff {α : Type u_1} {f : α → α} {x : α} :
x ∈ function.fixed_points f ↔ f x = x
source
@[simp]
theorem function.fixed_points_id {α : Type u} :
function.fixed_points id = set.univ
source
theorem function.fixed_points_subset_range {α : Type u} {f : α → α} :
function.fixed_points f ⊆ set.range f
source
theorem function.semiconj.maps_to_fixed_pts {α : Type u} {β : Type v} {fa : α → α} {fb : β → β} {g : α → β} (h : function.semiconj g fa fb) :
set.maps_to g (function.fixed_points fa) (function.fixed_points fb)

If g semiconjugates fa to fb, then it sends fixed points of fa to fixed points of fb.

source
theorem function.inv_on_fixed_pts_comp {α : Type u} {β : Type v} (f : α → β) (g : β → α) :
set.inv_on f g (function.fixed_points (f ∘ g)) (function.fixed_points (g ∘ f))

Any two maps f : α → β and g : β → α are inverse of each other on the sets of fixed points of f ∘ g and g ∘ f, respectively.

source
theorem function.maps_to_fixed_pts_comp {α : Type u} {β : Type v} (f : α → β) (g : β → α) :
set.maps_to f (function.fixed_points (g ∘ f)) (function.fixed_points (f ∘ g))

Any map f sends fixed points of g ∘ f to fixed points of f ∘ g.

source
theorem function.bij_on_fixed_pts_comp {α : Type u} {β : Type v} (f : α → β) (g : β → α) :
set.bij_on g (function.fixed_points (f ∘ g)) (function.fixed_points (g ∘ f))

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 inv_on_fixed_pts_comp.

source
theorem function.commute.inv_on_fixed_pts_comp {α : Type u} {f g : α → α} (h : function.commute f g) :
set.inv_on f g (function.fixed_points (f ∘ g)) (function.fixed_points (f ∘ g))

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.inv_on_fixed_pts_comp.

source
theorem function.commute.left_bij_on_fixed_pts_comp {α : Type u} {f g : α → α} (h : function.commute f g) :
set.bij_on f (function.fixed_points (f ∘ g)) (function.fixed_points (f ∘ g))

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.bij_on_fixed_pts_comp.

source
theorem function.commute.right_bij_on_fixed_pts_comp {α : Type u} {f g : α → α} (h : function.commute f g) :
set.bij_on g (function.fixed_points (f ∘ g)) (function.fixed_points (f ∘ g))

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.bij_on_fixed_pts_comp.