The rows of a product sweep

The semantic half of the closure under products (DescriptiveComplexity.Counting.Digits.ProdSweep). A product I · Πū. f(ū) of numbers given by their digits is an iterated multiplication, and a multiplication is an iterated addition; both iterations are one sweep, along the pairs (ū, j̄) of a tuple and a position, the tuples increasing and, for each tuple, the positions decreasing (DescriptiveComplexity.Digits.prodIx).

The row of (ū, j̄) holds (DescriptiveComplexity.Digits.pval) P · ⌊f(ū) / 2 ^ r⌋, where P is the product before ū and r the rank of j̄: Horner's scheme for P · f(ū), read from the most significant digit of f(ū) down. It is the double of the previous row, plus P when the digit of rank r of f(ū) is 1 (DescriptiveComplexity.Digits.prodPhi_eq); and P is itself a row, the last one of the previous tuple.

def DescriptiveComplexity.Digits.ut {A : Type} {m ℓ : ℕ} (i : Fin (m + ℓ) → A) : Fin m → A

The tuple of an index of a product sweep.

Equations

• DescriptiveComplexity.Digits.ut i k = i (Fin.castAdd ℓ k)

def DescriptiveComplexity.Digits.jt {A : Type} {m ℓ : ℕ} (i : Fin (m + ℓ) → A) : Fin ℓ → A

The position of an index of a product sweep.

Equations

• DescriptiveComplexity.Digits.jt i k = i (Fin.natAdd m k)

theorem DescriptiveComplexity.Digits.ut_append {A : Type} {m ℓ : ℕ} (u : Fin m → A) (j : Fin ℓ → A) : ut (Fin.append u j) = u

theorem DescriptiveComplexity.Digits.jt_append {A : Type} {m ℓ : ℕ} (u : Fin m → A) (j : Fin ℓ → A) : jt (Fin.append u j) = j

theorem DescriptiveComplexity.Digits.append_ut_jt {A : Type} {m ℓ : ℕ} (i : Fin (m + ℓ) → A) : Fin.append (ut i) (jt i) = i

def DescriptiveComplexity.Digits.prodIx {A : Type} {m ℓ : ℕ} : (Fin (m + ℓ) → A) ≃ Lex (Lex (Fin m → A) × (Lex (Fin ℓ → A))ᵒᵈ)

The indices of a product sweep, in the order of the sweep: the tuples increasing, and for each tuple the positions decreasing.

Equations

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

noncomputable def DescriptiveComplexity.Digits.pval {A : Type} {m ℓ : ℕ} [LinearOrder A] (Iw : ℕ) (f : Lex (Fin m → A) → ℕ) (i : Fin (m + ℓ) → A) : ℕ

The value of a row: the product before the tuple, times the digits of the factor of the tuple from the position up.

Equations

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

def DescriptiveComplexity.Digits.prodPhi {A : Type} {m ℓ : ℕ} [LinearOrder A] (Iw : ℕ) (f : Lex (Fin m → A) → ℕ) (i : Fin (m + ℓ) → A) (R : (Fin (m + ℓ) → A) → (Fin ℓ → A) → Prop) (p : Fin ℓ → A) : Prop

The condition defining a row from the rows before it: the double of the previous row of the same tuple, plus – when the digit of the factor at the position is 1 – the product before the tuple, which is the initial number at the first tuple and the last row of the previous tuple otherwise.

Equations

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

theorem DescriptiveComplexity.Digits.prodPhi_eq {A : Type} {m ℓ : ℕ} [LinearOrder A] [Finite A] [Nonempty A] (Iw : ℕ) (f : Lex (Fin m → A) → ℕ) (i : Fin (m + ℓ) → A) (R : (Fin (m + ℓ) → A) → (Fin ℓ → A) → Prop) (hR : ∀ (i₀ : Fin (m + ℓ) → A), prodIx i₀ < prodIx i → R i₀ = tupBits (pval Iw f i₀)) : prodPhi Iw f i R = tupBits (pval Iw f i)

A row is determined by the rows before it.