Alignment.lean`

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.UniqueGamesTheorem.Quadratic.alignmentMatrix line 24
Source documentation
The |n| * |ι| alignment columns for a fixed parametrization and input set. The input set is represented by any map point : E → V; no injectivity is needed for the exact algebraic equivalence.
```
def alignmentMatrix (b : Basis ι R V) (point : E → V) (z : V → n → F) :
    Matrix E (n × ι) F :=
…
```
theorem OAI.UniqueGamesTheorem.Quadratic.dot_lift_eq_alignment_mulVec line 31
Source documentation
Basis values of a linear lift give the coefficients of the alignment column combination. The identity holds for every lift, without selecting one in advance of the parametrization.
```
theorem dot_lift_eq_alignment_mulVec (b : Basis ι R V)
    (point : E → V) (z : V → n → F) (g : V →ₗ[R] (n → F)) (e : E) :
    (∑ i, z (point e) i * g (point e) i) =
      (alignmentMatrix b point z *ᵥ (fun ij => g (b ij.2) ij.1)) e := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.alignmentMatrix
theorem OAI.UniqueGamesTheorem.Quadratic.exists_lift_alignment_iff_mem_range line 54
Source documentation
Existence of any linear lift aligning on the chosen inputs is one column-membership event. In particular there is no field-size-dependent union bound over the possible lifts.
```
theorem exists_lift_alignment_iff_mem_range (b : Basis ι R V)
    (point : E → V) (z : V → n → F) (c : E → F) :
    (∃ g : V →ₗ[R] (n → F), ∀ e,
      (∑ i, z (point e) i * g (point e) i) = c e) ↔
      c ∈ LinearMap.range (alignmentMatrix b point z).mulVecLin := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.alignmentMatrix
theorem OAI.UniqueGamesTheorem.Quadratic.finrank_alignment_range_le line 79
Source documentation
The column-space dimension is at most the number of free basis values. For three field coordinates and a binary basis of size r, this is 3r.
```
theorem finrank_alignment_range_le (b : Basis ι R V)
    (point : E → V) (z : V → n → F) [Fintype E] :
    Module.finrank F (LinearMap.range (alignmentMatrix b point z).mulVecLin) ≤
      Fintype.card n * Fintype.card ι := by
…
```
Mentions: OAI.UniqueGamesTheorem.Quadratic.alignmentMatrix