Soundness of the packed Bernstein test

bernGE P m checks that every quadratic Bernstein coefficient of the packed polynomial P (layout L3) is at least m. On [-1,1]⁵ such a polynomial is a convex combination of its Bernstein coefficients, so it is at least m there.

Digits of layout L3

def Cayley.Pack.dg (i j : ℕ) : ℕ

Digit i of slot j.

Equations

• Cayley.Pack.dg i j = j / 3 ^ i % 3

theorem Cayley.Pack.dg_lt (i j : ℕ) : dg i j < 3

theorem Cayley.Pack.dg_shiftA (i : ℕ) : i < 5 → ∀ e < 3, ∀ j < 243, dg i j ≠ 0 ∨ j + e * 3 ^ i < 243

Shifting a slot whose digit i is 0 by e·3ⁱ makes that digit e and keeps the others.

theorem Cayley.Pack.dg_shiftB (i : ℕ) : i < 5 → ∀ e < 3, ∀ j < 243, dg i j ≠ 0 ∨ dg i (j + e * 3 ^ i) = e

theorem Cayley.Pack.dg_shiftC (i : ℕ) : i < 5 → ∀ e < 3, ∀ j < 243, ∀ a < 5, dg i j ≠ 0 ∨ a = i ∨ dg a (j + e * 3 ^ i) = dg a j

theorem Cayley.Pack.dg_shift (i : ℕ) : i < 5 → ∀ e < 3, ∀ j < 243, dg i j = 0 → j + e * 3 ^ i < 243 ∧ dg i (j + e * 3 ^ i) = e ∧ ∀ a < 5, a ≠ i → dg a (j + e * 3 ^ i) = dg a j

theorem Cayley.Pack.dg_unshift0 (i : ℕ) : i < 5 → ∀ e < 3, ∀ j < 243, dg i j ≠ e ∨ e * 3 ^ i ≤ j ∧ dg i (j - e * 3 ^ i) = 0

theorem Cayley.Pack.dg_unshift (i : ℕ) : i < 5 → ∀ e < 3, ∀ j < 243, dg i j = e → e * 3 ^ i ≤ j ∧ dg i (j - e * 3 ^ i) = 0

theorem Cayley.Pack.sum_fiber {M : Type u_1} [AddCommMonoid M] {i e : ℕ} (hi : i < 5) (he : e < 3) (g : ℕ → M) : (∑ j ∈ Finset.range 243, if dg i j = e then g j else 0) = ∑ j ∈ Finset.range 243, if dg i j = 0 then g (j + e * 3 ^ i) else 0

The slots with digit i equal to e are those with digit 0, shifted.

theorem Cayley.Pack.sum_split {M : Type u_1} [AddCommMonoid M] {i : ℕ} (hi : i < 5) (g : ℕ → M) : ∑ j ∈ Finset.range 243, g j = ∑ j ∈ Finset.range 243, if dg i j = 0 then g j + g (j + 3 ^ i) + g (j + 2 * 3 ^ i) else 0

A sum over the slots, grouped along digit i.

The coefficient transform

def Cayley.Pack.bM : ℕ → ℕ → ℤ

The Bernstein matrix on [-1,1]: row κ (Bernstein index), column e (power).

Equations

• Cayley.Pack.bM 0 1 = -1
• Cayley.Pack.bM 1 1 = 0
• Cayley.Pack.bM 1 2 = -1
• Cayley.Pack.bM x✝¹ x✝ = 1

theorem Cayley.Pack.abs_bM (a b : ℕ) : |bM a b| ≤ 1

def Cayley.Pack.axT (i : ℕ) (c : ℕ → ℤ) (j : ℕ) : ℤ

The Bernstein transform along digit i of slot coefficients c.

Equations

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

theorem Cayley.Pack.axT_shift {i e j : ℕ} (hi : i < 5) (he : e < 3) (hj : j < 243) (h0 : dg i j = 0) (c : ℕ → ℤ) : axT i c (j + e * 3 ^ i) = bM e 0 * c j + bM e 1 * c (j + 3 ^ i) + bM e 2 * c (j + 2 * 3 ^ i)

def Cayley.Pack.bT (c : ℕ → ℤ) : ℕ → ℤ

All five axes.

Equations

• Cayley.Pack.bT c = Cayley.Pack.axT 4 (Cayley.Pack.axT 3 (Cayley.Pack.axT 2 (Cayley.Pack.axT 1 (Cayley.Pack.axT 0 c))))

theorem Cayley.Pack.axT_bound {i : ℕ} (hi : i < 5) {c : ℕ → ℤ} {B : ℤ} (hc : ∀ j < 243, |c j| ≤ B) (j : ℕ) : j < 243 → |axT i c j| ≤ 3 * B

The packed value

theorem Cayley.Pack.int_add (a b : ℤ) : a.add b = a + b

theorem Cayley.Pack.int_sub (a b : ℤ) : a.sub b = a - b

theorem Cayley.Pack.int_mul (a b : ℤ) : a.mul b = a * b

def Cayley.Pack.pv (c : ℕ → ℤ) : ℤ

The packed integer with slot coefficients c.

Equations

• Cayley.Pack.pv c = ∑ j ∈ Finset.range 243, c j * 2 ^ (Cayley.K.PW * j)

theorem Cayley.Pack.onesL3_n : K.onesL3 = packN K.PW (fun (x : ℕ) => 1) 243

@[reducible, inline]

abbrev Cayley.Pack.enc (c : ℕ → ℤ) : ℕ

The offset encoding of slot coefficients c.

Equations

• Cayley.Pack.enc c = Cayley.Pack.packN Cayley.K.PW (Cayley.Pack.odig c) 243

theorem Cayley.Pack.enc_cast {c : ℕ → ℤ} (hc : ∀ j < 243, |c j| < ↑O) : ↑(enc c) = pv c + ↑((2 ^ (K.PW - 1)).mul K.onesL3)

theorem Cayley.Pack.enc_pv {c : ℕ → ℤ} (hc : ∀ j < 243, |c j| < ↑O) : (pv c + ↑((2 ^ (K.PW - 1)).mul K.onesL3)).toNat = packN K.PW (odig c) 243

Decoding one axis

theorem Cayley.Pack.zL3_eq (i : ℕ) : i < 5 → K.zL3 i = packN K.PW (fun (j : ℕ) => if dg i j = 0 then 1 else 0) 243

theorem Cayley.Pack.land_ite {W n : ℕ} {d : ℕ → ℕ} (hd : ∀ j < n, d j < 2 ^ W) (q : ℕ → Prop) [DecidablePred q] : packN W d n &&& packN W (fun (j : ℕ) => if q j then 2 ^ W - 1 else 0) n = packN W (fun (j : ℕ) => if q j then d j else 0) n

theorem Cayley.Pack.nat_shiftLeft (a b : ℕ) : a.shiftLeft b = a <<< b

theorem Cayley.Pack.packN_shift {i e : ℕ} (hi : i < 5) (he : e < 3) (x : ℕ → ℕ) : packN K.PW (fun (j : ℕ) => if dg i j = e then x j else 0) 243 = 2 ^ (K.PW * (e * 3 ^ i)) * packN K.PW (fun (j : ℕ) => if dg i j = 0 then x (j + e * 3 ^ i) else 0) 243

Shifting the digit-0 slots by e·3ⁱ.

theorem Cayley.Pack.odig_shift {i e : ℕ} (hi : i < 5) (he : e < 3) {c : ℕ → ℤ} (hc : ∀ j < 243, |c j| < ↑O) : ↑(packN K.PW (fun (j : ℕ) => if dg i j = 0 then odig c (j + e * 3 ^ i) else 0) 243) - ↑((2 ^ (K.PW - 1)).mul (K.zL3 i)) = ∑ j ∈ Finset.range 243, (if dg i j = 0 then c (j + e * 3 ^ i) else 0) * 2 ^ (K.PW * j)

theorem Cayley.Pack.shiftRight_part {i e : ℕ} (hi : i < 5) (he : e < 3) {c : ℕ → ℤ} (hc : ∀ j < 243, |c j| < ↑O) (s : ℕ) (hs : s = K.PW * (e * 3 ^ i)) : ((packN K.PW (odig c) 243).land ((K.pM.mul (K.zL3 i)).shiftLeft s)).shiftRight s = packN K.PW (fun (j : ℕ) => if dg i j = 0 then odig c (j + e * 3 ^ i) else 0) 243

theorem Cayley.Pack.pv_axT {i : ℕ} (hi : i < 5) (c : ℕ → ℤ) : pv (axT i c) = ∑ j ∈ Finset.range 243, (if dg i j = 0 then c (j + 0 * 3 ^ i) else 0) * 2 ^ (K.PW * j) - ∑ j ∈ Finset.range 243, (if dg i j = 0 then c (j + 1 * 3 ^ i) else 0) * 2 ^ (K.PW * j) + ∑ j ∈ Finset.range 243, (if dg i j = 0 then c (j + 2 * 3 ^ i) else 0) * 2 ^ (K.PW * j) + 2 ^ (K.PW * 3 ^ i) * (∑ j ∈ Finset.range 243, (if dg i j = 0 then c (j + 0 * 3 ^ i) else 0) * 2 ^ (K.PW * j) - ∑ j ∈ Finset.range 243, (if dg i j = 0 then c (j + 2 * 3 ^ i) else 0) * 2 ^ (K.PW * j)) + 2 ^ (K.PW * 3 ^ i) * 2 ^ (K.PW * 3 ^ i) * (∑ j ∈ Finset.range 243, (if dg i j = 0 then c (j + 0 * 3 ^ i) else 0) * 2 ^ (K.PW * j) + ∑ j ∈ Finset.range 243, (if dg i j = 0 then c (j + 1 * 3 ^ i) else 0) * 2 ^ (K.PW * j) + ∑ j ∈ Finset.range 243, (if dg i j = 0 then c (j + 2 * 3 ^ i) else 0) * 2 ^ (K.PW * j))

The digit-i grouping of pv (axT i c): the three Bernstein combinations of the digit-0, 1, 2 parts, shifted into place.

theorem Cayley.Pack.off_sum {i : ℕ} (hi : i < 5) : ↑((2 ^ (K.PW - 1)).mul (K.zL3 i)) = ∑ j ∈ Finset.range 243, (if dg i j = 0 then ↑O else 0) * 2 ^ (K.PW * j)

The offsets of one digit group, as a signed sum.

theorem Cayley.Pack.zL3_geo (i : ℕ) : i < 5 → K.zL3 i * (1 + 2 ^ (K.PW * 3 ^ i) + 2 ^ (K.PW * 3 ^ i) * 2 ^ (K.PW * 3 ^ i)) = K.onesL3

theorem Cayley.Pack.sum_off_nonneg {i : ℕ} (f : ℕ → ℤ) (hf : ∀ j < 243, dg i j = 0 → -↑O < f j) : 0 ≤ ∑ j ∈ Finset.range 243, (if dg i j = 0 then f j else 0) * 2 ^ (K.PW * j) + ∑ j ∈ Finset.range 243, (if dg i j = 0 then ↑O else 0) * 2 ^ (K.PW * j)

A digit-0 signed sum plus the offsets is nonnegative when every coefficient is above -O.

theorem Cayley.Pack.baxis_enc {i : ℕ} (hi : i < 5) {c : ℕ → ℤ} (hc : ∀ j < 243, |c j| < ↑O) (hT : ∀ j < 243, |axT i c j| < ↑O) : K.baxis i (enc c) = enc (axT i c)

One axis. baxis applies the Bernstein transform along digit i to the encoding.

All axes and the sign test

theorem Cayley.Pack.bern3_pv {c : ℕ → ℤ} {B : ℤ} (hc : ∀ j < 243, |c j| ≤ B) (hB : 243 * B < ↑O) : K.bern3 (enc c) = enc (bT c)

theorem Cayley.Pack.bT_bound {c : ℕ → ℤ} {B : ℤ} (hc : ∀ j < 243, |c j| ≤ B) (j : ℕ) : j < 243 → |bT c j| ≤ 243 * B

theorem Cayley.Pack.packN_inj {W n : ℕ} {d e : ℕ → ℕ} (hd : ∀ j < n, d j < 2 ^ W) (he : ∀ j < n, e j < 2 ^ W) (h : packN W d n = packN W e n) (j : ℕ) : j < n → d j = e j

theorem Cayley.Pack.ones_sum : ↑K.onesL3 = ∑ j ∈ Finset.range 243, 2 ^ (K.PW * j)

theorem Cayley.Pack.bernGE_spec {c : ℕ → ℤ} {B m : ℤ} (hc : ∀ j < 243, |c j| ≤ B) (hB : 243 * B + 2 ^ 390 ≤ ↑O) (h : K.bernGE (pv c) m = true) (j : ℕ) : j < 243 → m ≤ bT c j

The sign test. A passing bernGE bounds every Bernstein coefficient from below.

The polynomial is a convex combination of its Bernstein coefficients

noncomputable def Cayley.Pack.bβ (κ : ℕ) (x : ℝ) : ℝ

The quadratic Bernstein basis on [-1,1].

Equations

• Cayley.Pack.bβ κ x = if κ = 0 then ((1 - x) / 2) ^ 2 else if κ = 1 then (1 - x ^ 2) / 2 else ((1 + x) / 2) ^ 2

theorem Cayley.Pack.bβ_nonneg (κ : ℕ) {x : ℝ} (hx : |x| ≤ 1) : 0 ≤ bβ κ x

theorem Cayley.Pack.bβ_sum (x : ℝ) {e : ℕ} (he : e < 3) : ↑(bM 0 e) * bβ 0 x + ↑(bM 1 e) * bβ 1 x + ↑(bM 2 e) * bβ 2 x = x ^ e

theorem Cayley.Pack.axis_real {i : ℕ} (hi : i < 5) (c : ℕ → ℤ) (φ : ℕ → ℕ → ℝ) (g : ℕ → ℝ) (hg : ∀ e < 3, ↑(bM 0 e) * g 0 + ↑(bM 1 e) * g 1 + ↑(bM 2 e) * g 2 = φ i e) : ∑ j ∈ Finset.range 243, ↑(axT i c j) * ∏ a ∈ Finset.range 5, Function.update φ i g a (dg a j) = ∑ j ∈ Finset.range 243, ↑(c j) * ∏ a ∈ Finset.range 5, φ a (dg a j)

noncomputable def Cayley.Pack.φk (t : ℕ → ℝ) (k a d : ℕ) : ℝ

The weights after converting the first k axes.

Equations

• Cayley.Pack.φk t k a d = if a < k then Cayley.Pack.bβ d (t a) else t a ^ d

theorem Cayley.Pack.φk_succ (t : ℕ → ℝ) (k : ℕ) : (Function.update (φk t k) k fun (d : ℕ) => bβ d (t k)) = φk t (k + 1)

theorem Cayley.Pack.bern_real (c : ℕ → ℤ) (t : ℕ → ℝ) : ∑ j ∈ Finset.range 243, ↑(bT c j) * ∏ a ∈ Finset.range 5, bβ (dg a j) (t a) = ∑ j ∈ Finset.range 243, ↑(c j) * ∏ a ∈ Finset.range 5, t a ^ dg a j

theorem Cayley.Pack.bT_delta (j : ℕ) : j < 243 → bT (fun (j : ℕ) => if j = 0 then 1 else 0) j = 1

theorem Cayley.Pack.bernGE_le {e : PE} (h : L3.Fits e) {m : ℤ} (hb : 243 * ↑e.nrm + 2 ^ 390 ≤ ↑O) (hok : K.bernGE (PE.ev (fun (i : Fin 5) => K.pX ↑i) e) m = true) {t : Fin 5 → ℝ} (ht : ∀ (i : Fin 5), |t i| ≤ 1) : ↑m ≤ PE.ev t e

Bernstein bound. A passing bernGE bounds the polynomial on [-1,1]⁵.