If `f^[m] x = f^[n] x` then the range of `f^[·] x` is finite

Stream: Is there code for X?

[Andrew Yang]

I feel like the following proof is unreasonably long. Is there any filter/periodicPts API that can make this easier?

import Mathlib

example {α} {f : α → α} {n m x} (hnm : n ≠ m) (h : f^[n] x = f^[m] x) :
    Set.Finite (Set.range (f^[·] x)) := by
  classical
  wlog hnm' : n < m generalizing n m
  · exact this hnm.symm h.symm (hnm.lt_or_lt.resolve_left hnm')
  refine Set.Finite.ofFinset ((Finset.range m).image (f^[·] x)) ?_
  intro y
  simp only [Finset.mem_image, Finset.mem_range, Set.mem_range]
  refine ⟨fun H ↦ ⟨H.choose, H.choose_spec.2⟩, ?_⟩
  rintro ⟨k, rfl⟩
  induction k using Nat.strong_induction_on
  next k IH =>
  cases lt_or_le k m
  · exact ⟨k, ‹_›, rfl⟩
  · obtain ⟨a, ha, ha'⟩ := IH (k - (m - n))
      (Nat.sub_lt_self (Nat.sub_pos_of_lt hnm')
        (Nat.sub_le_of_le_add (le_add_right ‹_›)))
    use a, ha
    rw [ha', tsub_tsub_assoc ‹_› hnm'.le, Function.iterate_add_apply, h,
      ← Function.iterate_add_apply, tsub_add_cancel_of_le ‹_›]

[Andrew Yang]

I tried to split it up. Did I miss any of the lemmas in mathlib?

import Mathlib

open Filter Set

theorem Set.range_add_const {M}
    [CanonicallyOrderedAddCommMonoid M] (x : M) :
      range (· + x) = Ici x := by
  ext y; simp only [mem_Ici, mem_range]
  refine ⟨fun ⟨y, e⟩ ↦ e ▸ le_add_self, fun h ↦ ?_⟩
  simpa only [eq_comm (a := _ + _), add_comm x] using exists_add_of_le h

theorem Function.Periodic.image_Ico_eq_image_Ico {β}
    {f : ℕ → β} {c} (h : Periodic f c) (hc : 0 < c) :
      ∀ a, f '' Ico a (a + c) = f '' Ico 0 c
  | 0 => by rw [Nat.zero_add]
  | .succ a =>
    have : a < a + c := add_lt_add_left hc a
    by rw [← image_Ico_eq_image_Ico h hc a, Nat.succ_add, ← Nat.succ_eq_succ,
      Order.Ico_succ_right, Order.Icc_succ_left, ← Ioo_insert_left this,
      ← Ioo_insert_right this, image_insert_eq, image_insert_eq, h]

theorem Function.Periodic.image_Ico {β}
    {f : ℕ → β} {c} (h : Periodic f c)
    (hc : 0 < c) (a : ℕ) : f '' Ico a (a + c) = range f := by
  refine (image_subset_range _ _).antisymm <| range_subset_iff.2 fun x ↦ ?_
  rw [h.image_Ico_eq_image_Ico hc, ← h.image_Ico_eq_image_Ico hc x]
  exact ⟨x, ⟨le_rfl, add_lt_add_left hc x⟩, rfl⟩

theorem range_finite_of_eventually_periodic {α} (f : ℕ → α) {k} (hk : 0 < k)
    (hf : f =ᶠ[atTop] f ∘ (· + k)) : Set.Finite (range f) := by
  obtain ⟨N, hN⟩ := Filter.eventually_atTop.mp hf
  have : Function.Periodic (f ∘ (· + N)) k := by
    intro n
    simp only [Function.comp_apply, hN _ (Nat.le_add_left N n), add_right_comm n k N]
  rw [← image_univ, ← Ici_bot, bot_eq_zero', ← Ico_union_Ici_eq_Ici N.zero_le,
    ← range_add_const N, image_union, ← range_comp, ← this.image_Ico hk 0]
  exact ((Set.finite_Ico 0 N).image f).union ((Set.finite_Ico _ _).image _)

example {α} {f : α → α} {n m x} (hnm : n ≠ m) (h : f^[n] x = f^[m] x) :
    Set.Finite (Set.range (f^[·] x)) := by
  wlog hlt : n < m generalizing n m
  · apply this hnm.symm h.symm (hnm.lt_or_lt.resolve_left hlt)
  refine range_finite_of_eventually_periodic _
    (Nat.lt_sub_of_add_lt ((zero_add n).trans_lt hlt))
    (Filter.eventually_atTop.mpr ?_)
  use n
  intro b hb
  simp only [Function.comp_apply]
  rw [← tsub_add_cancel_of_le hb, add_assoc, add_tsub_cancel_of_le hlt.le,
    Function.iterate_add_apply, Function.iterate_add_apply, h]

[Floris van Doorn]

Presumably you can simplify Function.Periodic.image_Ico by mimicking the proof of docs#Function.Periodic.image_Ioc (although your version is already quite simple).

[Arend Mellendijk]

Alas, Nat is not a LinearOrderedAddCommGroup

[Floris van Doorn]

I missed that condition. Maybe some of these lemmas can be generalized to a weaker type class?

[Floris van Doorn]

Here is a generalization of some Mathlib lemmas so that it also works for Nat (not quite connected to the lemmas you need though):

import Mathlib.Algebra.Periodic

open Function Set
variable {α β : Type _} {f : α → β}

theorem exists_add_nsmul_eq_add_nsmul [LinearOrderedAddCommMonoid α]
    [Archimedean α] [Sub α] [OrderedSub α] [IsLeftCancelAdd α] [ExistsAddOfLE α]
    {a : α} (ha : 0 < a) (y : α) :
    ∃ (x : α), ∃ (k l : ℕ), x ∈ Ico 0 a ∧ x + k • a = y + l • a := by -- todo: maybe show that `x` is unique
  classical
  have ⟨k, hk⟩ := Archimedean.arch y ha
  have ⟨l, hl, h2l⟩ := Nat.findX <| Archimedean.arch (k • a - y) ha
  rw [tsub_le_iff_left] at hl
  simp_rw [tsub_le_iff_left] at h2l
  refine ⟨y + l • a - k • a, k, l, ⟨?_, ?_⟩, ?_⟩
  · apply le_tsub_of_add_le_left; rwa [add_zero]
  · rw [tsub_lt_iff_left hl, ← not_le]
    intro h
    cases' l with l
    · nth_rw 2 [← one_smul ℕ a] at h
      simp only [← add_smul, Nat.zero_eq, zero_smul, add_zero] at h hk
      have := h.trans hk
      rw [nsmul_le_nsmul_iff_left ha] at this
      omega
    · simp_rw [Nat.succ_eq_add_one] at *
      apply h2l l (lt_add_one l)
      apply le_of_add_le_add_right (a := a)
      rwa [add_smul, one_smul, ← add_assoc] at h
  · rw [tsub_add_cancel_of_le hl]

theorem Function.Periodic.exists_mem_Ico₀' [LinearOrderedAddCommMonoid α]
    [Archimedean α] [Sub α] [OrderedSub α] [IsLeftCancelAdd α] [ExistsAddOfLE α]
    (h : Periodic f c) (hc : 0 < c) (x) : ∃ y ∈ Ico 0 c, f x = f y := by
  obtain ⟨y, k, l, hy, hkl⟩ := exists_add_nsmul_eq_add_nsmul hc x
  refine ⟨y, hy, by rw [← h.nsmul l, ← hkl, h.nsmul k]⟩

[Yaël Dillies]

Andrew, your first lemma is just ext + docs#le_iff_exists_add

[Antoine Chambert-Loir]

In the initial proof, you prove that the range of your function equals the image of range m (when n<m). On the other hand, you only need the inclusion to get finiteness, and that might simplify the proof a little bit.