Truncated and unrestricted square kernels

This file records the elementary algebraic facts about the kernels (t - a)² and (t - a)₊² used for total nonnegativity. The positive part is max · 0.

def BollobasNikiforov.unrestrictedSquare {ι : Type u_1} {κ : Type u_2} (a : ι → ℝ) (t : κ → ℝ) : Matrix ι κ ℝ

The unrestricted square kernel (i, j) ↦ (t j - a i)².

Equations

• BollobasNikiforov.unrestrictedSquare a t i j = (t j - a i) ^ 2

def BollobasNikiforov.truncatedSquare {ι : Type u_1} {κ : Type u_2} (a : ι → ℝ) (t : κ → ℝ) : Matrix ι κ ℝ

The truncated square kernel (i, j) ↦ (t j - a i)₊².

Equations

• BollobasNikiforov.truncatedSquare a t i j = max (t j - a i) 0 ^ 2

@[simp]

theorem BollobasNikiforov.unrestrictedSquare_apply {ι : Type u_1} {κ : Type u_2} (a : ι → ℝ) (t : κ → ℝ) (i : ι) (j : κ) : unrestrictedSquare a t i j = (t j - a i) ^ 2

@[simp]

theorem BollobasNikiforov.truncatedSquare_apply {ι : Type u_1} {κ : Type u_2} (a : ι → ℝ) (t : κ → ℝ) (i : ι) (j : κ) : truncatedSquare a t i j = max (t j - a i) 0 ^ 2

def BollobasNikiforov.unrestrictedSquareLeft {ι : Type u_1} (a : ι → ℝ) : Matrix ι (Fin 3) ℝ

Row factor with columns (1, a, a²).

Equations

• BollobasNikiforov.unrestrictedSquareLeft a i = ![1, a i, a i ^ 2]

def BollobasNikiforov.unrestrictedSquareRight {κ : Type u_2} (t : κ → ℝ) : Matrix (Fin 3) κ ℝ

Column factor with rows (t², -2 t, 1).

Equations

• BollobasNikiforov.unrestrictedSquareRight t k j = ![t j ^ 2, -2 * t j, 1] k

theorem BollobasNikiforov.unrestrictedSquare_eq_sum_vecMulVec {ι : Type u_1} {κ : Type u_2} (a : ι → ℝ) (t : κ → ℝ) : unrestrictedSquare a t = ((Matrix.vecMulVec (fun (i : ι) => a i ^ 2) fun (x : κ) => 1) + Matrix.vecMulVec (fun (x : ι) => 1) fun (j : κ) => t j ^ 2) + -2 • Matrix.vecMulVec a t

TN05. The identity (t - a)² = t² + a² - 2 t a as a three-term rank-one expansion.

theorem BollobasNikiforov.unrestrictedSquare_eq_mul {ι : Type u_1} {κ : Type u_2} (a : ι → ℝ) (t : κ → ℝ) : unrestrictedSquare a t = unrestrictedSquareLeft a * unrestrictedSquareRight t

TN05. Factorization against (1, a, a²) and (t², -2 t, 1).

theorem BollobasNikiforov.unrestrictedSquare_rank_le {ι : Type u_1} {κ : Type u_2} [Fintype κ] (a : ι → ℝ) (t : κ → ℝ) : (unrestrictedSquare a t).rank ≤ 3

TN05. The unrestricted square matrix has rank at most three.

theorem BollobasNikiforov.unrestrictedSquare_submatrix_eq_mul {ι : Type u_1} {κ : Type u_2} (a : ι → ℝ) (t : κ → ℝ) {r : Type u_3} {c : Type u_4} (I : r → ι) (J : c → κ) : (unrestrictedSquare a t).submatrix I J = (unrestrictedSquareLeft a).submatrix I id * (unrestrictedSquareRight t).submatrix id J

theorem BollobasNikiforov.unrestrictedSquare_submatrix_det_eq_zero {ι : Type u_1} {κ : Type u_2} {r : ℕ} (hr : 4 ≤ r) (a : ι → ℝ) (t : κ → ℝ) (I : Fin r → ι) (J : Fin r → κ) : ((unrestrictedSquare a t).submatrix I J).det = 0

TN06. Every r × r minor of unrestricted squares with r ≥ 4 vanishes.

theorem BollobasNikiforov.unrestricted_sq_two_eq (a b t u : ℝ) : (t - a) ^ 2 * (u - b) ^ 2 - (u - a) ^ 2 * (t - b) ^ 2 = (t - u) * (a - b) * ((t - a) * (u - b) + (u - a) * (t - b))

Algebraic factorization of the 2×2 minor of unrestricted squares (TN07).

theorem BollobasNikiforov.unrestricted_sq_two_nonneg {a b t u : ℝ} (hab : a ≤ b) (hbt : b ≤ t) (htu : t ≤ u) : 0 ≤ (t - a) ^ 2 * (u - b) ^ 2 - (u - a) ^ 2 * (t - b) ^ 2

TN07. In the unrestricted chamber a ≤ b ≤ t ≤ u, the 2×2 minor is nonnegative. The remaining factor (t-a)(u-b)+(u-a)(t-b) is a sum of nonnegative terms in this chamber.

theorem BollobasNikiforov.unrestrictedSquare_det_two {a t : Fin 2 → ℝ} (ha : a 0 ≤ a 1) (ht : t 0 ≤ t 1) (hbt : a 1 ≤ t 0) : 0 ≤ (unrestrictedSquare a t).det

theorem BollobasNikiforov.unrestrictedSquare_det_fin_three (a t : Fin 3 → ℝ) : (unrestrictedSquare a t).det = 2 * (a 1 - a 0) * (a 2 - a 1) * (a 2 - a 0) * (t 1 - t 0) * (t 2 - t 1) * (t 2 - t 0)

Closed form for the 3×3 minor of unrestricted squares.

theorem BollobasNikiforov.unrestrictedSquare_det_fin_three_nonneg {a t : Fin 3 → ℝ} (ha : Monotone a) (ht : Monotone t) : 0 ≤ (unrestrictedSquare a t).det

TN08. The 3×3 minor of unrestricted squares is nonnegative on nondecreasing arguments.

theorem BollobasNikiforov.truncated_sq_two_nonneg {a b t u : ℝ} (hab : a ≤ b) (htu : t ≤ u) : 0 ≤ max (t - a) 0 ^ 2 * max (u - b) 0 ^ 2 - max (u - a) 0 ^ 2 * max (t - b) 0 ^ 2

TN09. Two-by-two minor of truncated squares.

theorem BollobasNikiforov.truncatedSquare_det_two {a t : Fin 2 → ℝ} (ha : a 0 ≤ a 1) (ht : t 0 ≤ t 1) : 0 ≤ (truncatedSquare a t).det

theorem BollobasNikiforov.truncated_sq_col_zero {k : ℕ} [NeZero k] {a t : Fin k → ℝ} (ha : Monotone a) (h : t 0 < a 0) (i : Fin k) : max (t 0 - a i) 0 = 0

TN10. If t 0 < a 0 and a is nondecreasing, every truncated entry in column 0 vanishes.

theorem BollobasNikiforov.truncatedSquare_column_zero {k : ℕ} [NeZero k] {a t : Fin k → ℝ} (ha : Monotone a) (h : t 0 < a 0) (i : Fin k) : truncatedSquare a t i 0 = 0

theorem BollobasNikiforov.truncatedSquare_det_eq_zero_of_first_col {k r : ℕ} [NeZero k] [NeZero r] {a t : Fin k → ℝ} (ha : Monotone a) (h : t 0 < a 0) (I J : Fin r → Fin k) (hJ : J 0 = 0) : ((truncatedSquare a t).submatrix I J).det = 0

TN10. Every square minor that includes column 0 vanishes.

theorem BollobasNikiforov.truncatedSquare_eq_zero_of_le {a t : ℝ} (h : t ≤ a) : max (t - a) 0 ^ 2 = 0

theorem BollobasNikiforov.truncatedSquare_eq_unrestricted_of_le {a t : ℝ} (h : a ≤ t) : max (t - a) 0 ^ 2 = (t - a) ^ 2

def BollobasNikiforov.finLast (k : ℕ) [NeZero k] : Fin k

The last index of a nonempty Fin k.

Equations

• BollobasNikiforov.finLast k = ⟨k - 1, ⋯⟩

theorem BollobasNikiforov.le_finLast {k : ℕ} [NeZero k] (i : Fin k) : i ≤ finLast k

theorem BollobasNikiforov.truncatedSquare_eq_unrestrictedSquare {k : ℕ} [NeZero k] {a t : Fin k → ℝ} (ha : Monotone a) (ht : Monotone t) (h : a (finLast k) ≤ t 0) : truncatedSquare a t = unrestrictedSquare a t

TN11. In the unrestricted chamber every truncated entry is unrestricted.

theorem BollobasNikiforov.truncatedSquare_submatrix_eq {r c n m : ℕ} (a : Fin r → ℝ) (t : Fin c → ℝ) (I : Fin n → Fin r) (J : Fin m → Fin c) : (truncatedSquare a t).submatrix I J = truncatedSquare (a ∘ I) (t ∘ J)

theorem BollobasNikiforov.unrestrictedSquare_submatrix_eq {r c n m : ℕ} (a : Fin r → ℝ) (t : Fin c → ℝ) (I : Fin n → Fin r) (J : Fin m → Fin c) : (unrestrictedSquare a t).submatrix I J = unrestrictedSquare (a ∘ I) (t ∘ J)

theorem BollobasNikiforov.monotone_comp_of_monotone {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Preorder α] [Preorder β] [Preorder γ] {f : β → γ} {g : α → β} (hf : Monotone f) (hg : Monotone g) : Monotone (f ∘ g)

theorem BollobasNikiforov.monotone_of_strictMono {α : Type u_3} {β : Type u_4} [LinearOrder α] [Preorder β] {f : α → β} (hf : StrictMono f) : Monotone f

theorem BollobasNikiforov.truncatedSquare_det_one {a t : Fin 1 → ℝ} : 0 ≤ (truncatedSquare a t).det

Size-one minors are squares of nonnegative numbers.

theorem BollobasNikiforov.unrestrictedSquare_det_one {a t : Fin 1 → ℝ} : 0 ≤ (unrestrictedSquare a t).det

theorem BollobasNikiforov.unrestrictedSquare_det_nonneg_chamber {n : ℕ} {a t : Fin n → ℝ} (ha : Monotone a) (ht : Monotone t) (hch : n = 0 ∨ ∃ (x : NeZero n), a (finLast n) ≤ t 0) : 0 ≤ (unrestrictedSquare a t).det

Unrestricted dets in the chamber a last ≤ t 0.

theorem BollobasNikiforov.truncatedSquare_unrestricted_chamber_minor_nonneg {k n : ℕ} [NeZero k] {a t : Fin k → ℝ} (ha : Monotone a) (ht : Monotone t) (h : a (finLast k) ≤ t 0) (I J : Fin n → Fin k) (hI : Monotone I) (hJ : Monotone J) : 0 ≤ ((truncatedSquare a t).submatrix I J).det

TN11. Increasing minors of a truncated matrix in the unrestricted chamber.

theorem BollobasNikiforov.truncatedSquare_block_zero {k : ℕ} {a t : Fin k → ℝ} (ha : Monotone a) (ht : Monotone t) {s j0 i j : Fin k} (hj0 : t j0 < a s) (hi : s ≤ i) (hj : j ≤ j0) : truncatedSquare a t i j = 0

TN12. A truncated entry vanishes on and below the diagonal of the staircase.

theorem BollobasNikiforov.truncatedSquare_block_zero_of_le {k : ℕ} {a t : Fin k → ℝ} (ha : Monotone a) (ht : Monotone t) {s j0 i j : Fin k} (hj0 : t j0 ≤ a s) (hi : s ≤ i) (hj : j ≤ j0) : truncatedSquare a t i j = 0

theorem BollobasNikiforov.det_block_triangular_add {m n : ℕ} (M : Matrix (Fin (m + n)) (Fin (m + n)) ℝ) (hz : ∀ (i : Fin n) (j : Fin m), M (Fin.natAdd m i) (Fin.castAdd n j) = 0) : M.det = (M.submatrix (Fin.castAdd n) (Fin.castAdd n)).det * (M.submatrix (Fin.natAdd m) (Fin.natAdd m)).det

Block-triangular determinant after splitting Fin (m + n) as Fin m ⊕ Fin n.

theorem BollobasNikiforov.truncatedSquare_det_eq_zero_of_le_first {n : ℕ} [NeZero n] {a t : Fin n → ℝ} (ha : Monotone a) (h : t 0 ≤ a 0) : (truncatedSquare a t).det = 0

theorem BollobasNikiforov.truncatedSquare_det_three_mixed {a t : Fin 3 → ℝ} (h01a : a 0 ≤ a 1) (h1t : a 1 ≤ t 0) (ht0a2 : t 0 ≤ a 2) (ha2t1 : a 2 ≤ t 1) (ht01 : t 0 ≤ t 1) (ht12 : t 1 ≤ t 2) : 0 ≤ (truncatedSquare a t).det

Mixed 3×3 staircase a 0 ≤ a 1 ≤ t 0 ≤ a 2 ≤ t 1 ≤ t 2.

theorem BollobasNikiforov.truncatedSquare_det_three {a t : Fin 3 → ℝ} (ha : Monotone a) (ht : Monotone t) : 0 ≤ (truncatedSquare a t).det

TN13: truncated squares are totally nonnegative

theorem BollobasNikiforov.truncatedSquare_det_nonneg_of_small_or_chamber {n : ℕ} {a t : Fin n → ℝ} (ha : Monotone a) (ht : Monotone t) (h : n ≤ 3 ∨ (∃ (x : NeZero n), t 0 ≤ a 0) ∨ ∃ (x : NeZero n), a (finLast n) ≤ t 0) : 0 ≤ (truncatedSquare a t).det

Square truncated determinants of size at most three, plus the two vanishing chambers of size at least four.

theorem BollobasNikiforov.truncatedSquare_minor_nonneg_of_small_or_chamber {r c k : ℕ} {a : Fin r → ℝ} {t : Fin c → ℝ} (ha : Monotone a) (ht : Monotone t) (I : Fin k → Fin r) (J : Fin k → Fin c) (hI : Monotone I) (hJ : Monotone J) (h : k ≤ 3 ∨ (∃ (x : NeZero k), t (J 0) ≤ a (I 0)) ∨ ∃ (x : NeZero k), a (I (finLast k)) ≤ t (J 0)) : 0 ≤ ((truncatedSquare a t).submatrix I J).det

TN13 for increasing selections of length at most three, and for every length in the first-column or unrestricted chambers.

theorem BollobasNikiforov.truncatedSquare_isTotallyNonnegative_of_small {r c : ℕ} {a : Fin r → ℝ} {t : Fin c → ℝ} (ha : Monotone a) (ht : Monotone t) (_k : ℕ) : _k ≤ 3 → ∀ (I : Fin _k → Fin r) (J : Fin _k → Fin c), StrictMono I → StrictMono J → 0 ≤ ((truncatedSquare a t).submatrix I J).det

Step kernel, Cauchy–Binet, and the discrete-to-continuous limit (TN13)

noncomputable def BollobasNikiforov.stepKernel {ι : Type u_1} {κ : Type u_2} (a : ι → ℝ) (t : κ → ℝ) : Matrix ι κ ℝ

Indicator kernel H(a,t) = 1_{a ≤ t}.

Equations

• BollobasNikiforov.stepKernel a t i j = if a i ≤ t j then 1 else 0

theorem BollobasNikiforov.stepKernel_apply {ι : Type u_1} {κ : Type u_2} (a : ι → ℝ) (t : κ → ℝ) (i : ι) (j : κ) : stepKernel a t i j = if a i ≤ t j then 1 else 0

theorem BollobasNikiforov.stepKernel_submatrix_eq {r c n m : ℕ} (a : Fin r → ℝ) (t : Fin c → ℝ) (I : Fin n → Fin r) (J : Fin m → Fin c) : (stepKernel a t).submatrix I J = stepKernel (a ∘ I) (t ∘ J)

noncomputable def BollobasNikiforov.stepSupport {n : ℕ} (a t : Fin n → ℝ) (i : Fin n) : Finset (Fin n)

Columns where the i-th step-row is one.

Equations

• BollobasNikiforov.stepSupport a t i = {j : Fin n | a i ≤ t j}

noncomputable def BollobasNikiforov.stepCutoff {n : ℕ} (a t : Fin n → ℝ) (i : Fin n) : ℕ

First column index where a i ≤ t j, or n if the row is zero.

Equations

• BollobasNikiforov.stepCutoff a t i = if h : (BollobasNikiforov.stepSupport a t i).Nonempty then ↑((BollobasNikiforov.stepSupport a t i).min' h) else n

theorem BollobasNikiforov.stepSupport_anti {n : ℕ} {a t : Fin n → ℝ} (ha : Monotone a) {i i' : Fin n} (h : i ≤ i') : stepSupport a t i' ⊆ stepSupport a t i

theorem BollobasNikiforov.stepCutoff_mono {n : ℕ} {a t : Fin n → ℝ} (ha : Monotone a) : Monotone (stepCutoff a t)

theorem BollobasNikiforov.stepKernel_eq_of_cutoff {n : ℕ} {a t : Fin n → ℝ} (ht : Monotone t) (i j : Fin n) : stepKernel a t i j = if stepCutoff a t i ≤ ↑j then 1 else 0

theorem BollobasNikiforov.det_ones_of_le (n : ℕ) : (Matrix.of fun (i j : Fin n) => if i ≤ j then 1 else 0).det = 1

theorem BollobasNikiforov.strictMono_fin_to_nat_ge {n : ℕ} {c : Fin n → ℕ} (hc : StrictMono c) (i : Fin n) : ↑i ≤ c i

theorem BollobasNikiforov.strictMono_fin_to_nat_walk {n : ℕ} {c : Fin (n + 1) → ℕ} (hc : StrictMono c) (i : Fin (n + 1)) (d : ℕ) (hd : ↑i + d < n + 1) : c i + d ≤ c ⟨↑i + d, hd⟩

theorem BollobasNikiforov.strictMono_fin_to_nat_eq {n : ℕ} {c : Fin (n + 1) → ℕ} (hc : StrictMono c) (hbnd : ∀ (i : Fin (n + 1)), c i < n + 1) (i : Fin (n + 1)) : c i = ↑i

theorem BollobasNikiforov.stepKernel_det_nonneg {n : ℕ} {a t : Fin n → ℝ} (ha : Monotone a) (ht : Monotone t) : 0 ≤ (stepKernel a t).det

theorem BollobasNikiforov.stepKernel_isTotallyNonneg {r c : ℕ} {a : Fin r → ℝ} {t : Fin c → ℝ} (ha : Monotone a) (ht : Monotone t) : IsTotallyNonneg (stepKernel a t)

theorem BollobasNikiforov.diagonal_isTotallyNonneg {ι : Type u_3} [LinearOrder ι] [DecidableEq ι] (d : ι → ℝ) (hd : ∀ (i : ι), 0 ≤ d i) : IsTotallyNonneg (Matrix.diagonal d)

@[reducible, inline]

abbrev BollobasNikiforov.StrictMonoFin (k m : ℕ) : Type

Strictly increasing maps Fin k → Fin m.

Equations

• BollobasNikiforov.StrictMonoFin k m = { f : Fin k → Fin m // StrictMono f }

@[instance_reducible]

noncomputable instance BollobasNikiforov.decidablePredStrictMonoFin (k m : ℕ) : DecidablePred fun (f : Fin k → Fin m) => StrictMono f

Equations

• BollobasNikiforov.decidablePredStrictMonoFin k m = Classical.decPred fun (f : Fin k → Fin m) => StrictMono f

@[instance_reducible]

noncomputable instance BollobasNikiforov.instFintypeStrictMonoFin (k m : ℕ) : Fintype (StrictMonoFin k m)

Equations

• BollobasNikiforov.instFintypeStrictMonoFin k m = Subtype.fintype StrictMono

noncomputable def BollobasNikiforov.injRearrange {k m : ℕ} {u : Fin k → Fin m} (hu : Function.Injective u) : StrictMonoFin k m

The strictly increasing enumeration of the image of an injection u : Fin k → Fin m.

Equations

• BollobasNikiforov.injRearrange hu = ⟨⇑((Finset.image u Finset.univ).orderEmbOfFin ⋯), ⋯⟩

theorem BollobasNikiforov.injRearrange_mem {k m : ℕ} {u : Fin k → Fin m} (hu : Function.Injective u) (i : Fin k) : ∃ (j : Fin k), ↑(injRearrange hu) j = u i

noncomputable def BollobasNikiforov.injPerm {k m : ℕ} {u : Fin k → Fin m} (hu : Function.Injective u) : Equiv.Perm (Fin k)

The permutation of Fin k through which an injection u factors as injRearrange hu ∘ injPerm hu.

Equations

• BollobasNikiforov.injPerm hu = Equiv.ofBijective (fun (i : Fin k) => Classical.choose ⋯) ⋯

theorem BollobasNikiforov.inj_eq_rearrange_comp {k m : ℕ} {u : Fin k → Fin m} (hu : Function.Injective u) : u = ↑(injRearrange hu) ∘ ⇑(injPerm hu)

theorem BollobasNikiforov.image_comp_perm {k m : ℕ} (S : Fin k → Fin m) (π : Equiv.Perm (Fin k)) : Finset.image (S ∘ ⇑π) Finset.univ = Finset.image S Finset.univ

theorem BollobasNikiforov.injRearrange_comp {k m : ℕ} (S : StrictMonoFin k m) (π : Equiv.Perm (Fin k)) : injRearrange ⋯ = S

theorem BollobasNikiforov.injPerm_comp {k m : ℕ} (S : StrictMonoFin k m) (π : Equiv.Perm (Fin k)) : injPerm ⋯ = π

noncomputable def BollobasNikiforov.equivInjOfStrictMono (k m : ℕ) : StrictMonoFin k m × Equiv.Perm (Fin k) ≃ { u : Fin k → Fin m // Function.Injective u }

Injections Fin k → Fin m correspond to pairs of a strictly increasing map and a permutation of Fin k.

Equations

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

theorem BollobasNikiforov.det_mul_eq_sum_comp {k m : ℕ} (P : Matrix (Fin k) (Fin m) ℝ) (Q : Matrix (Fin m) (Fin k) ℝ) : (P * Q).det = ∑ p : Fin k → Fin m, (P.submatrix id p).det * ∏ i : Fin k, Q (p i) i

theorem BollobasNikiforov.det_mul_eq_sum_strictMono {k m : ℕ} (P : Matrix (Fin k) (Fin m) ℝ) (Q : Matrix (Fin m) (Fin k) ℝ) : (P * Q).det = ∑ S : StrictMonoFin k m, (P.submatrix id ↑S).det * (Q.submatrix (↑S) id).det

theorem BollobasNikiforov.IsTotallyNonneg.mul {l : Type u_3} {m : Type u_4} {n : Type u_5} [LinearOrder l] [LinearOrder m] [LinearOrder n] [Fintype m] {A : Matrix l m ℝ} {B : Matrix m n ℝ} (hA : IsTotallyNonneg A) (hB : IsTotallyNonneg B) : IsTotallyNonneg (A * B)

Uniform grid composition

noncomputable def BollobasNikiforov.valuesFinset {r c : ℕ} (a : Fin r → ℝ) (t : Fin c → ℝ) : Finset ℝ

The finite set of all values a i and t j.

Equations

• BollobasNikiforov.valuesFinset a t = Finset.image a Finset.univ ∪ Finset.image t Finset.univ

theorem BollobasNikiforov.valuesFinset_nonempty {r c : ℕ} (hr : 0 < r) (a : Fin r → ℝ) (t : Fin c → ℝ) : (valuesFinset a t).Nonempty

noncomputable def BollobasNikiforov.gridXMin {r c : ℕ} (hr : 0 < r) (a : Fin r → ℝ) (t : Fin c → ℝ) : ℝ

One less than the smallest of the values a i and t j.

Equations

• BollobasNikiforov.gridXMin hr a t = (BollobasNikiforov.valuesFinset a t).min' ⋯ - 1

noncomputable def BollobasNikiforov.gridXMax {r c : ℕ} (hr : 0 < r) (a : Fin r → ℝ) (t : Fin c → ℝ) : ℝ

One more than the largest of the values a i and t j.

Equations

• BollobasNikiforov.gridXMax hr a t = (BollobasNikiforov.valuesFinset a t).max' ⋯ + 1

theorem BollobasNikiforov.gridXMin_lt_a {r c : ℕ} (hr : 0 < r) (a : Fin r → ℝ) (t : Fin c → ℝ) (i : Fin r) : gridXMin hr a t < a i

theorem BollobasNikiforov.gridXMax_gt_t {r c : ℕ} (hr : 0 < r) (a : Fin r → ℝ) (t : Fin c → ℝ) (j : Fin c) : t j < gridXMax hr a t

theorem BollobasNikiforov.gridXMax_gt_a {r c : ℕ} (hr : 0 < r) (a : Fin r → ℝ) (t : Fin c → ℝ) (i : Fin r) : a i < gridXMax hr a t

theorem BollobasNikiforov.grid_span_pos {r c : ℕ} (hr : 0 < r) (a : Fin r → ℝ) (t : Fin c → ℝ) : 0 < gridXMax hr a t - gridXMin hr a t

noncomputable def BollobasNikiforov.gridDelta {r c : ℕ} (hr : 0 < r) (a : Fin r → ℝ) (t : Fin c → ℝ) (N : ℕ) : ℝ

The mesh of the uniform grid with N steps from gridXMin to gridXMax.

Equations

• BollobasNikiforov.gridDelta hr a t N = (BollobasNikiforov.gridXMax hr a t - BollobasNikiforov.gridXMin hr a t) / ↑N

theorem BollobasNikiforov.gridDelta_nonneg {r c : ℕ} (hr : 0 < r) (a : Fin r → ℝ) (t : Fin c → ℝ) (N : ℕ) : 0 ≤ gridDelta hr a t N

theorem BollobasNikiforov.gridDelta_pos {r c : ℕ} (hr : 0 < r) (a : Fin r → ℝ) (t : Fin c → ℝ) {N : ℕ} (hN : 0 < N) : 0 < gridDelta hr a t N

noncomputable def BollobasNikiforov.gridPt {r c : ℕ} (hr : 0 < r) (a : Fin r → ℝ) (t : Fin c → ℝ) (N : ℕ) (k : Fin (N + 1)) : ℝ

The k-th point of the uniform grid: gridXMin + k * gridDelta.

Equations

• BollobasNikiforov.gridPt hr a t N k = BollobasNikiforov.gridXMin hr a t + ↑↑k * BollobasNikiforov.gridDelta hr a t N

theorem BollobasNikiforov.gridPt_mono {r c : ℕ} (hr : 0 < r) (a : Fin r → ℝ) (t : Fin c → ℝ) (N : ℕ) : Monotone (gridPt hr a t N)

theorem BollobasNikiforov.gridPt_strictMono {r c : ℕ} (hr : 0 < r) (a : Fin r → ℝ) (t : Fin c → ℝ) {N : ℕ} (hN : 0 < N) : StrictMono (gridPt hr a t N)

theorem BollobasNikiforov.gridPt_zero {r c : ℕ} (hr : 0 < r) (a : Fin r → ℝ) (t : Fin c → ℝ) (N : ℕ) : gridPt hr a t N 0 = gridXMin hr a t

theorem BollobasNikiforov.gridPt_last {r c : ℕ} (hr : 0 < r) (a : Fin r → ℝ) (t : Fin c → ℝ) {N : ℕ} (hN : 0 < N) : gridPt hr a t N (Fin.last N) = gridXMax hr a t

noncomputable def BollobasNikiforov.gridH1 {r c : ℕ} (hr : 0 < r) (a : Fin r → ℝ) (t : Fin c → ℝ) (N : ℕ) : Matrix (Fin r) (Fin (N + 1)) ℝ

The step kernel from the row parameters a to the grid points.

Equations

• BollobasNikiforov.gridH1 hr a t N = BollobasNikiforov.stepKernel a (BollobasNikiforov.gridPt hr a t N)

noncomputable def BollobasNikiforov.gridH2 (N : ℕ) : Matrix (Fin (N + 1)) (Fin (N + 1)) ℝ

The step kernel between grid indices, compared through their values.

Equations

• BollobasNikiforov.gridH2 N = BollobasNikiforov.stepKernel (fun (k : Fin (N + 1)) => ↑↑k) fun (ℓ : Fin (N + 1)) => ↑↑ℓ

noncomputable def BollobasNikiforov.gridH3 {r c : ℕ} (hr : 0 < r) (a : Fin r → ℝ) (t : Fin c → ℝ) (N : ℕ) : Matrix (Fin (N + 1)) (Fin c) ℝ

The step kernel from the grid points to the column parameters t.

Equations

• BollobasNikiforov.gridH3 hr a t N = BollobasNikiforov.stepKernel (BollobasNikiforov.gridPt hr a t N) t

noncomputable def BollobasNikiforov.gridD {r c : ℕ} (hr : 0 < r) (a : Fin r → ℝ) (t : Fin c → ℝ) (N : ℕ) : Matrix (Fin (N + 1)) (Fin (N + 1)) ℝ

The scalar matrix gridDelta • 1 on grid indices.

Equations

• BollobasNikiforov.gridD hr a t N = Matrix.diagonal fun (x : Fin (N + 1)) => BollobasNikiforov.gridDelta hr a t N

noncomputable def BollobasNikiforov.gridK {r c : ℕ} (hr : 0 < r) (a : Fin r → ℝ) (t : Fin c → ℝ) (N : ℕ) : Matrix (Fin r) (Fin c) ℝ

The product H₁ D H₂ D H₃ of the grid kernels.

Equations

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

theorem BollobasNikiforov.gridH2_isTotallyNonneg (N : ℕ) : IsTotallyNonneg (gridH2 N)

theorem BollobasNikiforov.gridK_isTotallyNonneg {r c : ℕ} (hr : 0 < r) {a : Fin r → ℝ} {t : Fin c → ℝ} (ha : Monotone a) (ht : Monotone t) (N : ℕ) : IsTotallyNonneg (gridK hr a t N)

theorem BollobasNikiforov.gridH2_apply (N : ℕ) (k ℓ : Fin (N + 1)) : gridH2 N k ℓ = if k ≤ ℓ then 1 else 0

theorem BollobasNikiforov.gridK_apply {r c : ℕ} (hr : 0 < r) (a : Fin r → ℝ) (t : Fin c → ℝ) (N : ℕ) (i : Fin r) (j : Fin c) : gridK hr a t N i j = gridDelta hr a t N ^ 2 * ∑ ℓ : Fin (N + 1), ∑ k : Fin (N + 1), if a i ≤ gridPt hr a t N k ∧ k ≤ ℓ ∧ gridPt hr a t N ℓ ≤ t j then 1 else 0

theorem BollobasNikiforov.sum_ite_le_real (n : ℕ) : (∑ i : Fin n, ∑ j : Fin n, if i ≤ j then 1 else 0) = ↑n * (↑n + 1) / 2

theorem BollobasNikiforov.sum_ite_le_finset {n : ℕ} (s : Finset (Fin n)) : (∑ x ∈ s, ∑ y ∈ s, if x ≤ y then 1 else 0) = ↑s.card * (↑s.card + 1) / 2

noncomputable def BollobasNikiforov.gridSupport {r c : ℕ} (hr : 0 < r) (a : Fin r → ℝ) (t : Fin c → ℝ) (N : ℕ) (i : Fin r) (j : Fin c) : Finset (Fin (N + 1))

The grid indices k with a i ≤ gridPt k ≤ t j.

Equations

• BollobasNikiforov.gridSupport hr a t N i j = {k : Fin (N + 1) | a i ≤ BollobasNikiforov.gridPt hr a t N k ∧ BollobasNikiforov.gridPt hr a t N k ≤ t j}

theorem BollobasNikiforov.grid_pair_sum_eq {r c : ℕ} (hr : 0 < r) (a : Fin r → ℝ) (t : Fin c → ℝ) (N : ℕ) (i : Fin r) (j : Fin c) : (∑ ℓ : Fin (N + 1), ∑ k : Fin (N + 1), if a i ≤ gridPt hr a t N k ∧ k ≤ ℓ ∧ gridPt hr a t N ℓ ≤ t j then 1 else 0) = ∑ ℓ ∈ gridSupport hr a t N i j, ∑ k ∈ gridSupport hr a t N i j, if k ≤ ℓ then 1 else 0

theorem BollobasNikiforov.gridK_apply_count {r c : ℕ} (hr : 0 < r) (a : Fin r → ℝ) (t : Fin c → ℝ) (N : ℕ) (i : Fin r) (j : Fin c) : gridK hr a t N i j = gridDelta hr a t N ^ 2 * ↑(gridSupport hr a t N i j).card * (↑(gridSupport hr a t N i j).card + 1) / 2

theorem BollobasNikiforov.gridSupport_interval {r c : ℕ} (hr : 0 < r) (a : Fin r → ℝ) (t : Fin c → ℝ) {N : ℕ} (_hN : 0 < N) (i : Fin r) (j : Fin c) (hne : (gridSupport hr a t N i j).Nonempty) : gridSupport hr a t N i j = Finset.Icc ((gridSupport hr a t N i j).min' hne) ((gridSupport hr a t N i j).max' hne)

theorem BollobasNikiforov.gridPt_succ {r c : ℕ} (hr : 0 < r) (a : Fin r → ℝ) (t : Fin c → ℝ) (N : ℕ) (k : Fin (N + 1)) (hk : ↑k + 1 < N + 1) : gridPt hr a t N ⟨↑k + 1, hk⟩ = gridPt hr a t N k + gridDelta hr a t N

theorem BollobasNikiforov.gridPt_sub_eq {r c : ℕ} (hr : 0 < r) (a : Fin r → ℝ) (t : Fin c → ℝ) (N : ℕ) {k ℓ : Fin (N + 1)} (hkl : k ≤ ℓ) : gridPt hr a t N ℓ - gridPt hr a t N k = ↑(↑ℓ - ↑k) * gridDelta hr a t N

theorem BollobasNikiforov.not_mem_gridSupport_zero {r c : ℕ} (hr : 0 < r) (a : Fin r → ℝ) (t : Fin c → ℝ) (N : ℕ) (i : Fin r) (j : Fin c) : 0 ∉ gridSupport hr a t N i j

theorem BollobasNikiforov.not_mem_gridSupport_last {r c : ℕ} (hr : 0 < r) (a : Fin r → ℝ) (t : Fin c → ℝ) {N : ℕ} (hN : 0 < N) (i : Fin r) (j : Fin c) : Fin.last N ∉ gridSupport hr a t N i j

theorem BollobasNikiforov.mem_gridSupport_iff {r c : ℕ} (hr : 0 < r) (a : Fin r → ℝ) (t : Fin c → ℝ) (N : ℕ) (i : Fin r) (j : Fin c) (k : Fin (N + 1)) : k ∈ gridSupport hr a t N i j ↔ a i ≤ gridPt hr a t N k ∧ gridPt hr a t N k ≤ t j

theorem BollobasNikiforov.gridSupport_card_mul_delta_sub_le {r c : ℕ} (hr : 0 < r) (a : Fin r → ℝ) (t : Fin c → ℝ) {N : ℕ} (hN : 0 < N) (i : Fin r) (j : Fin c) : |↑(gridSupport hr a t N i j).card * gridDelta hr a t N - max (t j - a i) 0| ≤ 2 * gridDelta hr a t N

theorem BollobasNikiforov.gridDelta_tendsto {r c : ℕ} (hr : 0 < r) (a : Fin r → ℝ) (t : Fin c → ℝ) : Filter.Tendsto (fun (n : ℕ) => gridDelta hr a t (n + 1)) Filter.atTop (nhds 0)

theorem BollobasNikiforov.gridSupport_mul_delta_tendsto {r c : ℕ} (hr : 0 < r) (a : Fin r → ℝ) (t : Fin c → ℝ) (i : Fin r) (j : Fin c) : Filter.Tendsto (fun (n : ℕ) => ↑(gridSupport hr a t (n + 1) i j).card * gridDelta hr a t (n + 1)) Filter.atTop (nhds (max (t j - a i) 0))

theorem BollobasNikiforov.gridK_tendsto {r c : ℕ} (hr : 0 < r) (a : Fin r → ℝ) (t : Fin c → ℝ) (i : Fin r) (j : Fin c) : Filter.Tendsto (fun (n : ℕ) => gridK hr a t (n + 1) i j) Filter.atTop (nhds (2⁻¹ * truncatedSquare a t i j))

theorem BollobasNikiforov.isTotallyNonneg_truncatedSquare {r c : ℕ} {a : Fin r → ℝ} {t : Fin c → ℝ} (ha : Monotone a) (ht : Monotone t) : IsTotallyNonneg (truncatedSquare a t)