Worms

This file defines worms as piecewise linear paths of unit length.

def Moser.sqrtApprox (s epsilon : ℚ) (fuel : ℕ := 100) : ℚ

Approximate sqrt(s) using Newton's method (Babylonian method). Given s ≥ 0 and epsilon > 0, returns a rational r such that |r - sqrt(s)| < epsilon

Equations

• Moser.sqrtApprox s epsilon fuel = if s ≤ 0 then 0 else Moser.sqrtApprox.newton s epsilon (max 1 s) fuel

@[irreducible]

def Moser.sqrtApprox.newton (s epsilon x : ℚ) (n : ℕ) : ℚ

One step of the Newton iteration on x, recursing up to n more times.

Equations

• Moser.sqrtApprox.newton s epsilon x n = if n = 0 then x else have x' := (x + s / x) / 2; if |x' * x' - s| < epsilon * epsilon then x' else Moser.sqrtApprox.newton s epsilon x' (n - 1)

def Moser.distanceApprox (p q : RationalPoint) (epsilon : ℚ) : ℚ

Approximate the Euclidean distance between two points to within epsilon. Returns a rational d such that |d - dist(p,q)| < epsilon

Equations

• Moser.distanceApprox p q epsilon = Moser.sqrtApprox (p.distSq q) epsilon

def Moser.totalLengthApprox (vertices : List RationalPoint) (epsilon : ℚ) : ℚ

Compute an approximate total length of a path given by vertices

Equations

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

structure Moser.Worm : Type

A worm is a piecewise linear path (at least 2 vertices)

• vertices : List RationalPoint

  The vertices defining the path

• nonempty : self.vertices.length ≥ 2

  The path has at least 2 vertices

def Moser.Worm.scaleRationalPoint (s : ℚ) (p : RationalPoint) : RationalPoint

Scale a point by a rational factor

Equations

• Moser.Worm.scaleRationalPoint s p = ![s * p 0, s * p 1]

def Moser.Worm.scale (w : Worm) (s : ℚ) : Worm

Scale all vertices of a worm by a factor

Equations

• w.scale s = { vertices := List.map (Moser.Worm.scaleRationalPoint s) w.vertices, nonempty := ⋯ }

def Moser.Worm.lengthApprox (w : Worm) (epsilon : ℚ) : ℚ

Get the approximate total length of the worm

Equations

• w.lengthApprox epsilon = Moser.totalLengthApprox w.vertices epsilon

def Moser.Worm.scaleToUnit (w : Worm) (epsilon : ℚ) : Worm

Scale a worm to have approximately unit length. Returns the scaled worm. The scaling factor is 1/length.

Equations

• w.scaleToUnit epsilon = if w.lengthApprox epsilon ≤ 0 then w else w.scale (1 / w.lengthApprox epsilon)

def Moser.Worm.toConvexPolygon (w : Worm) : ConvexPolygon

Convert worm vertices to a convex polygon

Equations

• w.toConvexPolygon = sorry

def Moser.Worm.convexHullPolygon (w : Worm) : ConvexPolygon

Get the convex hull as a ConvexPolygon

Equations

• w.convexHullPolygon = w.toConvexPolygon

structure Moser.UnitWorm : Type

A unit worm is a worm with total length approximately 1

• worm : Worm

  The underlying worm

• unitLength (epsilon : ℚ) : epsilon > 0 → |self.worm.lengthApprox epsilon - 1| < epsilon

  The total length is approximately 1 (converges to 1 as epsilon → 0)

def Moser.UnitWorm.vertices (w : UnitWorm) : List RationalPoint

Get the vertices of a unit worm

Equations

• w.vertices = w.worm.vertices

def Moser.UnitWorm.toConvexPolygon (w : UnitWorm) : ConvexPolygon

Convert to a convex polygon

Equations

• w.toConvexPolygon = w.worm.toConvexPolygon

def Moser.Worm.toUnitWorm (w : Worm) (epsilon : ℚ) : UnitWorm

Convert a worm to a unit worm by scaling to unit length. The epsilon parameter controls the precision of the length computation.

Equations

• w.toUnitWorm epsilon = sorry