Documentation

HexRCF.Isolations

source
def Hex.RCF.IsolationCert.toLiteral (replay : SturmReplay) (cert : IsolationCert) (h : check replay cert = true) :
HexRealRootsMathlib.LiteralIsolations replay.count replay.total

Package an accepted raw certificate into the generic literal-isolation interface.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem Hex.RCF.IsolationCert.size_toLiteral (replay : SturmReplay) (cert : IsolationCert) (h : check replay cert = true) :
    (toLiteral replay cert h).isolations.size = cert.intervals.size

    Converting an isolation certificate preserves the number of intervals.

    source
    theorem Hex.RCF.IsolationCert.interval_toLiteral (replay : SturmReplay) (cert : IsolationCert) (h : check replay cert = true) (i : ℕ) (hi : i < (toLiteral replay cert h).isolations.size) :
    (toLiteral replay cert h).isolations[i].interval = cert.intervals[i]

    The interval at each index is unchanged by conversion to literal isolations.

    source
    theorem Hex.RCF.IsolationCert.existsUnique_root {f : ZPoly} {replay : SturmReplay} {cert : IsolationCert} (hreplay : SturmReplay.check f replay = true) (hcert : check replay cert = true) (i : Fin cert.intervals.size) :
    ∃! r : ℝ, (HexRealRootsMathlib.toPolyℝ f).IsRoot r ∧ HexRealRootsMathlib.Literal.InInterval cert.intervals[i] r

    Every accepted interval contains exactly one real root of the replay head.

    source
    theorem Hex.RCF.IsolationCert.isolates_of_check {f : ZPoly} {replay : SturmReplay} {cert : IsolationCert} (hreplay : SturmReplay.check f replay = true) (hcert : check replay cert = true) (r : ℝ) :
    (HexRealRootsMathlib.toPolyℝ f).IsRoot r → ∃! i : Fin cert.intervals.size, HexRealRootsMathlib.Literal.InInterval cert.intervals[i] r

    Accepted raw intervals isolate every real root of the replay head at a unique original array index.