Integer affine relations #
Clearing denominators in a rational generalized inverse produces a finite family of integer relations. Their evaluations measure the discrepancy from a function that factors through the original constraint matrix.
theorem
EGZ.Expansion.relation_column_pos_neg_sum
{r : ℕ}
{S : Finset (IntCoord r)}
{Q : Matrix ↥S ↥S ℤ}
(hQ : affineConstraintMatrix S * Q = 0)
(q : ↥S)
:
A signed affine relation is represented by its positive and negative parts, which have the same nonnegative total size.
theorem
EGZ.Expansion.relation_evaluation
{I : Type u_1}
{J : Type u_2}
[Fintype I]
[Fintype J]
{R : Type u_3}
[CommRing R]
[DecidableEq J]
{A : Matrix I J ℤ}
{N : ℕ}
{B : Matrix J I ℤ}
{Q : Matrix J J ℤ}
(hQ : Q = ↑N • 1 - B * A)
(v : J → R)
:
(Q.map ⇑(Int.castRingHom R)).transpose.mulVec v = ↑N • v - (A.map ⇑(Int.castRingHom R)).transpose.mulVec ((B.map ⇑(Int.castRingHom R)).transpose.mulVec v)
def
EGZ.Expansion.affineFromCoefficients
{R : Type u_3}
[CommRing R]
{r : ℕ}
(a : Option (Fin r) → R)
:
The affine function encoded by its constant and linear coefficients.
Equations
- EGZ.Expansion.affineFromCoefficients a = AffineMap.const R (Fin r → R) (a none) + ∑ i : Fin r, a (some i) • AffineMap.proj i
Instances For
theorem
EGZ.Expansion.affine_relation_residual_bounded
{p r t N W L : ℕ}
{S : Finset (IntCoord r)}
{B : Matrix (↥S) (Option (Fin r)) ℤ}
{Q : Matrix ↥S ↥S ℤ}
(hQ : Q = ↑N • 1 - B * affineConstraintMatrix S)
(v : ↥S → ZMod p)
(ξ : FpCoord p t →ₗ[ZMod p] ZMod p)
(q : ↥S)
(x : FpCoord p (r + t))
(hx : (Coord.first r t) x = IntCoord.mod p ↑q)
(hlocal : HasBoundedRepresentative p W (ξ ((Coord.last r t) x) - v q))
(hrelation : HasBoundedRepresentative p L (∑ z : ↥S, ↑(Q z q) * v z))
:
HasBoundedRepresentative p (N * W + L)
((↑N • (ξ ∘ₗ Coord.last r t).toAffineMap - (affineFromCoefficients ((B.map ⇑(Int.castRingHom (ZMod p))).transpose.mulVec v)).comp
(Coord.first r t).toAffineMap)
x)
theorem
EGZ.Expansion.nonconstant_scaled_fibre_residual
{p r t N : ℕ}
[Fact (Nat.Prime p)]
(hN : 0 < N)
(hNp : N < p)
(ξ : FpCoord p t →ₗ[ZMod p] ZMod p)
(hξ : ξ ≠ 0)
(a : FpCoord p r →ᵃ[ZMod p] ZMod p)
:
NonconstantOnFibers (⇑(Coord.first r t)) (↑N • (ξ ∘ₗ Coord.last r t).toAffineMap - a.comp (Coord.first r t).toAffineMap)
Scaling a nonzero functional in the fibre directions and subtracting an arbitrary affine function of the labels still distinguishes a fibre.