theorem Hex.DyadicComplexBall.center_re (b : DyadicComplexBall) : b.center.re = HexRootsMathlib.Dyadic.toReal b.re

The centre of a ball, componentwise.

theorem Hex.DyadicComplexBall.center_im (b : DyadicComplexBall) : b.center.im = HexRootsMathlib.Dyadic.toReal b.im

theorem Hex.DyadicComplexBall.dist_le_of_mem {b : DyadicComplexBall} {z : ℂ} (h : z ∈ b.set) : dist z b.center ≤ b.realRadius

A point of a ball is within the radius of the centre.

theorem Hex.DyadicComplexBall.radius_nonneg_of_mem {b : DyadicComplexBall} {z : ℂ} (h : z ∈ b.set) : 0 ≤ b.realRadius

A ball with a point has nonnegative radius.

theorem Hex.DyadicComplexBall.meets_of_mem_set {b₁ b₂ : DyadicComplexBall} {z : ℂ} (h₁ : z ∈ b₁.set) (h₂ : z ∈ b₂.set) : b₁.meets b₂ = true

Two balls with a common point meet.

theorem Hex.DyadicComplexBall.dist_le_of_meets {b₁ b₂ : DyadicComplexBall} {z w : ℂ} (h : b₁.meets b₂ = true) (hz : z ∈ b₁.set) (hw : w ∈ b₂.set) : dist z w ≤ 2 * (b₁.realRadius + b₂.realRadius)

Points of two balls that meet are within twice the radius sum of each other.

theorem Hex.AlgebraicNumber.conj_mem_mirrorBall {b : DyadicComplexBall} {z : ℂ} (h : z ∈ b.set) : (starRingEnd ℂ) z ∈ (mirrorBall b).set

The mirror ball contains the conjugates of the ball's points.

theorem Hex.AlgebraicNumber.approx_radius_separationPrec (a : AlgebraicNumber) (p : ZPoly) : (a.approx (separationPrec p)).realRadius ≤ 2 ^ (-↑(mahlerPrec p)) / 4

At separationPrec p, the ball radius is at most a quarter of the separation guaranteed by mahlerPrec p, in the form the proofs use.

theorem Hex.AlgebraicNumber.eq_of_meets {p : ZPoly} (hp : p ≠ 0) {a b : AlgebraicNumber} (ha : (HexRootsMathlib.toPolyℂ p).IsRoot a.toComplex) (hb : (HexRootsMathlib.toPolyℂ p).IsRoot b.toComplex) {ballA ballB : DyadicComplexBall} (hA : a.toComplex ∈ ballA.set) (hB : b.toComplex ∈ ballB.set) (hrA : ballA.realRadius ≤ 2 ^ (-↑(mahlerPrec p)) / 4) (hrB : ballB.realRadius ≤ 2 ^ (-↑(mahlerPrec p)) / 4) (hmeets : ballA.meets ballB = true) : a.toComplex = b.toComplex

Two roots of p whose balls at separationPrec p meet are equal.

theorem Hex.AlgebraicNumber.conj_toComplex (a : AlgebraicNumber) : a.conj.toComplex = (starRingEnd ℂ) a.toComplex

conj is complex conjugation.

theorem Hex.AlgebraicNumber.isRoot_mul_left (a b : AlgebraicNumber) : (HexRootsMathlib.toPolyℂ (a.p * b.p)).IsRoot a.toComplex

A root of the product of two minimal polynomials.

theorem Hex.AlgebraicNumber.isRoot_mul_right (a b : AlgebraicNumber) : (HexRootsMathlib.toPolyℂ (a.p * b.p)).IsRoot b.toComplex

theorem Hex.AlgebraicNumber.mul_p_ne_zero (a b : AlgebraicNumber) : a.p * b.p ≠ 0

The product of two minimal polynomials is nonzero.

theorem Hex.AlgebraicNumber.abs_re_sub_center_le (a : AlgebraicNumber) (prec : ℤ) : |a.toComplex.re - HexRootsMathlib.Dyadic.toReal (a.approx prec).re| ≤ (a.approx prec).realRadius

The real part of a number is within the ball radius of the centre's.

theorem Hex.AlgebraicNumber.realCompare_eq (a b : AlgebraicNumber) (ha : a.isReal = true) (hb : b.isReal = true) : a.realCompare b = compare a.toComplex.re b.toComplex.re

realCompare is the order of the real parts.

theorem Hex.AlgebraicNumber.toPolyℂ_xsq_add_one : HexRootsMathlib.toPolyℂ (DensePoly.ofCoeffs #[1, 0, 1]) = Polynomial.X ^ 2 + 1

The complex interpretation of X² + 1.

theorem Hex.AlgebraicNumber.three_le_mahlerPrec (p : ZPoly) : 3 ≤ mahlerPrec p

mahlerPrec is at least three.

theorem Hex.AlgebraicNumber.square_im_pos_iff {d : AlgebraicNumber} (hd : d ∈ ZPoly.algebraicRoots (DensePoly.ofCoeffs #[1, 0, 1])) : 0 < (↑d.rep).square.im ↔ d.toComplex = Complex.I

A root of X² + 1 has a stored isolation centre in the upper half plane exactly when it is the imaginary unit.

theorem Hex.AlgebraicNumber.I_toComplex : I.toComplex = Complex.I

I is the imaginary unit.

theorem Hex.AlgebraicNumber.ofPoint_toComplex (re im : ℚ) : (ofPoint re im).toComplex = ↑re + ↑im * Complex.I

The complex value of a rational point.

theorem Hex.AlgebraicNumber.ofPoint_neg_toComplex (re im : ℚ) : (ofPoint re (-im)).toComplex = (starRingEnd ℂ) (↑re + ↑im * Complex.I)

The conjugate of a rational point.

theorem Hex.AlgebraicNumber.distSqTo_toComplex (a : AlgebraicNumber) (re im : ℚ) : (a.distSqTo re im).toComplex = ↑(‖a.toComplex - (↑re + ↑im * Complex.I)‖ ^ 2)

distSqTo is the squared distance to the point.

theorem Hex.AlgebraicNumber.distSqTo_isReal (a : AlgebraicNumber) (re im : ℚ) : (a.distSqTo re im).isReal = true

distSqTo is real.

@[reducible, inline]

noncomputable abbrev Hex.AlgebraicNumber.point (re im : ℚ) : ℂ

The point named by two rationals.

Equations

• Hex.AlgebraicNumber.point re im = ↑re + ↑im * Complex.I

theorem Hex.AlgebraicNumber.absRat_cast (q : ℚ) : ↑(absRat q) = |↑q|

theorem Hex.AlgebraicNumber.ballDistSq_cast (b : DyadicComplexBall) (re im : ℚ) : ↑(ballDistSq b re im) = ‖b.center - point re im‖ ^ 2

The squared distance from the point to the centre, as a real.

theorem Hex.AlgebraicNumber.norm_center_sub_le (b : DyadicComplexBall) (re im : ℚ) : ‖b.center - point re im‖ ≤ ↑(ballDistBound b re im)

The centre distance is at most the coordinate bound.

theorem Hex.AlgebraicNumber.realRadius_eq (b : DyadicComplexBall) : b.realRadius = ↑b.radius.toRat

theorem Hex.AlgebraicNumber.sq_norm_le_ballUpper {b : DyadicComplexBall} {z : ℂ} (hz : z ∈ b.set) (re im : ℚ) : ‖z - point re im‖ ^ 2 ≤ ↑(ballUpper b re im)

The squared distance from the point to any point of a ball is at most ballUpper.

theorem Hex.AlgebraicNumber.ballLower_le_sq_norm {b : DyadicComplexBall} {z : ℂ} (hz : z ∈ b.set) (re im : ℚ) : ↑(ballLower b re im) ≤ ‖z - point re im‖ ^ 2

The squared distance from the point to any point of a ball is at least ballLower.

theorem Hex.AlgebraicNumber.realCompare_distSqTo_lt (c b : AlgebraicNumber) (re im : ℚ) : ((c.distSqTo re im).realCompare (b.distSqTo re im) == Ordering.lt) = true ↔ ‖c.toComplex - point re im‖ < ‖b.toComplex - point re im‖

The exact comparison of squared distances decides the strict order of distances.

theorem Hex.AlgebraicNumber.certifiedNearest_sound {roots : Array AlgebraicNumber} {a : AlgebraicNumber} {prec : ℤ} {re im : ℚ} (h : certifiedNearest roots a prec re im = true) (c : AlgebraicNumber) : c ∈ roots → ‖a.toComplex - point re im‖ ≤ ‖c.toComplex - point re im‖

A certified nearest root is nearest.

theorem Hex.AlgebraicNumber.exactStep_none (re im : ℚ) (c : AlgebraicNumber) : exactStep re im none c = some c

theorem Hex.AlgebraicNumber.exactStep_some (re im : ℚ) (b c : AlgebraicNumber) : exactStep re im (some b) c = if ((c.distSqTo re im).realCompare (b.distSqTo re im) == Ordering.lt) = true then some c else some b

theorem Hex.AlgebraicNumber.foldl_exactStep (re im : ℚ) (l : List AlgebraicNumber) (acc : Option AlgebraicNumber) : match List.foldl (exactStep re im) acc l with | none => l = [] ∧ acc = none | some r => (r ∈ l ∨ acc = some r) ∧ (∀ c ∈ l, ‖r.toComplex - point re im‖ ≤ ‖c.toComplex - point re im‖) ∧ ∀ (b : AlgebraicNumber), acc = some b → ‖r.toComplex - point re im‖ ≤ ‖b.toComplex - point re im‖

The fold behind exactNearest, on lists.

theorem Hex.AlgebraicNumber.exactNearest_spec (roots : Array AlgebraicNumber) (re im : ℚ) : match exactNearest roots re im with | none => roots = #[] | some r => r ∈ roots ∧ ∀ c ∈ roots, ‖r.toComplex - point re im‖ ≤ ‖c.toComplex - point re im‖

exactNearest on a nonempty array is a nearest root.

theorem Hex.ZPoly.algebraicRoots_ne_empty {p : ZPoly} (hp : 0 < DensePoly.natDegree p) : p.algebraicRoots ≠ #[]

A polynomial of positive degree has a root in algebraicRoots.

theorem Hex.ZPoly.rootNear_mem (p : ZPoly) (hp : 0 < DensePoly.natDegree p) (re im : ℚ) : p.rootNear re im ∈ p.algebraicRoots

rootNear returns a root.

theorem Hex.ZPoly.rootNear_nearest (p : ZPoly) (re im : ℚ) (b : AlgebraicNumber) (hb : b ∈ p.algebraicRoots) : ‖(p.rootNear re im).toComplex - AlgebraicNumber.point re im‖ ≤ ‖b.toComplex - AlgebraicNumber.point re im‖

rootNear is nearest.

theorem Hex.ZPoly.rootNear_of_close (a : AlgebraicNumber) (re im : ℚ) (h : ‖AlgebraicNumber.point re im - a.toComplex‖ < 2 * (2 ^ (-↑(mahlerPrec a.p)) * (1449 / 1024))) : a.p.rootNear re im = a

A point within half the guaranteed separation of a number names it.