Deterministic analysis of the depth-first search (EPI-3)

The deterministic half of the proofs of Krivelevich–Sudakov, Theorem 1, part 2, and Theorem 2 (The phase transition in random graphs: a simple proof, Random Structures & Algorithms 43 (2013), arXiv:1201.6529): consequences of the properties of the search (Epidemics.GiantDFS) for an arbitrary sequence of answers l, with X = l.count true positive answers.

• card_mul_card_le: if all pairs between disjoint sets A and B have been queried, then |A| |B| is at most the number of queries.
• three_mul_explored_lt: "|S| < n/3 at time N₀" (proof of Theorem 1): if |S ∪ U| reached n / 3, then at the first such time |S| |T| would exceed the number of queries.
• le_length_stack: "|U| ≥ ε² n / 5" (proof of Theorem 1): otherwise |S| |T| would exceed the number of queries.
• exists_epoch_start: the current epoch started at a time τ when U was empty, so the explored set D had all its pairs with V ∖ D queried (proof of Theorem 2).
• exists_path_of_stack, card_comp_le_ncard: on the edge coins ω, the stack is a path of perc ⊤ ω and the current epoch lies in one connected component.

noncomputable def Epidemics.DFS.explored (V : Type u_2) [Fintype V] [DecidableEq V] (l : List Bool) : ℕ

|S ∪ U| after the answers l: the explored vertices.

Equations

• Epidemics.DFS.explored V l = ((Epidemics.DFS.ofAnswers V l).done ∪ (Epidemics.DFS.ofAnswers V l).stack.toFinset).card

theorem Epidemics.DFS.card_mul_card_le {V : Type u_1} {A B : Finset V} (hAB : Disjoint A B) {Q : Finset (Sym2 V)} (h : ∀ a ∈ A, ∀ b ∈ B, s(a, b) ∈ Q) : A.card * B.card ≤ Q.card

If all pairs between the disjoint sets A and B lie in Q, then |A| |B| ≤ |Q|.

theorem Epidemics.DFS.card_unvisited {V : Type u_1} [Fintype V] [DecidableEq V] (s : State V) : s.unvisited.card = Fintype.card V - (s.done ∪ s.stack.toFinset).card

theorem Epidemics.DFS.explored_le {V : Type u_1} [Fintype V] [DecidableEq V] (l : List Bool) : explored V l ≤ Fintype.card V

theorem Epidemics.DFS.card_done_add_length {V : Type u_1} [Fintype V] [DecidableEq V] (l : List Bool) : (ofAnswers V l).done.card + (ofAnswers V l).stack.length = explored V l

theorem Epidemics.DFS.explored_take_le {V : Type u_1} [Fintype V] [DecidableEq V] (l : List Bool) (j : ℕ) : explored V (List.take j l) ≤ explored V l

explored grows along prefixes.

theorem Epidemics.DFS.card_done_mul_card_unvisited_le {V : Type u_1} [Fintype V] [DecidableEq V] (l : List Bool) (hl : l.length ≤ (Fintype.card V).choose 2) : (ofAnswers V l).done.card * (ofAnswers V l).unvisited.card ≤ l.length

|S| |T| is at most the number of queries.

theorem Epidemics.DFS.count_take_le (l : List Bool) (j : ℕ) : List.count true (List.take j l) ≤ List.count true l

theorem Epidemics.DFS.three_mul_explored_lt {V : Type u_1} [Fintype V] [DecidableEq V] (l : List Bool) (hl : l.length ≤ (Fintype.card V).choose 2) (hn : 4 ≤ Fintype.card V) (h : ↑l.length < (↑(Fintype.card V) / 3 - 1 - ↑(List.count true l)) * ((2 * ↑(Fintype.card V) - 5) / 3)) : 3 * explored V l < Fintype.card V

|S ∪ U| < n/3 at time |l| (Krivelevich–Sudakov, proof of Theorem 1): at the first time when 3 |S ∪ U| ≥ n, we have |S ∪ U| ≤ (n + 5)/3 (it grows by at most 2 per query), so |S| ≥ n/3 - 1 - X and |T| ≥ (2n - 5)/3, and all the pairs between S and T have been queried.

theorem Epidemics.DFS.le_length_stack {V : Type u_1} [Fintype V] [DecidableEq V] (l : List Bool) (hl : l.length ≤ (Fintype.card V).choose 2) (h3 : 3 * explored V l < Fintype.card V) {Xlo L : ℝ} (hX : Xlo ≤ ↑(List.count true l)) (hL : L ≤ Xlo) (h1 : ↑l.length < (Xlo - L) * (↑(Fintype.card V) - Xlo)) (h2 : ↑l.length < (↑(Fintype.card V) / 3 - L) * (2 * ↑(Fintype.card V) / 3)) : L ≤ ↑(ofAnswers V l).stack.length

A long stack (Krivelevich–Sudakov, proof of Theorem 1): if 3 |S ∪ U| < n, the number of positive answers is at least Xlo ≥ L, and both (Xlo - L)(n - Xlo) and (n/3 - L)(2n/3) exceed the number of queries, then |U| ≥ L. (Otherwise |S| ≥ |S ∪ U| - L with Xlo ≤ |S ∪ U| < n/3, and by concavity |S| |T| would exceed the number of queries.)

theorem Epidemics.DFS.exists_epoch_start {V : Type u_1} [Fintype V] [DecidableEq V] (l : List Bool) (hl : l.length ≤ (Fintype.card V).choose 2) (hT : (ofAnswers V l).unvisited.Nonempty) : ∃ τ ≤ l.length, List.count true (List.drop τ l) ≤ (ofAnswers V l).comp.card ∧ (τ = 0 ∨ ∃ (d : ℕ), List.count true (List.take τ l) ≤ d ∧ d ≤ explored V l ∧ d * (Fintype.card V - d) ≤ τ)

The start of the current epoch (Krivelevich–Sudakov, proof of Theorem 2): there is a time τ ≤ |l| such that the positive answers after τ all lie in the current epoch and, unless τ = 0, at time τ an explored set D with |D| ≥ ∑_{i<τ} Xᵢ, |D| ≤ |S ∪ U| had all its pairs with V ∖ D queried, so that |D| (n - |D|) ≤ τ.

theorem Epidemics.DFS.le_card_comp {V : Type u_1} [Fintype V] [DecidableEq V] (l : List Bool) (hl : l.length ≤ (Fintype.card V).choose 2) (h3 : 3 * explored V l < Fintype.card V) {t₁ : ℕ} {p δ : ℝ} (hp : 0 ≤ p) (hδ0 : 0 ≤ δ) (hδ1 : δ ≤ 1) (hlow : ∀ (t : ℕ), t₁ ≤ t → t ≤ l.length → (1 - δ) * (↑t * p) ≤ ↑(List.count true (List.take t l))) (hcontr : 1 < (1 - δ) * p * (↑(Fintype.card V) - ↑l.length * p)) : ↑(List.count true l) - ↑(List.count true (List.take t₁ l)) ≤ ↑(ofAnswers V l).comp.card

A large epoch (Krivelevich–Sudakov, proof of Theorem 2): suppose 3 |S ∪ U| < n, at least (1 - δ) t p of the first t answers are positive for every t₁ ≤ t ≤ |l|, and (1 - δ) p (n - |l| p) > 1. Then the current epoch started by time t₁ (an earlier start at time τ > t₁ would give an explored set D with (1 - δ) τ p ≤ |D| < n/3 and |D| (n - |D|) ≤ τ < (1 - δ) τ p (n - |l| p)), so it contains all the positive answers after t₁.

On the edge coins

theorem Epidemics.DFS.adj_of_mem_found {V : Type u_1} [Fintype V] [DecidableEq V] (e₀ : Sym2 V) (ω : Sym2 V → Bool) (t : ℕ) {u v : V} (h : s(u, v) ∈ (ofAnswers V (queryAnswers (nextQuery e₀) ω t)).found) : (perc ⊤ ω).Adj u v

The found pairs are open edges of perc ⊤ ω.

theorem Epidemics.DFS.fromEdgeSet_found_le {V : Type u_1} [Fintype V] [DecidableEq V] (e₀ : Sym2 V) (ω : Sym2 V → Bool) (t : ℕ) : SimpleGraph.fromEdgeSet ↑(ofAnswers V (queryAnswers (nextQuery e₀) ω t)).found ≤ perc ⊤ ω

theorem Epidemics.DFS.exists_walk_of_isChain {V : Type u_1} {G : SimpleGraph V} (a : V) (L : List V) : List.IsChain G.Adj (a :: L) → ∃ (b : V) (q : G.Walk a b), q.support = a :: L

A chain of adjacent vertices is the support of a walk.

theorem Epidemics.DFS.exists_path_of_stack {V : Type u_1} [Fintype V] [DecidableEq V] (e₀ : Sym2 V) (ω : Sym2 V → Bool) (t : ℕ) (hne : (ofAnswers V (queryAnswers (nextQuery e₀) ω t)).stack ≠ []) : ∃ (u : V) (v : V) (q : (perc ⊤ ω).Walk u v), q.IsPath ∧ q.length + 1 = (ofAnswers V (queryAnswers (nextQuery e₀) ω t)).stack.length

The stack is a path of perc ⊤ ω with |U| - 1 edges.

theorem Epidemics.DFS.card_comp_le_ncard {V : Type u_1} [Fintype V] [DecidableEq V] (e₀ : Sym2 V) (ω : Sym2 V → Bool) (t : ℕ) {u : V} (hu : u ∈ (ofAnswers V (queryAnswers (nextQuery e₀) ω t)).comp) : (ofAnswers V (queryAnswers (nextQuery e₀) ω t)).comp.card ≤ ((perc ⊤ ω).connectedComponentMk u).supp.ncard

The current epoch lies in one connected component of perc ⊤ ω.