noncomputable def
HexRealRootsTheory.Tarski.chainPolys
{D : Type u}
{K : Type v}
[Zero D]
[DecidableEq D]
[Field K]
[DecidableEq K]
(f : D → K)
(hz : ∀ (a : D), f a = 0 ↔ a = 0)
(c : Hex.SignedRemainderChain D)
:
List (Polynomial K)
The polynomial list interpreted from the literal replay array.
Equations
Instances For
theorem
HexRealRootsTheory.Tarski.chainPolys_getD
{D : Type u}
{K : Type v}
[Zero D]
[DecidableEq D]
[Field K]
[DecidableEq K]
(f : D → K)
(hz : ∀ (a : D), f a = 0 ↔ a = 0)
(c : Hex.SignedRemainderChain D)
(i : ℕ)
:
theorem
HexRealRootsTheory.Tarski.check_signed
{D : Type u}
{K : Type v}
[Zero D]
[DecidableEq D]
[Add D]
[Sub D]
[Mul D]
[NatCast D]
[Field K]
[DecidableEq K]
[LinearOrder K]
[IsStrictOrderedRing K]
(f : D → K)
(hz : ∀ (a : D), f a = 0 ↔ a = 0)
(ha : ∀ (a b : D), f (a + b) = f a + f b)
(hs : ∀ (a b : D), f (a - b) = f a - f b)
(hm : ∀ (a b : D), f (a * b) = f a * f b)
(sign : D → ℤ)
(hpos : ∀ (a : D), sign a = 1 ↔ 0 < f a)
(p g : Hex.DensePoly D)
(c : Hex.SignedRemainderChain D)
(hc : Hex.SignedRemainderChain.check sign p g c = true)
:
Literal signed replay supplies all the abstract chain relations, including termination at a possibly nonconstant gcd.
theorem
HexRealRootsTheory.Tarski.check_seed
{D : Type u}
{K : Type v}
[Zero D]
[DecidableEq D]
[Add D]
[Sub D]
[Mul D]
[NatCast D]
[Field K]
[DecidableEq K]
[LinearOrder K]
[IsStrictOrderedRing K]
(f : D → K)
(hz : ∀ (a : D), f a = 0 ↔ a = 0)
(ha : ∀ (a b : D), f (a + b) = f a + f b)
(hs : ∀ (a b : D), f (a - b) = f a - f b)
(hm : ∀ (a b : D), f (a * b) = f a * f b)
(hnat : ∀ (n : ℕ), f ↑n = ↑n)
(sign : D → ℤ)
(hpos : ∀ (a : D), sign a = 1 ↔ 0 < f a)
(p g : Hex.DensePoly D)
(c : Hex.SignedRemainderChain D)
(hc : Hex.SignedRemainderChain.check sign p g c = true)
:
TauCeti.Sturm.IsTarskiSeed (HexPolyTheory.Interpret.interpret f hz p) (HexPolyTheory.Interpret.interpret f hz g)
((chainPolys f hz c).getD 1 0)
The initial reduction gives precisely the seed congruence required by Sturm–Tarski, without assuming a constant terminal polynomial.
noncomputable def
HexRealRootsTheory.Tarski.variations
{K : Type v}
[Field K]
[LinearOrder K]
(cs : List (Polynomial K))
:
Hex.Endpoint K → ℕ
Sign variations of an interpreted chain at a finite or infinite endpoint.
Equations
Instances For
theorem
HexRealRootsTheory.Tarski.signs_variations
{D : Type u}
{K : Type v}
[Zero D]
[DecidableEq D]
[Field K]
[DecidableEq K]
[LinearOrder K]
[IsStrictOrderedRing K]
(f : D → K)
(hz : ∀ (a : D), f a = 0 ↔ a = 0)
(sign : D → ℤ)
{E : Type w}
(point : E → K)
(ends : Hex.EndpointSigns D E)
(hsign : ∀ (a : D), sign a = ↑(SignType.sign (f a)))
(heval :
∀ (p : Hex.DensePoly D) (a : E),
ends.evalSign p a = ↑(SignType.sign (Polynomial.eval (point a) (HexPolyTheory.Interpret.interpret f hz p))))
(cs : Array (Hex.DensePoly D))
(a : Hex.Endpoint E)
:
Hex.signVar (Hex.TarskiCertificate.signs sign ends cs a).toList = variations (List.map (HexPolyTheory.Interpret.interpret f hz) cs.toList) (Hex.Endpoint.map point a)
Literal endpoint signs give the abstract variations, for independent coefficient and endpoint representations.
theorem
HexRealRootsTheory.Tarski.variation_eq
{K : Type v}
[Field K]
[LinearOrder K]
[IsStrictOrderedRing K]
[IsRealClosed K]
(p g : Polynomial K)
(cs : List (Polynomial K))
(hc : TauCeti.Sturm.IsSignedRemainderSeq (p :: cs))
(seed : TauCeti.Sturm.IsTarskiSeed p g (cs.head?.getD 0))
(a b : Hex.Endpoint K)
(hab :
match a, b with
| Hex.Endpoint.negInf, Hex.Endpoint.finite value => True
| Hex.Endpoint.negInf, Hex.Endpoint.posInf => True
| Hex.Endpoint.finite value, Hex.Endpoint.posInf => True
| Hex.Endpoint.finite x, Hex.Endpoint.finite y => x < y
| x, x_1 => False)
(ha : ∀ (x : K), a = Hex.Endpoint.finite x → Polynomial.eval x p ≠ 0)
(hb : ∀ (x : K), b = Hex.Endpoint.finite x → Polynomial.eval x p ≠ 0)
:
The shared signed-remainder theorem on an open interval with structural infinite endpoints. Positive scalings and nonconstant terminal gcds are allowed.