Basic results about finite ordinal types

This file collects elementary facts about finite ordinal types, including the classification of permutations of Fin 2, sums of reversed indices, indicator sums indexed by Fin n, the final value of a partial product, and the cyclic index arithmetic of Fin 3.

Fintype.sum_ite_eq evaluates a sum whose indicator compares two elements of the index type. When the comparison is instead between a natural number and the Fin.val of the index — as it is whenever a family is indexed by ℕ and summed over Fin n — the index may fall outside the range, so the value is a dite rather than a plain application.

Main results

• TauCeti.perm_fin_two_eq_one_or_swap: every permutation of Fin 2 is the identity or the transposition.
• TauCeti.forall_cons_swap_eq_zero_iff: vanishing of the final coordinates after swapping coordinate zero with coordinate d in a vector built with Fin.cons.
• Fin.rev_finRotate_rev and Fin.rev_finRotate_symm: reversal carries forward rotation to backward rotation and conversely.
• Fin.finRotate_rev_finRotate_rev: negation modulo n, written as i ↦ finRotate n i.rev, is an involution.
• Fin.coe_finRotate_pow: a power of the rotation finRotate n adds its exponent modulo n.
• Finset.sum_range_const_sub_succ: the sum of a reversed initial segment of natural numbers.
• Fin.sum_rev_castLE: the sum of the values of a reversed embedded finite ordinal.
• Fin.castSucc_add_one_of_ne_last, Fin.castSucc_sub_one_of_ne_zero: how Fin.castSucc interacts with the cyclic successor and predecessor.
• Fin.zero_sub_one_eq_last: subtracting one from 0 gives the last index.
• Fin.eq_castSucc_last_or_eq_last: an index ≥ n of Fin (n + 2) is the penultimate or the last one.
• Fin.last_ne_zero, Fin.castSucc_last_ne_zero, Fin.castSucc_last_ne_one, Fin.last_ne_one: the last and penultimate indices differ from 0 and 1 in the nondegenerate cases.
• Fin.sum_univ_eq_zero_add_last_add_sum_erase: a sum over Fin (n + 1) with its first and last summands split off.
• Fin.natCast_ne_zero: the cast of a natural number 0 < a < n to Fin n (under open Fin.NatCast) is nonzero.
• Fin.predAbove_succ_succAbove: Fin.predAbove p inverts p.succ.succAbove, the counterpart of Mathlib's Fin.predAbove_succAbove for p.castSucc.succAbove.
• Fin.val_succAbove: the value of p.succAbove i, read off the comparison of i with p.
• Fin.finRotate_succ_eq_succ_succAbove and Fin.finRotate_succ_succAbove_of_ne: the cyclic successor of Fin (n + 1) against the embeddings Fin.succ and i.succ.succAbove of Fin n, as used when a new entry is inserted into a cyclic sequence.
• Fin.succAbove_adjacent_cases: the positions p of Fin (n + 1) cyclically adjacent to p.succAbove i.
• Fin.swap_castSucc_succ_succAbove: the transposition of k.castSucc and k.succ exchanges the embeddings of Fin n skipping either of them.
• Fin.card_filter_prod_succAbove: a count of pairs in Fin (n + 1) split at a point in each coordinate.
• Fin.val_orderSucc_of_lt and Fin.orderSucc_eq_self_of_not_lt: the order successor of Fin n read off the value, below and at the top element. Mathlib's Fin.orderSucc_castSucc and Fin.orderSucc_last state the same thing in the castSucc/last normal form; these are the versions keyed on the inequality i + 1 < n.
• Fin.partialProd_last: the final partial product is the product of all the entries.
• Fin.partialSum_last: the final partial sum is the sum of all the entries.
• TauCeti.add_one_ne_self: adding one in Fin n is nontrivial when 2 ≤ n.
• TauCeti.add_one_add_one_ne_self: adding one twice in Fin n is nontrivial when 3 ≤ n; TauCeti.sub_one_ne_self and TauCeti.add_one_ne_sub_one are the companions for subtraction.
• TauCeti.apply_eq_apply_zero_of_add_one: a function on Fin (n + 1) unchanged by adding one is constant.
• TauCeti.eq_add_one_or_eq_add_two_fin_three: a distinct index of Fin 3 is one of the two shifts of the other.
• TauCeti.add_one_add_one_fin_three, TauCeti.add_one_add_two_fin_three, TauCeti.add_two_add_one_fin_three and TauCeti.add_two_add_two_fin_three: the shifts by 1 and 2 compose cyclically in Fin 3.
• TauCeti.sum_fin_three_rotate: a sum over Fin 3 read off starting from an arbitrary index.
• TauCeti.neg_one_pow_val_add_one: for n even, adding one in Fin n flips the sign (-1) ^ · read off the value.
• TauCeti.sum_ite_val_add: a sum against the indicator of b = k + j picks out the summand at b - j, or vanishes when there is no such index.
• TauCeti.exists_foldl_eq_of_parent: a decreasing parent table gives paths from its root.
• TauCeti.not_mem_Ioo_castSucc_succ: a monotone Fin family has no value strictly between consecutive entries.
• TauCeti.exists_mem_Icc_castSucc_succ: consecutive closed intervals cover the interval between the first and last values of a monotone Fin family.

theorem Finset.sum_range_const_sub_succ (N k : ℕ) (hk : k ≤ N) : ∑ x ∈ range k, (N - (x + 1)) = k.choose 2 + k * (N - k)

The sum of the first k entries of the reversed range N - 1, ..., 0.

theorem Fin.sum_rev_castLE (N k : ℕ) (hk : k ≤ N) : ∑ i : Fin k, ↑(castLE hk i).rev = k.choose 2 + k * (N - k)

The sum of the values in the first k positions of the reversed finite ordinal Fin N.

theorem Fin.partialProd_last {M : Type u_1} [CommMonoid M] {n : ℕ} (f : Fin n → M) : partialProd f (last n) = ∏ i : Fin n, f i

The final partial product is the product of all the entries.

theorem Fin.partialSum_last {M : Type u_1} [AddCommMonoid M] {n : ℕ} (f : Fin n → M) : partialSum f (last n) = ∑ i : Fin n, f i

The final partial sum is the sum of all the entries.

@[simp]

theorem Fin.rev_finRotate_rev {n : ℕ} (i : Fin n) : (i.rev + 1).rev = (Equiv.symm (finRotate n)) i

Conjugating forward rotation of a finite ordinal by reversal gives backward rotation.

@[simp]

theorem Fin.rev_finRotate_symm {n : ℕ} (i : Fin n) : (i - 1).rev = (finRotate n) i.rev

Reversal carries backward rotation of a finite ordinal to forward rotation.

theorem Fin.finRotate_rev_finRotate_rev {n : ℕ} (i : Fin n) : (finRotate n) ((finRotate n) i.rev).rev = i

The map i ↦ finRotate n i.rev, which is negation modulo n, is an involution.

theorem Fin.coe_finRotate_pow {n : ℕ} (k : ℕ) (c : Fin n) : ↑((finRotate n ^ k) c) = (↑c + k) % n

The value of a power of the cyclic permutation finRotate n: it adds k modulo n.

@[simp]

theorem Fin.predAbove_succ_succAbove {n : ℕ} (p i : Fin n) : p.predAbove (p.succ.succAbove i) = i

Collapsing the hole opened immediately after p back onto p inverts the embedding p.succ.succAbove.

theorem Fin.val_succAbove {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : ↑(p.succAbove i) = if ↑i < ↑p then ↑i else ↑i + 1

The value of p.succAbove i: the value of i below p, and one more from p on.

theorem Fin.finRotate_succ_eq_succ_succAbove {n : ℕ} (i : Fin n) : (finRotate (n + 1)) i.succ = i.succ.succAbove ((finRotate n) i)

The cyclic successor of i.succ in Fin (n + 1) is the cyclic successor of i in Fin n, read through the embedding i.succ.succAbove that skips i.succ.

theorem Fin.finRotate_succ_succAbove_of_ne {n : ℕ} {i k : Fin n} (hk : k ≠ i) : (finRotate (n + 1)) (i.succ.succAbove k) = i.succ.succAbove ((finRotate n) k)

Away from i, the embedding i.succ.succAbove : Fin n → Fin (n + 1), which skips i.succ, commutes with the cyclic successors.

theorem Fin.succAbove_adjacent_cases {n : ℕ} {p : Fin (n + 1)} {i : Fin n} (h : (finRotate (n + 1)) p = p.succAbove i ∨ (finRotate (n + 1)) (p.succAbove i) = p) : p = i.castSucc ∨ p = i.succ ∨ p = last n ∧ i.castSucc = 0 ∨ p = 0 ∧ i.succ = last n

A position p of Fin (n + 1) cyclically adjacent to p.succAbove i is i.castSucc or i.succ, or wraps around: p is last and p.succAbove i is 0, or p is 0 and p.succAbove i is last.

theorem Fin.swap_castSucc_succ_succAbove {n : ℕ} (k i : Fin n) : (Equiv.swap k.castSucc k.succ) (k.castSucc.succAbove i) = k.succ.succAbove i

The transposition of k.castSucc and k.succ carries the embedding k.castSucc.succAbove, which skips k.castSucc, to the embedding k.succ.succAbove, which skips k.succ.

theorem Fin.card_filter_prod_succAbove {n : ℕ} (P : Fin (n + 1) × Fin (n + 1) → Prop) [DecidablePred P] (a b : Fin (n + 1)) : (Finset.filter P Finset.univ).card = (if P (a, b) then 1 else 0) + {j : Fin n | P (a, b.succAbove j)}.card + {i : Fin n | P (a.succAbove i, b)}.card + {p : Fin n × Fin n | P (a.succAbove p.1, b.succAbove p.2)}.card

A count of pairs in Fin (n + 1), split at a in the first coordinate and at b in the second: the pair (a, b), the pairs with exactly one coordinate at its split point, and the pairs embedded by a.succAbove and b.succAbove.

theorem Fin.castSucc_add_one_of_ne_last {n : ℕ} {i : Fin (n + 1)} (hi : i ≠ last n) : (i + 1).castSucc = i.castSucc + 1

Adding one commutes with Fin.castSucc away from the last index.

theorem Fin.castSucc_sub_one_of_ne_zero {n : ℕ} {i : Fin (n + 1)} (hi : i ≠ 0) : (i - 1).castSucc = i.castSucc - 1

Subtracting one commutes with Fin.castSucc away from 0.

theorem Fin.zero_sub_one_eq_last {n : ℕ} : 0 - 1 = last n

Subtracting one from 0 gives the last index.

theorem Fin.last_ne_zero {n : ℕ} (hn : n ≠ 0) : last n ≠ 0

The last index of Fin (n + 1) is not 0 when n ≠ 0.

theorem Fin.castSucc_last_ne_zero {n : ℕ} (hn : n ≠ 0) : (last n).castSucc ≠ 0

The penultimate index of Fin (n + 2) is not 0 when n ≠ 0.

theorem Fin.castSucc_last_ne_one {n : ℕ} (hn : n ≠ 1) : (last n).castSucc ≠ 1

The penultimate index of Fin (n + 2) is not 1 when n ≠ 1.

theorem Fin.last_ne_one {n : ℕ} (hn : n ≠ 0) : last (n + 1) ≠ 1

The last index of Fin (n + 2) is not 1 when n ≠ 0.

theorem Fin.eq_castSucc_last_or_eq_last {n : ℕ} {i : Fin (n + 2)} (hi : n ≤ ↑i) : i = (last n).castSucc ∨ i = last (n + 1)

An index of Fin (n + 2) that is at least n is the penultimate or the last one.

theorem Fin.sum_univ_eq_zero_add_last_add_sum_erase {n : ℕ} {M : Type u_1} [AddCommMonoid M] (hn : n ≠ 0) (f : Fin (n + 1) → M) : ∑ i : Fin (n + 1), f i = f 0 + f (last n) + ∑ i ∈ (Finset.univ.erase 0).erase (last n), f i

A sum over Fin (n + 1) with the first and the last summands split off.

theorem Fin.natCast_ne_zero {n a : ℕ} [NeZero n] (ha : a ≠ 0) (han : a < n) : ↑a ≠ 0

The cast of a natural number 0 < a < n to Fin n is nonzero.

theorem Fin.val_orderSucc_of_lt {n : ℕ} {i : Fin n} (h : ↑i + 1 < n) : ↑(Order.succ i) = ↑i + 1

Below the top element of Fin n, the order successor increments the value.

theorem Fin.orderSucc_eq_self_of_not_lt {n : ℕ} {i : Fin n} (h : ¬↑i + 1 < n) : Order.succ i = i

At the top element of Fin n the order successor is that element itself.

theorem TauCeti.forall_cons_swap_eq_zero_iff {α : Type u_1} [Zero α] {n d : ℕ} (hd : d ≤ n) (a : α) (y : Fin n → α) : (∀ (i : Fin (n + 1)), d ≤ ↑i → Fin.cons a y ((Equiv.swap 0 ⟨d, ⋯⟩) i) = 0) ↔ a = 0 ∧ ∀ (j : Fin n), d ≤ ↑j → y j = 0

After swapping coordinates zero and d, the entries of Fin.cons a y at indices at least d vanish exactly when a and the entries of y at indices at least d vanish.

theorem TauCeti.exists_foldl_eq_of_parent {n : ℕ} {J : Type u_1} (step : Fin (n + 1) → J → Fin (n + 1)) (parent : Fin n → Fin (n + 1)) (edge : Fin n → J) (hparent : ∀ (a : Fin n), ↑(parent a) < ↑a.succ) (hstep : ∀ (a : Fin n), step (parent a) (edge a) = a.succ) (a : Fin (n + 1)) : ∃ (l : List J), List.foldl step 0 l = a

A decreasing parent table gives a word carrying its root to every vertex.

theorem TauCeti.not_mem_Ioo_castSucc_succ {β : Type u_1} [Preorder β] {n : ℕ} (a : Fin (n + 1) → β) (ha : Monotone a) (i : Fin n) (k : Fin (n + 1)) : a k ∉ Set.Ioo (a i.castSucc) (a i.succ)

No value of a monotone Fin family lies strictly between consecutive entries.

theorem TauCeti.exists_mem_Icc_castSucc_succ {β : Type u_1} [LinearOrder β] {n : ℕ} (a : Fin (n + 1) → β) (ha : Monotone a) (hn : n ≠ 0) {x : β} (hx : x ∈ Set.Icc (a 0) (a (Fin.last n))) : ∃ (i : Fin n), x ∈ Set.Icc (a i.castSucc) (a i.succ)

A point between the first and last values of a monotone Fin family lies between consecutive values.

theorem TauCeti.add_one_ne_self {n : ℕ} [NeZero n] (hn : 2 ≤ n) (i : Fin n) : i + 1 ≠ i

Adding one in Fin n never returns to the same element when 2 ≤ n.

theorem TauCeti.add_one_add_one_ne_self {n : ℕ} [NeZero n] (hn : 3 ≤ n) (i : Fin n) : i + 1 + 1 ≠ i

Adding one twice in Fin n never returns to the same element when 3 ≤ n.

theorem TauCeti.sub_one_ne_self {n : ℕ} [NeZero n] (hn : 2 ≤ n) (i : Fin n) : i - 1 ≠ i

Subtracting one in Fin n never returns to the same element when 2 ≤ n.

theorem TauCeti.add_one_ne_sub_one {n : ℕ} [NeZero n] (hn : 3 ≤ n) (i : Fin n) : i + 1 ≠ i - 1

In Fin n with 3 ≤ n, the successor and the predecessor of an element are distinct.

theorem TauCeti.apply_eq_apply_zero_of_add_one {β : Type u_1} {n : ℕ} {f : Fin (n + 1) → β} (h : ∀ (i : Fin (n + 1)), f (i + 1) = f i) (i : Fin (n + 1)) : f i = f 0

A function on Fin (n + 1) unchanged by adding one is constant.

theorem TauCeti.neg_one_pow_val_add_one {M : Type u_1} [Monoid M] [HasDistribNeg M] {n : ℕ} [NeZero n] (hn : Even n) (i : Fin n) : (-1) ^ ↑(i + 1) = -(-1) ^ ↑i

Adding one in Fin n flips the sign (-1) ^ · read off the value when n is even. The wraparound at the last index respects the sign exactly because n is even.

theorem TauCeti.perm_fin_two_eq_one_or_swap (e : Equiv.Perm (Fin 2)) : e = 1 ∨ e = Equiv.swap 0 1

A permutation of Fin 2 is either the identity or the transposition.

theorem TauCeti.sum_ite_val_add {M : Type u_1} [AddCommMonoid M] {n : ℕ} (f : Fin n → M) (b j : ℕ) : (∑ k : Fin n, if b = ↑k + j then f k else 0) = if h : b - j < n ∧ j ≤ b then f ⟨b - j, ⋯⟩ else 0

A shifted indicator picks out one summand. Summing f over Fin n against the indicator of b = k + j gives f at the index b - j when that is a valid index and j ≤ b, and 0 otherwise.

Cyclic index arithmetic in Fin 3

theorem TauCeti.eq_add_one_or_eq_add_two_fin_three {i j : Fin 3} (h : i ≠ j) : i = j + 1 ∨ i = j + 2

A distinct index of Fin 3 is one of the two shifts of the other.

theorem TauCeti.add_one_add_one_fin_three (j : Fin 3) : j + 1 + 1 = j + 2

Shifting an index of Fin 3 by one twice is shifting it by two.

theorem TauCeti.add_one_add_two_fin_three (j : Fin 3) : j + 1 + 2 = j

Shifting an index of Fin 3 by one and then by two returns to it.

theorem TauCeti.add_two_add_one_fin_three (j : Fin 3) : j + 2 + 1 = j

Shifting an index of Fin 3 by two and then by one returns to it.

theorem TauCeti.add_two_add_two_fin_three (j : Fin 3) : j + 2 + 2 = j + 1

Shifting an index of Fin 3 by two twice is shifting it by one.

theorem TauCeti.sum_fin_three_rotate {M : Type u_1} [AddCommMonoid M] (f : Fin 3 → M) (j : Fin 3) : ∑ m : Fin 3, f m = f j + f (j + 1) + f (j + 2)

A sum over Fin 3 read off starting from an arbitrary index.