Planar Isometries

This file defines planar isometries (rotations + translations) with rational approximations.

structure Moser.DirectIsometry : Type

A planar isometry represented by rotation angle (via sin/cos) then a translation

• cos : ℚ

  Cosine of rotation angle (rational approximation)

• sin : ℚ

  Sine of rotation angle (rational approximation)

• translation : RationalPoint

  Translation vector

• isValid : self.cos * self.cos + self.sin * self.sin = 1

  sin cos

def Moser.DirectIsometry.id : DirectIsometry

The identity isometry

Equations

• Moser.DirectIsometry.id = { cos := 1, sin := 0, translation := 0, isValid := Moser.DirectIsometry.id._proof_1 }

def Moser.DirectIsometry.apply (iso : DirectIsometry) (p : RationalPoint) : RationalPoint

Apply the isometry to a point

Equations

• iso.apply p = ![iso.cos * p 0 - iso.sin * p 1, iso.sin * p 0 + iso.cos * p 1] + iso.translation

theorem Moser.DirectIsometry.apply_injective (iso : DirectIsometry) : Function.Injective iso.apply

Applying a DirectIsometry is an injective function on RationalPoint.

theorem Moser.DirectIsometry.apply_surjective (iso : DirectIsometry) : Function.Surjective iso.apply

Applying a DirectIsometry is a surjective function on RationalPoint.

@[implicit_reducible]

instance Moser.DirectIsometry.instFunLikeRationalPoint : FunLike DirectIsometry RationalPoint RationalPoint

Equations

• Moser.DirectIsometry.instFunLikeRationalPoint = { coe := Moser.DirectIsometry.apply, coe_injective' := Moser.DirectIsometry.instFunLikeRationalPoint._proof_1 }

def Moser.DirectIsometry.applyPolygon (iso : DirectIsometry) (poly : ConvexPolygon) : ConvexPolygon

Apply the isometry to a polygon

Equations

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

def Moser.DirectIsometry.compose (iso1 iso2 : DirectIsometry) : DirectIsometry

Compose two isometries

Equations

• iso1.compose iso2 = { cos := iso1.cos * iso2.cos - iso1.sin * iso2.sin, sin := iso1.sin * iso2.cos + iso1.cos * iso2.sin, translation := iso1.apply iso2.translation, isValid := ⋯ }