OAI/Combinatorics/ContingencyTables/Sampling/PhysicalGraphDegree.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The manuscript's finite neighbor bound on the physical small graph

  1. def OAI.ContingencyTables.SmallGraphProfiles.fullNeighbors line 19
  2. lemma OAI.ContingencyTables.SmallGraphProfiles.fullNeighbors_subset line 24
  3. theorem OAI.ContingencyTables.SmallGraphProfiles.fullNeighbors_card_le line 51

    Source documentation

    Counting distinct neighbors, with repeated exchange/repair edges removed by the finite-set union, gives exactly the source bound.

    theorem fullNeighbors_card_le (r : I → ℕ) (c : J → ℕ) (U L : ℕ) (B : I → J → ℕ)
    (hB : ∀ i j,firstPaperSmall r c U i j=true → B i j=U)
    (v : SmallProfile (firstPaperSmall r c U)) :
    (fullNeighbors r c U L B hB v).card ≤ 5*(Fintype.card (Cells (firstPaperSmall r c U)))^2+1 := by
…

    Mentions: OAI.ContingencyTables.SmallGraphProfiles.fullNeighbors