Extending a partial graph embedding

The existence and counting lemmas use the same local extension step. Their estimates for how many extension vertices exist remain separate.

noncomputable def PartialEmbedding.candidates {α : Type u_1} {β : Type u_2} (G : SimpleGraph α) (L : SimpleGraph β) (parts : β → Finset α) (f : β → α) (S : Finset β) (y : β) : Finset α

Vertices in parts y compatible with the partial edge map f on S. Exclusion of already used vertices is handled separately when extending the embedding.

Equations

• PartialEmbedding.candidates G L parts f S y = {w ∈ parts y | ∀ z ∈ S, L.Adj z y → G.Adj (f z) w}

theorem PartialEmbedding.extend {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (G : SimpleGraph α) [DecidableRel G.Adj] (L : SimpleGraph β) (parts : β → Finset α) {d : ℝ} (hd : 0 < d) (hd₁ : d ≤ 1) (S : Finset β) (x : β) (hxS : x ∉ S) (f : β → α) (v : α) (hinj : Set.InjOn f ↑S) (hmem : ∀ z ∈ S, f z ∈ parts z) (hadj : ∀ a ∈ S, ∀ b ∈ S, L.Adj a b → G.Adj (f a) (f b)) (hcand : ∀ y ∉ S, d ^ S.card * ↑(parts y).card ≤ ↑(candidates G L parts f S y).card) (hvC : v ∈ candidates G L parts f S x) (hvS : v ∉ Finset.image f S) (hgood : ∀ y ∉ insert x S, L.Adj x y → d * ↑(candidates G L parts f S y).card ≤ ↑{w ∈ candidates G L parts f S y | G.Adj v w}.card) : Set.InjOn (Function.update f x v) ↑(insert x S) ∧ (∀ z ∈ insert x S, Function.update f x v z ∈ parts z) ∧ (∀ a ∈ insert x S, ∀ b ∈ insert x S, L.Adj a b → G.Adj (Function.update f x v a) (Function.update f x v b)) ∧ ∀ y ∉ insert x S, d ^ (insert x S).card * ↑(parts y).card ≤ ↑(candidates G L parts (Function.update f x v) (insert x S) y).card

An admissible new image extends a partial embedding and preserves the lower bounds on all remaining candidate sets. The density argument that produces an admissible image is kept in the respective existence and counting lemmas.