Lagrange indicators for signs

SignType.lagrangeCoeff gives the coefficients of the three indicator polynomials 1 - x², (x² - x) / 2, and (x² + x) / 2 on {-1,0,1}. SignType.sum_lagrangeCoeff_mul_pow evaluates these indicators on signs, supplying the one-coordinate inverse in finite sign determination.

References

S. Basu, R. Pollack, and M.-F. Roy, Algorithms in Real Algebraic Geometry, second edition, Chapter 10, for the ternary sign-moment inverse.

def SignType.lagrangeCoeff (s : SignType) (e : Fin 3) : ℚ

Coefficients of the three Lagrange indicator polynomials on {-1,0,1}.

Equations

• SignType.zero.lagrangeCoeff e = if e = 0 then 1 else if e = 2 then -1 else 0
• SignType.neg.lagrangeCoeff e = if e = 1 then -1 / 2 else if e = 2 then 1 / 2 else 0
• SignType.pos.lagrangeCoeff e = if e = 1 then 1 / 2 else if e = 2 then 1 / 2 else 0

theorem SignType.lagrangeCoeff_zero (e : Fin 3) : lagrangeCoeff 0 e = if e = 0 then 1 else if e = 2 then -1 else 0

theorem SignType.lagrangeCoeff_neg_one (e : Fin 3) : (-1).lagrangeCoeff e = if e = 1 then -1 / 2 else if e = 2 then 1 / 2 else 0

theorem SignType.lagrangeCoeff_one (e : Fin 3) : lagrangeCoeff 1 e = if e = 1 then 1 / 2 else if e = 2 then 1 / 2 else 0

@[simp]

theorem SignType.sum_lagrangeCoeff_mul_pow (s t : SignType) : ∑ e : Fin 3, s.lagrangeCoeff e * ↑t ^ ↑e = if s = t then 1 else 0

Each Lagrange indicator evaluates to one at its own sign and zero at the other signs.