Documentation

Mathlib.Dynamics.PeriodicPts

Periodic points #

A point x : α is a periodic point of f : α → α of period n if f^[n] x = x.

Main definitions #

Main statements #

We provide “dot syntax”-style operations on terms of the form h : IsPeriodicPt f n x including arithmetic operations on n and h.map (hg : SemiconjBy g f f'). We also prove that f is bijective on each set ptsOfPeriod f n and on periodicPts f. Finally, we prove that x is a periodic point of f of period n if and only if minimalPeriod f x | n.

References #

def Function.IsPeriodicPt {α : Type u_1} (f : αα) (n : ) (x : α) :

A point x is a periodic point of f : α → α of period n if f^[n] x = x. Note that we do not require 0 < n in this definition. Many theorems about periodic points need this assumption.

Equations
Instances For
    theorem Function.IsFixedPt.isPeriodicPt {α : Type u_1} {f : αα} {x : α} (hf : Function.IsFixedPt f x) (n : ) :

    A fixed point of f is a periodic point of f of any prescribed period.

    theorem Function.is_periodic_id {α : Type u_1} (n : ) (x : α) :

    For the identity map, all points are periodic.

    theorem Function.isPeriodicPt_zero {α : Type u_1} (f : αα) (x : α) :

    Any point is a periodic point of period 0.

    instance Function.IsPeriodicPt.instDecidableOfDecidableEq {α : Type u_1} [DecidableEq α] {f : αα} {n : } {x : α} :
    Equations
    • Function.IsPeriodicPt.instDecidableOfDecidableEq = Function.IsFixedPt.decidable
    theorem Function.IsPeriodicPt.isFixedPt {α : Type u_1} {f : αα} {x : α} {n : } (hf : Function.IsPeriodicPt f n x) :
    theorem Function.IsPeriodicPt.map {α : Type u_1} {β : Type u_2} {fa : αα} {fb : ββ} {x : α} {n : } (hx : Function.IsPeriodicPt fa n x) {g : αβ} (hg : Function.Semiconj g fa fb) :
    theorem Function.IsPeriodicPt.apply_iterate {α : Type u_1} {f : αα} {x : α} {n : } (hx : Function.IsPeriodicPt f n x) (m : ) :
    theorem Function.IsPeriodicPt.apply {α : Type u_1} {f : αα} {x : α} {n : } (hx : Function.IsPeriodicPt f n x) :
    theorem Function.IsPeriodicPt.add {α : Type u_1} {f : αα} {x : α} {m : } {n : } (hn : Function.IsPeriodicPt f n x) (hm : Function.IsPeriodicPt f m x) :
    theorem Function.IsPeriodicPt.left_of_add {α : Type u_1} {f : αα} {x : α} {m : } {n : } (hn : Function.IsPeriodicPt f (n + m) x) (hm : Function.IsPeriodicPt f m x) :
    theorem Function.IsPeriodicPt.right_of_add {α : Type u_1} {f : αα} {x : α} {m : } {n : } (hn : Function.IsPeriodicPt f (n + m) x) (hm : Function.IsPeriodicPt f n x) :
    theorem Function.IsPeriodicPt.sub {α : Type u_1} {f : αα} {x : α} {m : } {n : } (hm : Function.IsPeriodicPt f m x) (hn : Function.IsPeriodicPt f n x) :
    theorem Function.IsPeriodicPt.mul_const {α : Type u_1} {f : αα} {x : α} {m : } (hm : Function.IsPeriodicPt f m x) (n : ) :
    theorem Function.IsPeriodicPt.const_mul {α : Type u_1} {f : αα} {x : α} {m : } (hm : Function.IsPeriodicPt f m x) (n : ) :
    theorem Function.IsPeriodicPt.trans_dvd {α : Type u_1} {f : αα} {x : α} {m : } (hm : Function.IsPeriodicPt f m x) {n : } (hn : m n) :
    theorem Function.IsPeriodicPt.iterate {α : Type u_1} {f : αα} {x : α} {n : } (hf : Function.IsPeriodicPt f n x) (m : ) :
    theorem Function.IsPeriodicPt.comp {α : Type u_1} {f : αα} {x : α} {n : } {g : αα} (hco : Function.Commute f g) (hf : Function.IsPeriodicPt f n x) (hg : Function.IsPeriodicPt g n x) :
    theorem Function.IsPeriodicPt.comp_lcm {α : Type u_1} {f : αα} {x : α} {m : } {n : } {g : αα} (hco : Function.Commute f g) (hf : Function.IsPeriodicPt f m x) (hg : Function.IsPeriodicPt g n x) :
    Function.IsPeriodicPt (f g) (m.lcm n) x
    theorem Function.IsPeriodicPt.left_of_comp {α : Type u_1} {f : αα} {x : α} {n : } {g : αα} (hco : Function.Commute f g) (hfg : Function.IsPeriodicPt (f g) n x) (hg : Function.IsPeriodicPt g n x) :
    theorem Function.IsPeriodicPt.iterate_mod_apply {α : Type u_1} {f : αα} {x : α} {n : } (h : Function.IsPeriodicPt f n x) (m : ) :
    f^[m % n] x = f^[m] x
    theorem Function.IsPeriodicPt.mod {α : Type u_1} {f : αα} {x : α} {m : } {n : } (hm : Function.IsPeriodicPt f m x) (hn : Function.IsPeriodicPt f n x) :
    theorem Function.IsPeriodicPt.gcd {α : Type u_1} {f : αα} {x : α} {m : } {n : } (hm : Function.IsPeriodicPt f m x) (hn : Function.IsPeriodicPt f n x) :
    Function.IsPeriodicPt f (m.gcd n) x
    theorem Function.IsPeriodicPt.eq_of_apply_eq_same {α : Type u_1} {f : αα} {x : α} {y : α} {n : } (hx : Function.IsPeriodicPt f n x) (hy : Function.IsPeriodicPt f n y) (hn : 0 < n) (h : f x = f y) :
    x = y

    If f sends two periodic points x and y of the same positive period to the same point, then x = y. For a similar statement about points of different periods see eq_of_apply_eq.

    theorem Function.IsPeriodicPt.eq_of_apply_eq {α : Type u_1} {f : αα} {x : α} {y : α} {m : } {n : } (hx : Function.IsPeriodicPt f m x) (hy : Function.IsPeriodicPt f n y) (hm : 0 < m) (hn : 0 < n) (h : f x = f y) :
    x = y

    If f sends two periodic points x and y of positive periods to the same point, then x = y.

    def Function.ptsOfPeriod {α : Type u_1} (f : αα) (n : ) :
    Set α

    The set of periodic points of a given (possibly non-minimal) period.

    Equations
    Instances For
      @[simp]
      theorem Function.mem_ptsOfPeriod {α : Type u_1} {f : αα} {x : α} {n : } :
      theorem Function.Semiconj.mapsTo_ptsOfPeriod {α : Type u_1} {β : Type u_2} {fa : αα} {fb : ββ} {g : αβ} (h : Function.Semiconj g fa fb) (n : ) :
      theorem Function.bijOn_ptsOfPeriod {α : Type u_1} (f : αα) {n : } (hn : 0 < n) :
      theorem Function.directed_ptsOfPeriod_pNat {α : Type u_1} (f : αα) :
      Directed (fun (x1 x2 : Set α) => x1 x2) fun (n : ℕ+) => Function.ptsOfPeriod f n
      def Function.periodicPts {α : Type u_1} (f : αα) :
      Set α

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

      Equations
      Instances For
        theorem Function.mk_mem_periodicPts {α : Type u_1} {f : αα} {x : α} {n : } (hn : 0 < n) (hx : Function.IsPeriodicPt f n x) :
        theorem Function.mem_periodicPts {α : Type u_1} {f : αα} {x : α} :
        theorem Function.isPeriodicPt_of_mem_periodicPts_of_isPeriodicPt_iterate {α : Type u_1} {f : αα} {x : α} {m : } {n : } (hx : x Function.periodicPts f) (hm : Function.IsPeriodicPt f m (f^[n] x)) :
        theorem Function.bUnion_ptsOfPeriod {α : Type u_1} (f : αα) :
        ⋃ (n : ), ⋃ (_ : n > 0), Function.ptsOfPeriod f n = Function.periodicPts f
        theorem Function.iUnion_pNat_ptsOfPeriod {α : Type u_1} (f : αα) :
        theorem Function.Semiconj.mapsTo_periodicPts {α : Type u_1} {β : Type u_2} {fa : αα} {fb : ββ} {g : αβ} (h : Function.Semiconj g fa fb) :
        def Function.minimalPeriod {α : Type u_1} (f : αα) (x : α) :

        Minimal period of a point x under an endomorphism f. If x is not a periodic point of f, then minimalPeriod f x = 0.

        Equations
        Instances For
          @[simp]
          theorem Function.iterate_minimalPeriod {α : Type u_1} {f : αα} {x : α} :
          @[simp]
          theorem Function.iterate_add_minimalPeriod_eq {α : Type u_1} {f : αα} {x : α} {n : } :
          @[simp]
          theorem Function.iterate_mod_minimalPeriod_eq {α : Type u_1} {f : αα} {x : α} {n : } :
          theorem Function.minimalPeriod_eq_zero_of_nmem_periodicPts {α : Type u_1} {f : αα} {x : α} (hx : xFunction.periodicPts f) :
          theorem Function.IsPeriodicPt.minimalPeriod_pos {α : Type u_1} {f : αα} {x : α} {n : } (hn : 0 < n) (hx : Function.IsPeriodicPt f n x) :
          theorem Function.IsPeriodicPt.minimalPeriod_le {α : Type u_1} {f : αα} {x : α} {n : } (hn : 0 < n) (hx : Function.IsPeriodicPt f n x) :
          theorem Function.minimalPeriod_apply_iterate {α : Type u_1} {f : αα} {x : α} (hx : x Function.periodicPts f) (n : ) :
          theorem Function.minimalPeriod_apply {α : Type u_1} {f : αα} {x : α} (hx : x Function.periodicPts f) :
          theorem Function.le_of_lt_minimalPeriod_of_iterate_eq {α : Type u_1} {f : αα} {x : α} {m : } {n : } (hm : m < Function.minimalPeriod f x) (hmn : f^[m] x = f^[n] x) :
          m n
          theorem Function.iterate_injOn_Iio_minimalPeriod {α : Type u_1} {f : αα} {x : α} :
          Set.InjOn (fun (x_1 : ) => f^[x_1] x) (Set.Iio (Function.minimalPeriod f x))
          theorem Function.iterate_eq_iterate_iff_of_lt_minimalPeriod {α : Type u_1} {f : αα} {x : α} {m : } {n : } (hm : m < Function.minimalPeriod f x) (hn : n < Function.minimalPeriod f x) :
          f^[m] x = f^[n] x m = n
          @[simp]
          theorem Function.minimalPeriod_id {α : Type u_1} {x : α} :
          theorem Function.IsPeriodicPt.eq_zero_of_lt_minimalPeriod {α : Type u_1} {f : αα} {x : α} {n : } (hx : Function.IsPeriodicPt f n x) (hn : n < Function.minimalPeriod f x) :
          n = 0
          theorem Function.not_isPeriodicPt_of_pos_of_lt_minimalPeriod {α : Type u_1} {f : αα} {x : α} {n : } :
          theorem Function.IsPeriodicPt.minimalPeriod_dvd {α : Type u_1} {f : αα} {x : α} {n : } (hx : Function.IsPeriodicPt f n x) :
          theorem Function.minimalPeriod_eq_minimalPeriod_iff {α : Type u_1} {β : Type u_2} {f : αα} {x : α} {g : ββ} {y : β} :
          theorem Function.minimalPeriod_eq_prime {α : Type u_1} {f : αα} {x : α} {p : } [hp : Fact (Nat.Prime p)] (hper : Function.IsPeriodicPt f p x) (hfix : ¬Function.IsFixedPt f x) :
          theorem Function.minimalPeriod_eq_prime_pow {α : Type u_1} {f : αα} {x : α} {p : } {k : } [hp : Fact (Nat.Prime p)] (hk : ¬Function.IsPeriodicPt f (p ^ k) x) (hk1 : Function.IsPeriodicPt f (p ^ (k + 1)) x) :
          theorem Function.Commute.minimalPeriod_of_comp_dvd_lcm {α : Type u_1} {f : αα} {x : α} {g : αα} (h : Function.Commute f g) :
          theorem Function.minimalPeriod_iterate_eq_div_gcd {α : Type u_1} {f : αα} {x : α} {n : } (h : n 0) :
          def Function.periodicOrbit {α : Type u_1} (f : αα) (x : α) :

          The orbit of a periodic point x of f is the cycle [x, f x, f (f x), ...]. Its length is the minimal period of x.

          If x is not a periodic point, then this is the empty (aka nil) cycle.

          Equations
          Instances For
            theorem Function.periodicOrbit_def {α : Type u_1} (f : αα) (x : α) :

            The definition of a periodic orbit, in terms of List.map.

            theorem Function.periodicOrbit_eq_cycle_map {α : Type u_1} (f : αα) (x : α) :

            The definition of a periodic orbit, in terms of Cycle.map.

            @[simp]
            theorem Function.periodicOrbit_length {α : Type u_1} {f : αα} {x : α} :
            @[simp]
            theorem Function.periodicOrbit_eq_nil_iff_not_periodic_pt {α : Type u_1} {f : αα} {x : α} :
            theorem Function.periodicOrbit_eq_nil_of_not_periodic_pt {α : Type u_1} {f : αα} {x : α} (h : xFunction.periodicPts f) :
            @[simp]
            theorem Function.mem_periodicOrbit_iff {α : Type u_1} {f : αα} {x : α} {y : α} (hx : x Function.periodicPts f) :
            y Function.periodicOrbit f x ∃ (n : ), f^[n] x = y
            @[simp]
            theorem Function.iterate_mem_periodicOrbit {α : Type u_1} {f : αα} {x : α} (hx : x Function.periodicPts f) (n : ) :
            @[simp]
            theorem Function.self_mem_periodicOrbit {α : Type u_1} {f : αα} {x : α} (hx : x Function.periodicPts f) :
            theorem Function.nodup_periodicOrbit {α : Type u_1} {f : αα} {x : α} :
            theorem Function.periodicOrbit_apply_iterate_eq {α : Type u_1} {f : αα} {x : α} (hx : x Function.periodicPts f) (n : ) :
            theorem Function.periodicOrbit_apply_eq {α : Type u_1} {f : αα} {x : α} (hx : x Function.periodicPts f) :
            theorem Function.periodicOrbit_chain {α : Type u_1} (r : ααProp) {f : αα} {x : α} :
            theorem Function.periodicOrbit_chain' {α : Type u_1} (r : ααProp) {f : αα} {x : α} (hx : x Function.periodicPts f) :
            Cycle.Chain r (Function.periodicOrbit f x) ∀ (n : ), r (f^[n] x) (f^[n + 1] x)
            @[simp]
            theorem Function.isFixedPt_prod_map {α : Type u_1} {β : Type u_2} {f : αα} {g : ββ} (x : α × β) :
            @[simp]
            theorem Function.isPeriodicPt_prod_map {α : Type u_1} {β : Type u_2} {f : αα} {g : ββ} {n : } (x : α × β) :
            theorem Function.minimalPeriod_prod_map {α : Type u_1} {β : Type u_2} (f : αα) (g : ββ) (x : α × β) :
            theorem Function.minimalPeriod_fst_dvd {α : Type u_1} {β : Type u_2} {f : αα} {g : ββ} {x : α × β} :
            theorem Function.minimalPeriod_snd_dvd {α : Type u_1} {β : Type u_2} {f : αα} {g : ββ} {x : α × β} :
            noncomputable def AddAction.period {α : Type v} {M : Type u} [AddMonoid M] [AddAction M α] (m : M) (a : α) :

            The period of an additive action of g on a is the smallest positive n such that (n • g) +ᵥ a = a, or 0 if such an n does not exist.

            Equations
            Instances For
              noncomputable def MulAction.period {α : Type v} {M : Type u} [Monoid M] [MulAction M α] (m : M) (a : α) :

              The period of a multiplicative action of g on a is the smallest positive n such that g ^ n • a = a, or 0 if such an n does not exist.

              Equations
              Instances For
                theorem AddAction.period_eq_minimalPeriod {α : Type v} {M : Type u} [AddMonoid M] [AddAction M α] {m : M} {a : α} :
                AddAction.period m a = Function.minimalPeriod (fun (x : α) => m +ᵥ x) a

                AddAction.period m a is definitionally equal to Function.minimalPeriod (m +ᵥ ·) a

                theorem MulAction.period_eq_minimalPeriod {α : Type v} {M : Type u} [Monoid M] [MulAction M α] {m : M} {a : α} :
                MulAction.period m a = Function.minimalPeriod (fun (x : α) => m x) a

                MulAction.period m a is definitionally equal to Function.minimalPeriod (m • ·) a.

                @[simp]
                theorem AddAction.nsmul_period_vadd {α : Type v} {M : Type u} [AddMonoid M] [AddAction M α] (m : M) (a : α) :

                (period m a) • m fixes a.

                @[simp]
                theorem MulAction.pow_period_smul {α : Type v} {M : Type u} [Monoid M] [MulAction M α] (m : M) (a : α) :

                m ^ (period m a) fixes a.

                theorem AddAction.isPeriodicPt_vadd_iff {α : Type v} {M : Type u} [AddMonoid M] [AddAction M α] {m : M} {a : α} {n : } :
                Function.IsPeriodicPt (fun (x : α) => m +ᵥ x) n a n m +ᵥ a = a
                theorem MulAction.isPeriodicPt_smul_iff {α : Type v} {M : Type u} [Monoid M] [MulAction M α] {m : M} {a : α} {n : } :
                Function.IsPeriodicPt (fun (x : α) => m x) n a m ^ n a = a

                Multiples of MulAction.period #

                It is easy to convince oneself that if g ^ n • a = a (resp. (n • g) +ᵥ a = a), then n must be a multiple of period g a.

                This also holds for negative powers/multiples.

                theorem AddAction.nsmul_vadd_eq_iff_period_dvd {α : Type v} {M : Type u} [AddMonoid M] [AddAction M α] {n : } {m : M} {a : α} :
                theorem MulAction.pow_smul_eq_iff_period_dvd {α : Type v} {M : Type u} [Monoid M] [MulAction M α] {n : } {m : M} {a : α} :
                m ^ n a = a MulAction.period m a n
                theorem AddAction.zsmul_vadd_eq_iff_period_dvd {α : Type v} {G : Type u} [AddGroup G] [AddAction G α] {j : } {g : G} {a : α} :
                j g +ᵥ a = a (AddAction.period g a) j
                theorem MulAction.zpow_smul_eq_iff_period_dvd {α : Type v} {G : Type u} [Group G] [MulAction G α] {j : } {g : G} {a : α} :
                g ^ j a = a (MulAction.period g a) j
                @[simp]
                theorem AddAction.nsmul_mod_period_vadd {α : Type v} {M : Type u} [AddMonoid M] [AddAction M α] (n : ) {m : M} {a : α} :
                (n % AddAction.period m a) m +ᵥ a = n m +ᵥ a
                @[simp]
                theorem MulAction.pow_mod_period_smul {α : Type v} {M : Type u} [Monoid M] [MulAction M α] (n : ) {m : M} {a : α} :
                m ^ (n % MulAction.period m a) a = m ^ n a
                @[simp]
                theorem AddAction.zsmul_mod_period_vadd {α : Type v} {G : Type u} [AddGroup G] [AddAction G α] (j : ) {g : G} {a : α} :
                (j % (AddAction.period g a)) g +ᵥ a = j g +ᵥ a
                @[simp]
                theorem MulAction.zpow_mod_period_smul {α : Type v} {G : Type u} [Group G] [MulAction G α] (j : ) {g : G} {a : α} :
                g ^ (j % (MulAction.period g a)) a = g ^ j a
                @[simp]
                theorem AddAction.nsmul_add_period_vadd {α : Type v} {M : Type u} [AddMonoid M] [AddAction M α] (n : ) (m : M) (a : α) :
                (n + AddAction.period m a) m +ᵥ a = n m +ᵥ a
                @[simp]
                theorem MulAction.pow_add_period_smul {α : Type v} {M : Type u} [Monoid M] [MulAction M α] (n : ) (m : M) (a : α) :
                m ^ (n + MulAction.period m a) a = m ^ n a
                @[simp]
                theorem AddAction.nsmul_period_add_vadd {α : Type v} {M : Type u} [AddMonoid M] [AddAction M α] (n : ) (m : M) (a : α) :
                (AddAction.period m a + n) m +ᵥ a = n m +ᵥ a
                @[simp]
                theorem MulAction.pow_period_add_smul {α : Type v} {M : Type u} [Monoid M] [MulAction M α] (n : ) (m : M) (a : α) :
                m ^ (MulAction.period m a + n) a = m ^ n a
                @[simp]
                theorem AddAction.zsmul_add_period_vadd {α : Type v} {G : Type u} [AddGroup G] [AddAction G α] (i : ) (g : G) (a : α) :
                (i + (AddAction.period g a)) g +ᵥ a = i g +ᵥ a
                @[simp]
                theorem MulAction.zpow_add_period_smul {α : Type v} {G : Type u} [Group G] [MulAction G α] (i : ) (g : G) (a : α) :
                g ^ (i + (MulAction.period g a)) a = g ^ i a
                @[simp]
                theorem AddAction.zsmul_period_add_vadd {α : Type v} {G : Type u} [AddGroup G] [AddAction G α] (i : ) (g : G) (a : α) :
                ((AddAction.period g a) + i) g +ᵥ a = i g +ᵥ a
                @[simp]
                theorem MulAction.zpow_period_add_smul {α : Type v} {G : Type u} [Group G] [MulAction G α] (i : ) (g : G) (a : α) :
                g ^ ((MulAction.period g a) + i) a = g ^ i a
                theorem AddAction.nsmul_vadd_eq_iff_minimalPeriod_dvd {α : Type v} {G : Type u} [AddGroup G] [AddAction G α] {a : G} {b : α} {n : } :
                n a +ᵥ b = b Function.minimalPeriod (fun (x : α) => a +ᵥ x) b n
                theorem MulAction.pow_smul_eq_iff_minimalPeriod_dvd {α : Type v} {G : Type u} [Group G] [MulAction G α] {a : G} {b : α} {n : } :
                a ^ n b = b Function.minimalPeriod (fun (x : α) => a x) b n
                theorem AddAction.zsmul_vadd_eq_iff_minimalPeriod_dvd {α : Type v} {G : Type u} [AddGroup G] [AddAction G α] {a : G} {b : α} {n : } :
                n a +ᵥ b = b (Function.minimalPeriod (fun (x : α) => a +ᵥ x) b) n
                theorem MulAction.zpow_smul_eq_iff_minimalPeriod_dvd {α : Type v} {G : Type u} [Group G] [MulAction G α] {a : G} {b : α} {n : } :
                a ^ n b = b (Function.minimalPeriod (fun (x : α) => a x) b) n
                @[simp]
                theorem AddAction.nsmul_vadd_mod_minimalPeriod {α : Type v} {G : Type u} [AddGroup G] [AddAction G α] (a : G) (b : α) (n : ) :
                (n % Function.minimalPeriod (fun (x : α) => a +ᵥ x) b) a +ᵥ b = n a +ᵥ b
                @[simp]
                theorem MulAction.pow_smul_mod_minimalPeriod {α : Type v} {G : Type u} [Group G] [MulAction G α] (a : G) (b : α) (n : ) :
                a ^ (n % Function.minimalPeriod (fun (x : α) => a x) b) b = a ^ n b
                @[simp]
                theorem AddAction.zsmul_vadd_mod_minimalPeriod {α : Type v} {G : Type u} [AddGroup G] [AddAction G α] (a : G) (b : α) (n : ) :
                (n % (Function.minimalPeriod (fun (x : α) => a +ᵥ x) b)) a +ᵥ b = n a +ᵥ b
                @[simp]
                theorem MulAction.zpow_smul_mod_minimalPeriod {α : Type v} {G : Type u} [Group G] [MulAction G α] (a : G) (b : α) (n : ) :
                a ^ (n % (Function.minimalPeriod (fun (x : α) => a x) b)) b = a ^ n b