Half Spaces and Lines

This file defines closed and open half-spaces and lines over rational points.

structure ClosedHalfSpace : Type

A closed half-space in ℚ², given by a basepoint and an inward-pointing normal.

• basepoint : RationalPoint

  A point on the boundary line of the half-space.

• normal : RationalPoint

  The normal, where if the dot product of this with (p - basepoint) is nonnegative, then p is in the half-space.

• normal_pos : 0 < self.normal.lengthSq

  The normal must be nonzero (positive squared length).

structure OpenHalfSpace : Type

An open half-space in ℚ², given by a basepoint and an inward-pointing normal.

• basepoint : RationalPoint

  A point on the boundary line of the half-space.

• normal : RationalPoint

  The normal, where if the dot product of this with (p - basepoint) is positive, then p is in the half-space.

• normal_pos : 0 < self.normal.lengthSq

  The normal must be nonzero (positive squared length).

def OpenHalfSpace.contains (h : OpenHalfSpace) (p : RationalPoint) : Bool

Decide whether the point p lies in the open half-space h.

Equations

• h.contains p = decide (h.normal.dotProduct (p - h.basepoint) > 0)

def RationalPoint.toStrictlyLeft (p1 p2 : RationalPoint) (hne : p1 ≠ p2) : OpenHalfSpace

The open half-space strictly to the left of the directed segment from p1 to p2.

Equations

• p1.toStrictlyLeft p2 hne = { basepoint := p1, normal := (p2 - p1).rotate90Counterclockwise, normal_pos := ⋯ }

structure Line : Type

A line in ℚ², given by a point on the line and a nonzero direction vector.

• point : RationalPoint

  A point lying on the line.

• direction : RationalPoint

  A nonzero direction vector for the line.

• direction_pos : 0 < self.direction.lengthSq

  direction must be nonzero

def Line.parallel (l1 l2 : Line) : Bool

Decide whether two lines l1 and l2 are parallel (cross product of directions is zero).

Equations

• l1.parallel l2 = decide (l1.direction.crossProduct l2.direction = 0)

def Line.intersection (l1 l2 : Line) : Option RationalPoint

Note AI generated

Equations

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

def ClosedHalfSpace.boundaryLine (h : ClosedHalfSpace) : Line

The boundary line of a closed half-space (perpendicular to its normal).

Equations

• h.boundaryLine = { point := h.basepoint, direction := h.normal.rotate90Counterclockwise, direction_pos := ⋯ }

def ClosedHalfSpace.lineIntersection (h1 h2 : ClosedHalfSpace) : Option RationalPoint

Given two closed half-spaces, compute the intersection point of their boundary lines if it exists. Returns none if the lines are parallel (no intersection or infinite intersection).

Equations

• h1.lineIntersection h2 = h1.boundaryLine.intersection h2.boundaryLine

def ClosedHalfSpace.contains (h : ClosedHalfSpace) (p : RationalPoint) : Bool

Decide whether the point p lies in the closed half-space h.

Equations

• h.contains p = decide (h.normal.dotProduct (p - h.basepoint) ≥ 0)

def RationalPoint.toWeaklyLeft (p1 p2 : RationalPoint) (hne : p1 ≠ p2) : ClosedHalfSpace

The closed half-space weakly to the left of the directed segment from p1 to p2.

Equations

• p1.toWeaklyLeft p2 hne = { basepoint := p1, normal := (p2 - p1).rotate90Counterclockwise, normal_pos := ⋯ }

def RationalPoint.toWeaklyRight (p1 p2 : RationalPoint) (hne : p1 ≠ p2) : ClosedHalfSpace

The closed half-space weakly to the right of the directed segment from p1 to p2.

Equations

• p1.toWeaklyRight p2 hne = { basepoint := p1, normal := (p1 - p2).rotate90Counterclockwise, normal_pos := ⋯ }

def ClosedHalfSpace.moveInward (h : ClosedHalfSpace) (dist tolerance : ℚ) (hdist : 0 < dist) (htol : 0 < tolerance) : ClosedHalfSpace

Change the half-space by moving the basepoint inward by at least dist in the normal direction, and at most dist + tolerance to account for numerical issues.

Equations

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