Documentation

Complexity.Computability.Circuit.Rational.Eval

Rational hitting lists: evaluation #

Basic properties of the partial evaluation of rational formulas: values are unique, they are transported along ring homomorphisms, and they lift back along homomorphisms reflecting units. The second part collects facts on two-by-two block matrices over a possibly noncommutative ring, notably the Schur-complement criterion for invertibility of a block matrix with a zero corner.

Main definitions #

Main results #

References #

source
theorem Cslib.Circuits.Rational.Formula.Eval.unique {n : ℕ} {R : Type u_1} [Ring R] {c : ℚ →+* R} {X : Fin n → R} {h : Formula n} {a b : R} (ha : Eval c X h a) (hb : Eval c X h b) :
a = b

A formula has at most one value at a substitution.

source
theorem Cslib.Circuits.Rational.Formula.Eval.map {n : ℕ} {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {c : ℚ →+* R} {X : Fin n → R} {h : Formula n} {a : R} (ha : Eval c X h a) (f : R →+* S) :
Eval (f.comp c) (fun (i : Fin n) => f (X i)) h (f a)

A ring homomorphism maps a value of a formula to a value at the mapped substitution.

source
theorem Cslib.Circuits.Rational.Formula.Eval.lift {n : ℕ} {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R →+* S) (hf : ∀ (x : R), IsUnit (f x) → IsUnit x) {c : ℚ →+* R} {X : Fin n → R} {h : Formula n} {a : S} (ha : Eval (f.comp c) (fun (i : Fin n) => f (X i)) h a) :
∃ (b : R), Eval c X h b ∧ f b = a

Defined evaluations lift through a homomorphism reflecting units. In particular this handles every inverse occurrence before considering the root.

source
theorem Cslib.Circuits.Rational.Formula.Eval.unit_of_division_lift {n : ℕ} {R : Type u_1} [Ring R] {D : Type u_3} [DivisionRing D] [Nontrivial R] (f : D →+* R) {c : ℚ →+* D} {X : Fin n → D} {h : Formula n} {a : R} (ha : Eval (f.comp c) (fun (i : Fin n) => f (X i)) h a) (ha0 : a ≠ 0) :
IsUnit a

Mapping a defined nonzero value out of a division ring makes it a unit. This is used after the partial-specialization domain proof, not instead of it.

source
@[reducible, inline]
abbrev Cslib.Circuits.Rational.NoncommBlocks.matMul {R : Type u_1} [Ring R] {l : Type u_4} {m : Type u_5} {n : Type u_6} [Fintype m] (A : Matrix l m R) (B : Matrix m n R) :
Matrix l n R

Matrix multiplication over the possibly noncommutative coefficient ring.

Instances For
    source
    theorem Cslib.Circuits.Rational.NoncommBlocks.upper_unit {R : Type u_1} [Ring R] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (B : Matrix ι κ R) :
    IsUnit (Matrix.fromBlocks 1 B 0 1)

    An upper unitriangular block matrix is invertible.

    source
    theorem Cslib.Circuits.Rational.NoncommBlocks.lower_unit {R : Type u_1} [Ring R] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (C : Matrix κ ι R) :
    IsUnit (Matrix.fromBlocks 1 0 C 1)

    A lower unitriangular block matrix is invertible.

    source
    theorem Cslib.Circuits.Rational.NoncommBlocks.diag_unit_iff {R : Type u_1} [Ring R] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (A : Matrix ι ι R) (D : Matrix κ κ R) :
    IsUnit (Matrix.fromBlocks A 0 0 D) ↔ IsUnit A ∧ IsUnit D

    A block diagonal matrix is invertible exactly when both diagonal blocks are.

    source
    theorem Cslib.Circuits.Rational.NoncommBlocks.schur_factor {R : Type u_1} [Ring R] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (A A' : Matrix ι ι R) (B : Matrix ι κ R) (C : Matrix κ ι R) (hAA' : A * A' = 1) (hA'A : A' * A = 1) :
    Matrix.fromBlocks A B C 0 = Matrix.fromBlocks 1 0 (C * A') 1 * Matrix.fromBlocks A 0 0 (-C * A' * B) * Matrix.fromBlocks 1 (A' * B) 0 1

    The Schur factorization of a block matrix with a zero corner and an invertible corner.

    source
    theorem Cslib.Circuits.Rational.NoncommBlocks.schur_unit_iff {R : Type u_1} [Ring R] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (A A' : Matrix ι ι R) (B : Matrix ι κ R) (C : Matrix κ ι R) (hAA' : A * A' = 1) (hA'A : A' * A = 1) :
    IsUnit (Matrix.fromBlocks A B C 0) ↔ IsUnit (C * A' * B)

    A block matrix with a zero corner and an invertible corner is invertible exactly when its Schur complement is.

    source
    theorem Cslib.Circuits.Rational.NoncommBlocks.schur_inverse {R : Type u_1} [Ring R] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (A A' : Matrix ι ι R) (B : Matrix ι κ R) (C : Matrix κ ι R) (a b : Matrix κ κ R) (hAA' : A * A' = 1) (hA'A : A' * A = 1) (ha : C * A' * B = a) (hab : a * b = 1) (hba : b * a = 1) :
    ∃ (M : Matrix (ι ⊕ κ) (ι ⊕ κ) R), Matrix.fromBlocks A B C 0 * M = 1 ∧ M * Matrix.fromBlocks A B C 0 = 1 ∧ matMul (matMul (Matrix.fromCols 0 (-1)) M) (Matrix.fromRows 0 1) = b

    An inverse of a block matrix with a zero corner and an invertible corner, whose corner block is the inverse of the Schur complement.