Documentation

Mathlib.Dynamics.FixedPoints.Basic

Fixed points of a self-map #

In this file we define

We also prove some simple lemmas about IsFixedPt and ∘, iterate, and Semiconj.

Tags #

fixed point

source
def Function.IsFixedPt {α : Type u} (f : α → α) (x : α) :
Prop

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

Equations
Instances For
    source
    theorem Function.isFixedPt_id {α : Type u} (x : α) :
    Function.IsFixedPt id x

    Every point is a fixed point of id.

    source
    instance Function.IsFixedPt.decidable {α : Type u} [h : DecidableEq α] {f : α → α} {x : α} :
    Decidable (Function.IsFixedPt f x)
    Equations
    • Function.IsFixedPt.decidable = h (f x) x
    source
    theorem Function.IsFixedPt.eq {α : Type u} {f : α → α} {x : α} (hf : Function.IsFixedPt 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
    theorem Function.IsFixedPt.comp {α : Type u} {f : α → α} {g : α → α} {x : α} (hf : Function.IsFixedPt f x) (hg : Function.IsFixedPt g x) :
    Function.IsFixedPt (f ∘ g) x

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

    source
    theorem Function.IsFixedPt.iterate {α : Type u} {f : α → α} {x : α} (hf : Function.IsFixedPt f x) (n : ℕ) :
    Function.IsFixedPt f^[n] x

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

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

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

    source
    theorem Function.IsFixedPt.to_leftInverse {α : Type u} {f : α → α} {g : α → α} {x : α} (hf : Function.IsFixedPt f x) (h : Function.LeftInverse g f) :
    Function.IsFixedPt 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
    theorem Function.IsFixedPt.map {α : Type u} {β : Type v} {fa : α → α} {fb : β → β} {x : α} (hx : Function.IsFixedPt fa x) {g : α → β} (h : Function.Semiconj g fa fb) :
    Function.IsFixedPt fb (g x)

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

    source
    theorem Function.IsFixedPt.apply {α : Type u} {f : α → α} {x : α} (hx : Function.IsFixedPt f x) :
    Function.IsFixedPt f (f x)
    source
    theorem Function.IsFixedPt.preimage_iterate {α : Type u} {f : α → α} {s : Set α} (h : Function.IsFixedPt (Set.preimage f) s) (n : ℕ) :
    Function.IsFixedPt (Set.preimage f^[n]) s
    source
    theorem Function.IsFixedPt.image_iterate {α : Type u} {f : α → α} {s : Set α} (h : Function.IsFixedPt (Set.image f) s) (n : ℕ) :
    Function.IsFixedPt (Set.image f^[n]) s
    source
    theorem Function.IsFixedPt.equiv_symm {α : Type u} {x : α} {e : Equiv.Perm α} (h : Function.IsFixedPt (⇑e) x) :
    Function.IsFixedPt (⇑e.symm) x
    source
    theorem Function.IsFixedPt.perm_inv {α : Type u} {x : α} {e : Equiv.Perm α} (h : Function.IsFixedPt (⇑e) x) :
    Function.IsFixedPt (⇑e⁻¹) x
    source
    theorem Function.IsFixedPt.perm_pow {α : Type u} {x : α} {e : Equiv.Perm α} (h : Function.IsFixedPt (⇑e) x) (n : ℕ) :
    Function.IsFixedPt (⇑(e ^ n)) x
    source
    theorem Function.IsFixedPt.perm_zpow {α : Type u} {x : α} {e : Equiv.Perm α} (h : Function.IsFixedPt (⇑e) x) (n : ℤ) :
    Function.IsFixedPt (⇑(e ^ n)) x
    source
    @[simp]
    theorem Function.Injective.isFixedPt_apply_iff {α : Type u} {f : α → α} (hf : Function.Injective f) {x : α} :
    Function.IsFixedPt f (f x) ↔ Function.IsFixedPt f x
    source
    def Function.fixedPoints {α : Type u} (f : α → α) :
    Set α

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

    Equations
    Instances For
      source
      instance Function.fixedPoints.decidable {α : Type u} [DecidableEq α] (f : α → α) (x : α) :
      Decidable (x ∈ Function.fixedPoints f)
      Equations
      source
      @[simp]
      theorem Function.mem_fixedPoints {α : Type u} {f : α → α} {x : α} :
      x ∈ Function.fixedPoints f ↔ Function.IsFixedPt f x
      source
      theorem Function.mem_fixedPoints_iff {α : Type u_1} {f : α → α} {x : α} :
      x ∈ Function.fixedPoints f ↔ f x = x
      source
      @[simp]
      theorem Function.fixedPoints_id {α : Type u} :
      Function.fixedPoints id = Set.univ
      source
      theorem Function.fixedPoints_subset_range {α : Type u} {f : α → α} :
      Function.fixedPoints f ⊆ Set.range f
      source
      theorem Function.Semiconj.mapsTo_fixedPoints {α : Type u} {β : Type v} {fa : α → α} {fb : β → β} {g : α → β} (h : Function.Semiconj g fa fb) :
      Set.MapsTo g (Function.fixedPoints fa) (Function.fixedPoints fb)

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

      source
      theorem Function.invOn_fixedPoints_comp {α : Type u} {β : Type v} (f : α → β) (g : β → α) :
      Set.InvOn f g (Function.fixedPoints (f ∘ g)) (Function.fixedPoints (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.mapsTo_fixedPoints_comp {α : Type u} {β : Type v} (f : α → β) (g : β → α) :
      Set.MapsTo f (Function.fixedPoints (g ∘ f)) (Function.fixedPoints (f ∘ g))

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

      source
      theorem Function.bijOn_fixedPoints_comp {α : Type u} {β : Type v} (f : α → β) (g : β → α) :
      Set.BijOn g (Function.fixedPoints (f ∘ g)) (Function.fixedPoints (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 invOn_fixedPoints_comp.

      source
      theorem Function.Commute.invOn_fixedPoints_comp {α : Type u} {f : α → α} {g : α → α} (h : Function.Commute f g) :
      Set.InvOn f g (Function.fixedPoints (f ∘ g)) (Function.fixedPoints (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.invOn_fixedPoints_comp.

      source
      theorem Function.Commute.left_bijOn_fixedPoints_comp {α : Type u} {f : α → α} {g : α → α} (h : Function.Commute f g) :
      Set.BijOn f (Function.fixedPoints (f ∘ g)) (Function.fixedPoints (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.bijOn_fixedPoints_comp.

      source
      theorem Function.Commute.right_bijOn_fixedPoints_comp {α : Type u} {f : α → α} {g : α → α} (h : Function.Commute f g) :
      Set.BijOn g (Function.fixedPoints (f ∘ g)) (Function.fixedPoints (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.bijOn_fixedPoints_comp.