Another Pigeonhole?

Stream: Is there code for X?

[MohanadAhmed]

Is this a valid formulation: if a function maps numbers between (0 and m) to numbers between (0 and n), and m is greater than n, there must be at least (m - n) collisions, i.e. different numbers mapped to the same number.

import Mathlib.Data.Set.Card

theorem at_least_m_sub_n_collisions
  (m n : ℕ)(hmn : n < m)
  (f : (Fin m) → (Fin n)) :
  (m -n) ≤ {x : (Fin m) | ∃ y, y ≠ x ∧ f y = f x}.ncard := by sorry

[Michael Rothgang]

Can you precisely define (in English) what you mean by "collisions"?

[MohanadAhmed]

If $x \neq y$ but $f(x) = f(y)$ then this is a collision. An injective function produces no collisions. For some reason I was using the hashing terminology :)

[Kevin Buzzard]

How many collisions does the function from $\{1,2,3,4\}$ to $\{1\}$ have? Three? Six?

[Michael Rothgang]

Four?

[MohanadAhmed]

I think four

[MohanadAhmed]

Kevin Buzzard said:

How many collisions does the function from $\{1,2,3,4\}$ to $\{1\}$ have? Three? Six?

Alternatively, can define collisions to exclude one element (that is arbitrarily assigned to be the representative of its image e.g. in your example I can say $1$ is good and $2,3,4$ are "collisions"). With this definition the number of collisions would still be at least the difference of the domain and codomain cardinalities.

[Scott Carnahan]

If you are willing to use the order on Fin m, you can change your defining condition to y < x instead of y ≠ x. This more or less selects the least element of the preimage (if it exists) as a preferred element. Alternatively, you can sum over Fin n the quantity (size of preimage of element - 1).

[Antoine Chambert-Loir]

docs#Finset.exists_lt_card_fiber_of_nsmul_lt_card_of_maps_to will give you one element which is reached a large number of times. But you want something slightly different, since you appear to wish to count multiple preimages of several points.