The Katona circle method

This file provides tooling to use the Katona circle method, which is double-counting ways to order n elements on a circle under some condition.

@[reducible, inline]

abbrev Numbering (X : Type u_1) [Fintype X] : Type u_1

A numbering of a fintype X is a bijection between X and Fin (card X).

Equations

• Numbering X = (X ≃ Fin (Fintype.card X))

@[simp]

theorem Fintype.card_numbering {X : Type u_1} [Fintype X] [DecidableEq X] : card (Numbering X) = (card X).factorial

def Numbering.IsPrefix {X : Type u_1} [Fintype X] (f : Numbering X) (s : Finset X) : Prop

IsPrefix f s means that the elements of s precede the elements of sᶜ in the numbering f.

Equations

• f.IsPrefix s = ∀ (x : X), x ∈ s ↔ ↑(f x) < s.card

theorem Numbering.IsPrefix.subset_of_card_le_card {X : Type u_1} [Fintype X] {f : Numbering X} {s t : Finset X} (hs : f.IsPrefix s) (ht : f.IsPrefix t) (hst : s.card ≤ t.card) : s ⊆ t

instance Numbering.instDecidableIsPrefix {X : Type u_1} [Fintype X] {f : Numbering X} {s : Finset X} [DecidableEq X] : Decidable (f.IsPrefix s)

Equations

• Numbering.instDecidableIsPrefix = id inferInstance

def Numbering.prefixed {X : Type u_1} [Fintype X] [DecidableEq X] (s : Finset X) : Finset (Numbering X)

The set of numberings of which s is a prefix.

Equations

• Numbering.prefixed s = {f : Numbering X | f.IsPrefix s}

@[simp]

theorem Numbering.mem_prefixed {X : Type u_1} [Fintype X] {f : Numbering X} {s : Finset X} [DecidableEq X] : f ∈ prefixed s ↔ f.IsPrefix s

def Numbering.prefixedEquiv {X : Type u_1} [Fintype X] [DecidableEq X] (s : Finset X) : ↥(prefixed s) ≃ Numbering ↥s × Numbering ↥sᶜ

Decompose a numbering of which s is a prefix into a numbering of s and a numbering on sᶜ.

Equations

• One or more equations did not get rendered due to their size.

theorem Numbering.card_prefixed {X : Type u_1} [Fintype X] [DecidableEq X] (s : Finset X) : (prefixed s).card = s.card.factorial * (Fintype.card X - s.card).factorial

@[simp]

theorem Numbering.dens_prefixed {X : Type u_1} [Fintype X] [DecidableEq X] (s : Finset X) : (prefixed s).dens = (↑((Fintype.card X).choose s.card))⁻¹

theorem Numbering.disjoint_prefixed_prefixed {X : Type u_1} [Fintype X] {s t : Finset X} [DecidableEq X] (hst : ¬s ⊆ t) (hts : ¬t ⊆ s) : Disjoint (prefixed s) (prefixed t)