OAI/Combinatorics/Ramsey/CycleClique/Construction/LayerSums.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CycleClique.Construction.parityIndices line 14
2. def OAI.CycleClique.Construction.alternatingSum line 17
3. theorem OAI.CycleClique.Construction.alternatingSum_zero line 19
4. theorem OAI.CycleClique.Construction.alternatingSum_partition line 22
5. theorem OAI.CycleClique.Construction.alternatingSum_shifted_partition line 34
6. theorem OAI.CycleClique.Construction.alternatingSum_positive line 41
7. theorem OAI.CycleClique.Construction.indepNum_le_card line 53
8. theorem OAI.CycleClique.Construction.indepNum_pos_of_nonempty line 59
9. theorem OAI.CycleClique.Construction.distanceLayer_zero_indepNum line 66
10. theorem OAI.CycleClique.Construction.distanceLayer_one_nonempty line 78
11. def OAI.CycleClique.Construction.parityIndependent line 94
12. theorem OAI.CycleClique.Construction.parityIndependent_independent line 99
13. theorem OAI.CycleClique.Construction.parityIndependent_card line 114
14. theorem OAI.CycleClique.Construction.distanceLayer_order_sum line 128

    Source documentation

    Expansion of the preceding parity union gives the exact first-layer order inequality used in the density argument.

    theorem distanceLayer_order_sum {V : Type*} [Fintype V]
        {G : SimpleGraph V} {k : ℕ} (hk : 1 ≤ k)
        (hexpand : ∀ I : Finset V, G.IsIndepSet (I : Set V) → I.Nonempty →
          k * I.card + 1 ≤ (closedNeighborhood G I).card)
        (root : V) {i : ℕ} (hi : 1 ≤ i) :
        k * alternatingSum (fun j => (G.induce (distanceLayer G root j : Set V)).indepNum) (i - 1) ≤
          ∑ j ∈ Finset.range i, (distanceLayer G root (j + 1)).card := by
    …

    Mentions: OAI.CycleClique.Construction.closedNeighborhood, OAI.CycleClique.Construction.alternatingSum, OAI.CycleClique.Construction.distanceLayer