@[simp]

theorem HexRootsMathlib.GaussDyadic.toComplex_zero : toComplex (0, 0) = 0

The zero Gaussian dyadic embeds as complex zero.

@[simp]

theorem HexRootsMathlib.GaussDyadic.toReal_lo (z : Hex.GaussDyadic) : Dyadic.toReal z.lo = max |(toComplex z).re| |(toComplex z).im|

The real value of the executable lower modulus bound.

@[simp]

theorem HexRootsMathlib.GaussDyadic.toReal_hi (z : Hex.GaussDyadic) : Dyadic.toReal z.hi = |(toComplex z).re| + |(toComplex z).im|

The real value of the executable upper modulus bound.

theorem HexRootsMathlib.GaussDyadic.lo_le_norm (z : Hex.GaussDyadic) : Dyadic.toReal z.lo ≤ ‖toComplex z‖

The executable lo bound is below the complex modulus.

theorem HexRootsMathlib.GaussDyadic.norm_le_sqrt_two_mul_lo (z : Hex.GaussDyadic) : ‖toComplex z‖ ≤ √2 * Dyadic.toReal z.lo

The complex modulus is at most √2 times the executable lo bound.

theorem HexRootsMathlib.GaussDyadic.norm_le_hi (z : Hex.GaussDyadic) : ‖toComplex z‖ ≤ Dyadic.toReal z.hi

The complex modulus is below the executable hi bound.

theorem HexRootsMathlib.GaussDyadic.hi_le_sqrt_two_mul_norm (z : Hex.GaussDyadic) : Dyadic.toReal z.hi ≤ √2 * ‖toComplex z‖

The executable hi bound is at most √2 times the complex modulus.

theorem HexRootsMathlib.sqrt2Lo_lt_sqrt_two : Dyadic.toReal Hex.sqrt2Lo < √2

The executable lower approximation 181/128 is strictly below √2.

theorem HexRootsMathlib.sqrt_two_lt_sqrt2Hi : √2 < Dyadic.toReal Hex.sqrt2Hi

The executable upper approximation 1449/1024 is strictly above √2.

def HexRootsMathlib.SquareBounds.Contains (b : Hex.SquareBounds) (s : Hex.DyadicSquare) : Prop

A computed bounding box contains the full coordinate extent of a square.

Equations

• One or more equations did not get rendered due to their size.

theorem HexRootsMathlib.SquareBounds.bounds_contains (s : Hex.DyadicSquare) : Contains s.bounds s

A square's own bounds contain it.

theorem HexRootsMathlib.SquareBounds.contains_merge_left {b : Hex.SquareBounds} {s t : Hex.DyadicSquare} (h : Contains b s) : Contains (b.merge t) s

Merging another square into a bounding box keeps everything it already contained.

theorem HexRootsMathlib.SquareBounds.contains_merge_right (b : Hex.SquareBounds) (s : Hex.DyadicSquare) : Contains (b.merge s) s

A merged bounding box contains the newly merged square.

theorem HexRootsMathlib.SquareBounds.contains_extend_old {b : Option Hex.SquareBounds} {s t : Hex.DyadicSquare} (h : ∃ (box : Hex.SquareBounds), b = some box ∧ Contains box s) : ∃ (box : Hex.SquareBounds), Hex.SquareBounds.extend b t = some box ∧ Contains box s

Extending an optional bounding box keeps every previously contained square.

theorem HexRootsMathlib.SquareBounds.contains_extend_new (b : Option Hex.SquareBounds) (s : Hex.DyadicSquare) : ∃ (box : Hex.SquareBounds), Hex.SquareBounds.extend b s = some box ∧ Contains box s

Extending an optional bounding box contains the newly added square.

theorem HexRootsMathlib.SquareBounds.mem_boundingBox {squares : Array Hex.DyadicSquare} {s : Hex.DyadicSquare} (hs : s ∈ squares.toList) : ∃ (box : Hex.SquareBounds), Hex.boundingBox squares = some box ∧ Contains box s

Every input square is contained in the exact bounding box returned by the executable fold.

def HexRootsMathlib.supNorm (z : ℂ) : ℝ

The sup norm on ℂ, used to view an axis-aligned square as a ball.

Equations

• HexRootsMathlib.supNorm z = max |z.re| |z.im|

theorem HexRootsMathlib.supNorm_add_le (z w : ℂ) : supNorm (z + w) ≤ supNorm z + supNorm w

The complex sup norm satisfies the triangle inequality.

def HexRootsMathlib.supDist (z w : ℂ) : ℝ

The distance associated to supNorm.

Equations

• HexRootsMathlib.supDist z w = HexRootsMathlib.supNorm (z - w)

def HexRootsMathlib.supClosedBall (c : ℂ) (r : ℝ) : Set ℂ

A closed sup-norm ball in ℂ.

Equations

• HexRootsMathlib.supClosedBall c r = {z : ℂ | HexRootsMathlib.supDist z c ≤ r}

def HexRootsMathlib.supOpenBall (c : ℂ) (r : ℝ) : Set ℂ

An open sup-norm ball in ℂ.

Equations

• HexRootsMathlib.supOpenBall c r = {z : ℂ | HexRootsMathlib.supDist z c < r}

def HexRootsMathlib.DyadicSquare.center (s : Hex.DyadicSquare) : ℂ

The complex centre of a dyadic square.

Equations

• HexRootsMathlib.DyadicSquare.center s = HexRootsMathlib.GaussDyadic.toComplex s.center

def HexRootsMathlib.DyadicSquare.halfWidth (s : Hex.DyadicSquare) : ℝ

The real half-width of a dyadic square.

Equations

• HexRootsMathlib.DyadicSquare.halfWidth s = HexRootsMathlib.Dyadic.toReal s.halfWidth

noncomputable def HexRootsMathlib.DyadicSquare.radius (s : Hex.DyadicSquare) : ℝ

The Euclidean radius of the square's circumscribed disc.

Equations

• HexRootsMathlib.DyadicSquare.radius s = HexRootsMathlib.DyadicSquare.halfWidth s * √2

def HexRootsMathlib.DyadicSquare.closedSquare (s : Hex.DyadicSquare) : Set ℂ

The closed axis-aligned square represented by s.

Equations

• HexRootsMathlib.DyadicSquare.closedSquare s = HexRootsMathlib.supClosedBall (HexRootsMathlib.DyadicSquare.center s) (HexRootsMathlib.DyadicSquare.halfWidth s)

def HexRootsMathlib.DyadicSquare.openSquare (s : Hex.DyadicSquare) : Set ℂ

The interior of the axis-aligned square represented by s.

Equations

• HexRootsMathlib.DyadicSquare.openSquare s = HexRootsMathlib.supOpenBall (HexRootsMathlib.DyadicSquare.center s) (HexRootsMathlib.DyadicSquare.halfWidth s)

def HexRootsMathlib.DyadicSquare.disc (s : Hex.DyadicSquare) : Set ℂ

The open circumscribed disc of s.

Equations

• HexRootsMathlib.DyadicSquare.disc s = Metric.ball (HexRootsMathlib.DyadicSquare.center s) (HexRootsMathlib.DyadicSquare.radius s)

def HexRootsMathlib.DyadicSquare.closedDisc (s : Hex.DyadicSquare) : Set ℂ

The closed circumscribed disc of s.

Equations

• HexRootsMathlib.DyadicSquare.closedDisc s = Metric.closedBall (HexRootsMathlib.DyadicSquare.center s) (HexRootsMathlib.DyadicSquare.radius s)

@[simp]

theorem HexRootsMathlib.DyadicSquare.center_eq (s : Hex.DyadicSquare) : center s = GaussDyadic.toComplex s.center

@[simp]

theorem HexRootsMathlib.DyadicSquare.halfWidth_eq (s : Hex.DyadicSquare) : halfWidth s = 2 ^ (-s.prec)

@[simp]

theorem HexRootsMathlib.DyadicSquare.radius_eq (s : Hex.DyadicSquare) : radius s = 2 ^ (-s.prec) * √2

@[simp]

theorem HexRootsMathlib.DyadicSquare.disc_eq (s : Hex.DyadicSquare) : disc s = Metric.ball (center s) (2 ^ (-s.prec) * √2)

theorem HexRootsMathlib.DyadicSquare.closedSquare_eq_supClosedBall (s : Hex.DyadicSquare) : closedSquare s = supClosedBall (center s) (halfWidth s)

The closed square is the sup-norm closed ball of half-width radius about the centre. Characterising lemma recording what is otherwise a definitional equality, so consumers need not unfold closedSquare.

theorem HexRootsMathlib.DyadicSquare.center_mem_closedSquare (s : Hex.DyadicSquare) : center s ∈ closedSquare s

The centre belongs to its closed square.

theorem HexRootsMathlib.DyadicSquare.mem_closedSquare_iff_re_im (s : Hex.DyadicSquare) (z : ℂ) : z ∈ closedSquare s ↔ |z.re - Dyadic.toReal s.re| ≤ halfWidth s ∧ |z.im - Dyadic.toReal s.im| ≤ halfWidth s

Membership in a closed dyadic square is exactly the pair of coordinate bounds around its centre.

theorem HexRootsMathlib.DyadicSquare.radiusLo_eq (s : Hex.DyadicSquare) : Dyadic.toReal s.radiusLo = halfWidth s * Dyadic.toReal Hex.sqrt2Lo

theorem HexRootsMathlib.DyadicSquare.radiusHi_eq (s : Hex.DyadicSquare) : Dyadic.toReal s.radiusHi = halfWidth s * Dyadic.toReal Hex.sqrt2Hi

theorem HexRootsMathlib.DyadicSquare.radiusLo_lt_radius (s : Hex.DyadicSquare) : Dyadic.toReal s.radiusLo < radius s

theorem HexRootsMathlib.DyadicSquare.radius_lt_radiusHi (s : Hex.DyadicSquare) : radius s < Dyadic.toReal s.radiusHi

@[simp]

theorem HexRootsMathlib.DyadicSquare.toReal_distSq (z w : Hex.GaussDyadic) : Dyadic.toReal (z.distSq w) = dist (GaussDyadic.toComplex z) (GaussDyadic.toComplex w) ^ 2

The exact executable squared centre distance casts to the square of the Euclidean distance.

theorem HexRootsMathlib.DyadicSquare.discContains_iff_mem_closedDisc (s : Hex.DyadicSquare) (z : Hex.GaussDyadic) : s.discContains z = true ↔ GaussDyadic.toComplex z ∈ closedDisc s

The exact executable point-in-disc test is membership in the represented closed circumscribed disc.

theorem HexRootsMathlib.DyadicSquare.closedDisc_disjoint_of_discsMeet_eq_false (s t : Hex.DyadicSquare) (h : s.discsMeet t = false) : Disjoint (closedDisc s) (closedDisc t)

A negative executable disc-intersection test certifies disjoint closed circumscribed discs.

theorem HexRootsMathlib.DyadicSquare.dist_center_le_of_discsMeet {s t : Hex.DyadicSquare} (h : s.discsMeet t = true) : dist (center s) (center t) ≤ radius s + radius t

A positive executable disc-intersection test is the corresponding centre distance bound.

theorem HexRootsMathlib.DyadicSquare.closedDisc_disjoint_of_pairwiseDisjoint {ss : Array Hex.DyadicSquare} (h : Hex.pairwiseDisjoint ss = true) {i j : ℕ} (hi : i < ss.size) (hj : j < ss.size) (hij : i < j) : Disjoint (closedDisc ss[i]) (closedDisc ss[j])

The executable array test gives semantic disjointness for every ordered pair of stored squares.

theorem HexRootsMathlib.DyadicSquare.closedDisc_subset_of_discInside {inner outer : Hex.DyadicSquare} (h : inner.discInside outer = true) : closedDisc inner ⊆ closedDisc outer

The exact executable disc-containment check implies containment of the represented closed circumscribed discs.

theorem HexRootsMathlib.DyadicSquare.closedSquare_subset_of_squareInside {inner outer : Hex.DyadicSquare} (h : inner.squareInside outer = true) : closedSquare inner ⊆ closedSquare outer

The exact executable square-containment check implies containment of the represented closed sup-norm squares.

theorem HexRootsMathlib.DyadicSquare.closedSquare_subset_encSquare {squares : Array Hex.DyadicSquare} {s : Hex.DyadicSquare} (hs : s ∈ squares.toList) : closedSquare s ⊆ closedSquare (Hex.encSquare squares)

Every input square is contained in the power-of-two square constructed from its array's exact bounding box.

theorem HexRootsMathlib.DyadicSquare.closedSquare_subset_closedDisc (s : Hex.DyadicSquare) : closedSquare s ⊆ closedDisc s

The square is contained in its closed circumscribed Euclidean disc.

theorem HexRootsMathlib.DyadicSquare.closedSquare_subset_ball_radiusHi (s : Hex.DyadicSquare) : closedSquare s ⊆ Metric.ball (center s) (Dyadic.toReal s.radiusHi)

The closed square lies in the open disc obtained from the executable strict upper radius bound.