OAI/NumberTheory/Ostmann/Tree/CellGroupPigeonhole.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.encodeCellGroups line 9
2. def OAI.Ostmann.decodeCellGroups line 13
3. theorem OAI.Ostmann.decode_encodeCellGroups line 18
4. theorem OAI.Ostmann.encodeCellGroups_injective_of_length line 24
5. theorem OAI.Ostmann.encodeCellGroups_length line 31
6. theorem OAI.Ostmann.encodeCellGroups_entries line 38
7. theorem OAI.Ostmann.common_cell_groups line 55

   Source documentation

   Length-prefix coding retains the group boundaries while using only one extra entry per group. Thus the pigeonhole cost depends on the total label count, rather than the product of the separate group-length bounds.

   theorem common_cell_groups (E : Finset ℕ) (hE : E.Nonempty) (r N B : ℕ)
       (ws : ℕ → List (List ℕ))
       (hr : ∀ a ∈ E, (ws a).length = r)
       (hlen : ∀ a ∈ E, ((ws a).map List.length).sum ≤ N)
       (hentry : ∀ a ∈ E, ∀ w ∈ ws a, ∀ h ∈ w, h ≤ B) :
       ∃ v : List (List ℕ), ∃ S : Finset ℕ, S ⊆ E ∧ S.Nonempty ∧
         E.card ≤ ((N + r + 1) * (max N B + 1) ^ (N + r)) * S.card ∧
         ∀ a ∈ S, ws a = v := by
   …