The γ = 0 perturbation

If configγ s t ρ x = 0, enlarge the configuration by a new vector y* = √ε • (x*, 1) with x* strictly to the right of every t i and ε > 0. Every new H i is then positive, hence the enlarged γ is positive (SC19). The principal submatrix of M on the original indices differs from the original M only by diagonal O(ε) Laplacian terms coming from edges to y*, and therefore converges as ε ↓ 0 (SC20). Closedness of the CP cone upgrades SC18 on the enlargements to CP of the original M, including the case p = 0 (SC21).

SC19 — vanishing H i when γ = 0

theorem BollobasNikiforov.configH_eq_zero_of_configγ_eq_zero {k p : ℕ} {s t : Fin k → ℝ} {ρ x : Fin p → ℝ} (hs : ∀ (i : Fin k), 0 < s i) (hρ : ∀ (j : Fin p), 0 < ρ j) (hγ : configγ s t ρ x = 0) (i : Fin k) : configH t ρ x i = 0

Original γ = 0 forces each summand s i * H i / d i to vanish.

Canonical abscissa x*

noncomputable def BollobasNikiforov.configXstar {k : ℕ} (t : Fin k → ℝ) : ℝ

If k = 0, take x* = 0; if k ≥ 1, take x* = (max t i) + 1.

Equations

• BollobasNikiforov.configXstar x = 0
• BollobasNikiforov.configXstar t_2 = Finset.univ.sup' ⋯ t_2 + 1

theorem BollobasNikiforov.configXstar_zero (t : Fin 0 → ℝ) : configXstar t = 0

theorem BollobasNikiforov.configXstar_succ {n : ℕ} (t : Fin (n + 1) → ℝ) : configXstar t = Finset.univ.sup' ⋯ t + 1

theorem BollobasNikiforov.configXstar_nonneg {k : ℕ} {t : Fin k → ℝ} (ht : ∀ (i : Fin k), 0 < t i) : 0 ≤ configXstar t

theorem BollobasNikiforov.lt_configXstar {k : ℕ} (t : Fin k → ℝ) (i : Fin k) : t i < configXstar t

Enlarged weights and abscissae

def BollobasNikiforov.configExtendρ {p : ℕ} (ρ : Fin p → ℝ) (ε : ℝ) : Fin (p + 1) → ℝ

Extend ρ by a last coordinate ε.

Equations

• BollobasNikiforov.configExtendρ ρ ε = Fin.snoc ρ ε

def BollobasNikiforov.configExtendx {p : ℕ} (x : Fin p → ℝ) (xstar : ℝ) : Fin (p + 1) → ℝ

Extend x by a last coordinate x*.

Equations

• BollobasNikiforov.configExtendx x xstar = Fin.snoc x xstar

@[simp]

theorem BollobasNikiforov.configExtendρ_castSucc {p : ℕ} (ρ : Fin p → ℝ) (ε : ℝ) (j : Fin p) : configExtendρ ρ ε j.castSucc = ρ j

@[simp]

theorem BollobasNikiforov.configExtendρ_last {p : ℕ} (ρ : Fin p → ℝ) (ε : ℝ) : configExtendρ ρ ε (Fin.last p) = ε

@[simp]

theorem BollobasNikiforov.configExtendx_castSucc {p : ℕ} (x : Fin p → ℝ) (xstar : ℝ) (j : Fin p) : configExtendx x xstar j.castSucc = x j

@[simp]

theorem BollobasNikiforov.configExtendx_last {p : ℕ} (x : Fin p → ℝ) (xstar : ℝ) : configExtendx x xstar (Fin.last p) = xstar

theorem BollobasNikiforov.configExtendρ_pos {p : ℕ} {ρ : Fin p → ℝ} (hρ : ∀ (j : Fin p), 0 < ρ j) {ε : ℝ} (hε : 0 < ε) (j : Fin (p + 1)) : 0 < configExtendρ ρ ε j

theorem BollobasNikiforov.configExtendx_nonneg {p : ℕ} {x : Fin p → ℝ} (hx : ∀ (j : Fin p), 0 ≤ x j) {xstar : ℝ} (hxstar : 0 ≤ xstar) (j : Fin (p + 1)) : 0 ≤ configExtendx x xstar j

Embedding ConfigIdx k p ↪ ConfigIdx k (p + 1)

def BollobasNikiforov.configIdxEmbed {k p : ℕ} (α : ConfigIdx k p) : ConfigIdx k (p + 1)

Keep z₀, each z i, and the original y j (the latter via Fin.castSucc).

Equations

• One or more equations did not get rendered due to their size.

theorem BollobasNikiforov.configIdxEmbed_z0 {k p : ℕ} : configIdxEmbed idxZ0 = idxZ0

theorem BollobasNikiforov.configIdxEmbed_z {k p : ℕ} (i : Fin k) : configIdxEmbed (idxZ i) = idxZ i

theorem BollobasNikiforov.configIdxEmbed_y {k p : ℕ} (j : Fin p) : configIdxEmbed (idxY j) = idxY j.castSucc

theorem BollobasNikiforov.configIdxEmbed_val {k p : ℕ} (α : ConfigIdx k p) : ↑(configIdxEmbed α) = ↑α

theorem BollobasNikiforov.configIdxEmbed_lt_iff {k p : ℕ} {α β : ConfigIdx k p} : configIdxEmbed α < configIdxEmbed β ↔ α < β

theorem BollobasNikiforov.configIdxEmbed_injective {k p : ℕ} : Function.Injective configIdxEmbed

theorem BollobasNikiforov.configIdxEmbed_lt_idxY_last {k p : ℕ} (α : ConfigIdx k p) : configIdxEmbed α < idxY (Fin.last p)

Original vectors are unchanged

theorem BollobasNikiforov.yVec_extend_castSucc {p : ℕ} (ρ x : Fin p → ℝ) (ε xstar : ℝ) (j : Fin p) : yVec (configExtendρ ρ ε) (configExtendx x xstar) j.castSucc = yVec ρ x j

theorem BollobasNikiforov.configVec_extend_embed {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (ε xstar : ℝ) (α : ConfigIdx k p) : configVec s t (configExtendρ ρ ε) (configExtendx x xstar) (configIdxEmbed α) = configVec s t ρ x α

theorem BollobasNikiforov.Xconfig_extend_submatrix {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (ε xstar : ℝ) : (Xconfig s t (configExtendρ ρ ε) (configExtendx x xstar)).submatrix configIdxEmbed configIdxEmbed = Xconfig s t ρ x

The Gram matrix among original indices is independent of ε.

theorem BollobasNikiforov.Xconfig_embed_ystar {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (ε xstar : ℝ) (α : ConfigIdx k p) : Xconfig s t (configExtendρ ρ ε) (configExtendx x xstar) (configIdxEmbed α) (idxY (Fin.last p)) = √ε * (configVec s t ρ x α 0 * xstar + configVec s t ρ x α 1)

SC19 — positivity of the enlarged H i and γ

theorem BollobasNikiforov.configH_extend {k p : ℕ} (t : Fin k → ℝ) (ρ x : Fin p → ℝ) (ε xstar : ℝ) (i : Fin k) : configH t (configExtendρ ρ ε) (configExtendx x xstar) i = configH t ρ x i + ε * max (xstar - t i) 0 ^ 2

theorem BollobasNikiforov.configH_extend_pos {k p : ℕ} (t : Fin k → ℝ) {ρ : Fin p → ℝ} (hρ : ∀ (j : Fin p), 0 < ρ j) (x : Fin p → ℝ) {ε : ℝ} (hε : 0 < ε) {xstar : ℝ} (hxstar : ∀ (i : Fin k), t i < xstar) (i : Fin k) : 0 < configH t (configExtendρ ρ ε) (configExtendx x xstar) i

Each new H i is strictly positive: (x* - t i)_+ > 0 and ε > 0.

theorem BollobasNikiforov.configγ_extend_pos {k p : ℕ} [NeZero k] (s t : Fin k → ℝ) {ρ : Fin p → ℝ} (hρ : ∀ (j : Fin p), 0 < ρ j) (x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) {ε : ℝ} (hε : 0 < ε) {xstar : ℝ} (hxstar : ∀ (i : Fin k), t i < xstar) : 0 < configγ s t (configExtendρ ρ ε) (configExtendx x xstar)

The enlarged configuration has γ > 0 (needs at least one z-index).

theorem BollobasNikiforov.configH_extend_configXstar_pos {k p : ℕ} (t : Fin k → ℝ) {ρ : Fin p → ℝ} (hρ : ∀ (j : Fin p), 0 < ρ j) (x : Fin p → ℝ) {ε : ℝ} (hε : 0 < ε) (i : Fin k) : 0 < configH t (configExtendρ ρ ε) (configExtendx x (configXstar t)) i

theorem BollobasNikiforov.configγ_extend_configXstar_pos {k p : ℕ} [NeZero k] (s t : Fin k → ℝ) {ρ : Fin p → ℝ} (hρ : ∀ (j : Fin p), 0 < ρ j) (x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) {ε : ℝ} (hε : 0 < ε) : 0 < configγ s t (configExtendρ ρ ε) (configExtendx x (configXstar t))

SC20 — principal submatrices of M

theorem BollobasNikiforov.sum_configIdx_extend {k p : ℕ} (f : ConfigIdx k (p + 1) → ℝ) : ∑ α : ConfigIdx k (p + 1), f α = ∑ α : ConfigIdx k p, f (configIdxEmbed α) + f (idxY (Fin.last p))

theorem BollobasNikiforov.MX_extend_submatrix_of_ne {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (ε xstar : ℝ) {α β : ConfigIdx k p} (hne : α ≠ β) : M (Xconfig s t (configExtendρ ρ ε) (configExtendx x xstar)) (configIdxEmbed α) (configIdxEmbed β) = M (Xconfig s t ρ x) α β

Off-diagonals of M among original indices ignore the new vertex.

theorem BollobasNikiforov.MX_extend_submatrix_diag_add {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (ε xstar : ℝ) (α : ConfigIdx k p) : M (Xconfig s t (configExtendρ ρ ε) (configExtendx x xstar)) (configIdxEmbed α) (configIdxEmbed α) = M (Xconfig s t ρ x) α α + if Xconfig s t (configExtendρ ρ ε) (configExtendx x xstar) (configIdxEmbed α) (idxY (Fin.last p)) < 0 then Xconfig s t (configExtendρ ρ ε) (configExtendx x xstar) (configIdxEmbed α) (idxY (Fin.last p)) ^ 2 else 0

Diagonals pick up one extra Laplacian weight from the edge to y*.

theorem BollobasNikiforov.MX_extend_submatrix_diag {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) {ε : ℝ} (hε : 0 < ε) (xstar : ℝ) (α : ConfigIdx k p) : M (Xconfig s t (configExtendρ ρ ε) (configExtendx x xstar)) (configIdxEmbed α) (configIdxEmbed α) = M (Xconfig s t ρ x) α α + if configVec s t ρ x α 0 * xstar + configVec s t ρ x α 1 < 0 then ε * (configVec s t ρ x α 0 * xstar + configVec s t ρ x α 1) ^ 2 else 0

For ε > 0 the extra diagonal term is ε times a constant (hence O(ε)).

theorem BollobasNikiforov.MX_extend_submatrix {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) {ε : ℝ} (hε : 0 < ε) (xstar : ℝ) : (M (Xconfig s t (configExtendρ ρ ε) (configExtendx x xstar))).submatrix configIdxEmbed configIdxEmbed = M (Xconfig s t ρ x) + Matrix.diagonal fun (α : ConfigIdx k p) => if configVec s t ρ x α 0 * xstar + configVec s t ρ x α 1 < 0 then ε * (configVec s t ρ x α 0 * xstar + configVec s t ρ x α 1) ^ 2 else 0

M of the enlargement, restricted to original indices, is the original M plus a diagonal of order ε. (M of the large matrix then submatrix is not M of the Gram submatrix, because Laplacian edges to y* affect diagonals; continuous_M would only recover M of that submatrix.)

theorem BollobasNikiforov.tendsto_MX_extend_submatrix {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (xstar : ℝ) : Filter.Tendsto (fun (ε : ℝ) => (M (Xconfig s t (configExtendρ ρ ε) (configExtendx x xstar))).submatrix configIdxEmbed configIdxEmbed) (nhdsWithin 0 (Set.Ioi 0)) (nhds (M (Xconfig s t ρ x)))

As ε ↓ 0, the principal submatrix of M(X_ε) converges to M(X).

theorem BollobasNikiforov.tendsto_MX_extend_submatrix_configXstar {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) : Filter.Tendsto (fun (ε : ℝ) => (M (Xconfig s t (configExtendρ ρ ε) (configExtendx x (configXstar t)))).submatrix configIdxEmbed configIdxEmbed) (nhdsWithin 0 (Set.Ioi 0)) (nhds (M (Xconfig s t ρ x)))

SC21 — γ = 0 and p = 0 by closedness

theorem BollobasNikiforov.isCompletelyPositive_MX_extend {k p : ℕ} [NeZero k] (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (ht : ∀ (i : Fin k), 0 < t i) (hmono : Monotone t) (hρ : ∀ (j : Fin p), 0 < ρ j) (hx : ∀ (j : Fin p), 0 ≤ x j) {ε : ℝ} (hε : 0 < ε) : IsCompletelyPositive (M (Xconfig s t (configExtendρ ρ ε) (configExtendx x (configXstar t))))

theorem BollobasNikiforov.isCompletelyPositive_MX_extend_submatrix {k p : ℕ} [NeZero k] (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (ht : ∀ (i : Fin k), 0 < t i) (hmono : Monotone t) (hρ : ∀ (j : Fin p), 0 < ρ j) (hx : ∀ (j : Fin p), 0 ≤ x j) {ε : ℝ} (hε : 0 < ε) : IsCompletelyPositive ((M (Xconfig s t (configExtendρ ρ ε) (configExtendx x (configXstar t)))).submatrix configIdxEmbed configIdxEmbed)

theorem BollobasNikiforov.isCompletelyPositive_M_Xconfig_of_configγ_eq_zero {k p : ℕ} [NeZero k] (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (ht : ∀ (i : Fin k), 0 < t i) (hmono : Monotone t) (hρ : ∀ (j : Fin p), 0 < ρ j) (hx : ∀ (j : Fin p), 0 ≤ x j) (_hγ : configγ s t ρ x = 0) : IsCompletelyPositive (M (Xconfig s t ρ x))

If γ = 0, the original M is completely positive: enlarge, apply SC18, restrict to original indices, and pass to the limit by closedness of CP.

theorem BollobasNikiforov.configH_eq_zero_of_p_eq_zero {k : ℕ} (t : Fin k → ℝ) (ρ x : Fin 0 → ℝ) (i : Fin k) : configH t ρ x i = 0

theorem BollobasNikiforov.configγ_eq_zero_of_p_eq_zero {k : ℕ} (s t : Fin k → ℝ) (ρ x : Fin 0 → ℝ) : configγ s t ρ x = 0

theorem BollobasNikiforov.isCompletelyPositive_M_Xconfig_of_p_eq_zero {k : ℕ} [NeZero k] (s t : Fin k → ℝ) (ρ x : Fin 0 → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (ht : ∀ (i : Fin k), 0 < t i) (hmono : Monotone t) : IsCompletelyPositive (M (Xconfig s t ρ x))

The case p = 0 has H i = 0 for every i, hence γ = 0.