tatarize

I have a BS in CS and tend to work with real world 2D geometric plotter technologies.

tatarize / affine.lean

Created May 4, 2023 08:52

LeanSolver code for creating an affine transformation matrix from 4 points.

tatarize / unitsquare.lean

Created May 5, 2023 22:36

Lean Code for the Unit Square transformation from points (x1,x1), (x2,y2), (x3,y3), (x4,y4) to (0,0), (0,1), (1,1), (1,0).

	import tactic

	def transform : ℚ × ℚ × ℚ × ℚ × ℚ × ℚ × ℚ × ℚ × ℚ → ℚ × ℚ → ℚ × ℚ
	\| (a, b, c, d, e, f, g, h, i) (x, y) := ((a * x + b * y + c) / (g * x + h * y + i), (d * x + e * y + f) / (g * x + h * y + i))

	def xy : ℚ × ℚ := (0, 0)
	def xy' : ℚ × ℚ := (0, 1)
	def x'y' : ℚ × ℚ := (1, 1)
	def x'y : ℚ × ℚ := (1, 0)

tatarize / 4-to-4.lean

Created May 6, 2023 10:57

4-to-4 matrix lean.

	import tactic

	def transform : ℚ × ℚ × ℚ × ℚ × ℚ × ℚ × ℚ × ℚ × ℚ → ℚ × ℚ → ℚ × ℚ
	\| (a, b, c, d, e, f, g, h, i) (x, y) := ((a * x + b * y + c) / (g * x + h * y + i), (d * x + e * y + f) / (g * x + h * y + i))


	example (ax1 ay1 ax2 ay2 ax3 ay3 ax4 ay4 bx1 by1 bx2 by2 bx3 by3 bx4 by4 a b c d e f g h i : ℚ)
	: transform (a, b, c, d, e, f, g, h, i)(ax1, ay1) = (bx1, by1)
	∧ transform (a, b, c, d, e, f, g, h, i)(ax2, ay2) = (bx2, by2)
	∧ transform (a, b, c, d, e, f, g, h, i)(ax3, ay3) = (bx3, by3)

tatarize / boys.txt

Last active July 12, 2023 22:31

Gist to create random children names