Documentation

LeanPool.BollobasNikiforov.Kernel.Signs

Sign lemmas for the kernel auxiliaries P and Z #

The expansions and nonnegativity statements for P and Z in docs/sol.tex §3 (eq:functions, after eq:factor).

Truncated squares #

source
theorem BollobasNikiforov.truncSq_nonneg (ti x : ℝ) :
0 ≤ truncSq ti x
source
theorem BollobasNikiforov.truncSq_eq_zero {ti x : ℝ} (h : x ≤ ti) :
truncSq ti x = 0
source
theorem BollobasNikiforov.truncSq_eq_sq {ti x : ℝ} (h : ti ≤ x) :
truncSq ti x = (x - ti) ^ 2
source
theorem BollobasNikiforov.h_nonneg {k : ℕ} (t q : Fin k → ℝ) (hq : ∀ (i : Fin k), 0 < q i) (x : ℝ) :
0 ≤ h t q x

KR14: Z ≥ 0 #

source
theorem BollobasNikiforov.Z_nonneg {k : ℕ} (t q : Fin k → ℝ) (γ : ℝ) (hq : ∀ (i : Fin k), 0 < q i) (hγ : 0 < γ) {x : ℝ} (_hx : 0 ≤ x) :
0 ≤ Z t q γ x

Z(x) = γ x² + (γ + a₀) h(x) is nonnegative for x ≥ 0.

Pairwise summation helper #

source
theorem BollobasNikiforov.sum_add_swap_lt {k : ℕ} (f : Fin k → Fin k → ℝ) (hf : ∀ (i : Fin k), f i i = 0) :
∑ i : Fin k, ∑ j : Fin k, f i j = ∑ i : Fin k, ∑ j : Fin k with i < j, (f i j + f j i)

Split a vanishing-diagonal double sum into strictly upper-triangular pairs.

KR15: expansion of P #

source
theorem BollobasNikiforov.m_one {k : ℕ} (t q : Fin k → ℝ) :
m t q 1 = ∑ i : Fin k, q i * t i
source
theorem BollobasNikiforov.P_expand {k : ℕ} (t q : Fin k → ℝ) (x : ℝ) :
P t q x = a0 t q * x + ∑ i : Fin k, q i * t i * (x ^ 2 - truncSq (t i) x) + ∑ i : Fin k, ∑ j : Fin k with i < j, q i * q j * (t j - t i) * (truncSq (t i) x - truncSq (t j) x)

Algebraic expansion of P into a linear term, a sum of truncated-square defects, and a pairwise increment.

KR16: each summand of P is nonnegative #

source
theorem BollobasNikiforov.sq_sub_truncSq_nonneg {ti x : ℝ} (hx : 0 ≤ x) (hti : 0 < ti) :
0 ≤ x ^ 2 - truncSq ti x

For x ≥ 0 and 0 < tᵢ, one has 0 ≤ x² - (x - tᵢ)₊².

source
theorem BollobasNikiforov.truncSq_sub_truncSq_nonneg {ti tj x : ℝ} (_hx : 0 ≤ x) (_hti : 0 < ti) (htij : ti ≤ tj) :
0 ≤ truncSq ti x - truncSq tj x

For x ≥ 0 and 0 < tᵢ ≤ tⱼ, the truncated squares are antitone in the threshold.

KR17: P ≥ 0 #

source
theorem BollobasNikiforov.P_nonneg {k : ℕ} (t q : Fin k → ℝ) (hq : ∀ (i : Fin k), 0 < q i) (ht : ∀ (i : Fin k), 0 < t i) (hmono : Monotone t) {x : ℝ} (hx : 0 ≤ x) :
0 ≤ P t q x

P(x) ≥ 0 for x ≥ 0 when the nodes are positive and nondecreasing and the weights are positive.