Documentation

Complexitylib.RationalHitting.Internal.Evaluation

Rational hitting lists: evaluation #

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/RationalHitting/Evaluation.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical arguments are retained.

source
theorem Complexity.RationalHitting.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
source
theorem Complexity.RationalHitting.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)
source
theorem Complexity.RationalHitting.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 Complexity.RationalHitting.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 Complexity.RationalHitting.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.

Equations
Instances For
    source
    theorem Complexity.RationalHitting.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)
    source
    theorem Complexity.RationalHitting.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)
    source
    theorem Complexity.RationalHitting.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
    source
    theorem Complexity.RationalHitting.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
    source
    theorem Complexity.RationalHitting.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)
    source
    theorem Complexity.RationalHitting.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