EndpointAssignment.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Infinite endpoint assignment from a finite density inequality. No countability or distinctness assumption on the edge labels is needed.

def OAI.Dixmier.endpointSlots line 15

theorem OAI.Dixmier.endpointSlots_biUnion line 20

Source documentation

All neighboring slots of a finite edge set: endpoints have distinct copies.

theorem endpointSlots_biUnion (row : E → V) (col : E → W) (r : ℕ)
    (F : Finset E) :
    F.biUnion (endpointSlots row col r) =
      ((F.image row) ×ˢ (univ : Finset (Fin r))).disjSum ((F.image col) ×ˢ univ) := by
…

Mentions: OAI.Dixmier.endpointSlots

theorem OAI.Dixmier.exists_endpoint_assignment line 29

Source documentation

Infinite Hall matching with r slots at every row and every column.

theorem exists_endpoint_assignment (row : E → V) (col : E → W) (r : ℕ)
    (hdensity : ∀ F : Finset E, F.card ≤ r * ((F.image row).card + (F.image col).card)) :
    ∃ f : E → (V × Fin r) ⊕ (W × Fin r), Function.Injective f ∧
      ∀ e, f e ∈ endpointSlots row col r e := by
…

Mentions: OAI.Dixmier.endpointSlots

def OAI.Dixmier.slotIndex line 40
def OAI.Dixmier.isRowSlot line 44
theorem OAI.Dixmier.assigned_row_eq line 48
theorem OAI.Dixmier.assigned_col_eq line 60

theorem OAI.Dixmier.assigned_row_card_le line 73

Source documentation

Injectivity of the slot assignment bounds every finite row load.

theorem assigned_row_card_le {row : E → V} {col : E → W} {r : ℕ}
    {f : E → (V × Fin r) ⊕ (W × Fin r)}
    (hinj : Function.Injective f) (hf : ∀ e, f e ∈ endpointSlots row col r e)
    (v : V) (F : Finset E) (hF : ∀ e ∈ F, row e = v ∧ isRowSlot (f e) = true) :
    F.card ≤ r := by
…

Mentions: OAI.Dixmier.endpointSlots, OAI.Dixmier.isRowSlot

theorem OAI.Dixmier.assigned_col_card_le line 91

Source documentation

Injectivity also bounds every finite column load.

theorem assigned_col_card_le {row : E → V} {col : E → W} {r : ℕ}
    {f : E → (V × Fin r) ⊕ (W × Fin r)}
    (hinj : Function.Injective f) (hf : ∀ e, f e ∈ endpointSlots row col r e)
    (w : W) (F : Finset E) (hF : ∀ e ∈ F, col e = w ∧ isRowSlot (f e) = false) :
    F.card ≤ r := by
…

Mentions: OAI.Dixmier.endpointSlots, OAI.Dixmier.isRowSlot

theorem OAI.Dixmier.exists_sparse_mask line 109

Source documentation

A sparse mask from finite endpoint density.

theorem exists_sparse_mask {G I : Type*} [Group G] [Fintype I] (s : I → G) (r : ℕ)
    (hdensity : ∀ F : Finset (G × I), F.card ≤
      r * ((F.image Prod.fst).card + (F.image (fun e => e.1 * s e.2)).card)) :
    ∃ a : G → I → Bool, (∀ x, (rowOnes a x).card ≤ r) ∧
      ∀ y, (columnZeros a s y).card ≤ r := by
…

Mentions: OAI.Dixmier.rowOnes, OAI.Dixmier.columnZeros