Lune of Hippocrates

AbbreviationCoordinate plane for Hippocrates' lunes#✓fully proved

The coordinate plane is the set \(\mathbb{R} \times \mathbb{R}\) of ordered pairs \((x, y)\) of real numbers.

abbrev Plane := ℝ × ℝ

Used by 13

Used byRight-angle vertex of the lune triangle · Horizontal leg endpoint of the lune triangle · Vertical leg endpoint of the lune triangle · Closed half-disk on a diameter · Planar determinant for Hippocrates' lunes · Squared Euclidean distance in the plane · Hippocrates' theorem on lunes · Lune on the horizontal leg · Half-disk on the hypotenuse · Midpoint of two points in the plane · Right triangle with legs on the axes · Displacement vector between two points of the plane · Hippocrates lune on the vertical leg

DefinitionPlanar determinant for Hippocrates' lunes#✓fully proved

For vectors \(u = (u_1, u_2)\) and \(v = (v_1, v_2)\) of the coordinate plane, \(\det(u, v) = u_1 v_2 - u_2 v_1\), the signed area of the parallelogram spanned by \(u\) and \(v\).

def det2 (u v : Plane) : ℝ := u.1 * v.2 - u.2 * v.1

Uses 1 · Used by 1

Statement usesCoordinate plane for Hippocrates' lunes

Used byClosed half-disk on a diameter

DefinitionMidpoint of two points in the plane#✓fully proved

For points \(p = (p_1, p_2)\) and \(q = (q_1, q_2)\) of the coordinate plane, their midpoint is \(\left(\frac{p_1 + q_1}{2}, \frac{p_2 + q_2}{2}\right)\).

noncomputable def midpoint (p q : Plane) : Plane := ((p.1 + q.1) / 2, (p.2 + q.2) / 2)

Uses 1 · Used by 1

Statement usesCoordinate plane for Hippocrates' lunes

Used byClosed half-disk on a diameter

DefinitionDisplacement vector between two points of the plane#✓fully proved

For points \(p = (p_1, p_2)\) and \(q = (q_1, q_2)\) of \(\mathbb{R}^2\), the displacement vector from \(p\) to \(q\) is \((q_1 - p_1, q_2 - p_2)\).

def vec (p q : Plane) : Plane := (q.1 - p.1, q.2 - p.2)

Uses 1 · Used by 1

Statement usesCoordinate plane for Hippocrates' lunes

Used byClosed half-disk on a diameter

DefinitionSquared Euclidean distance in the plane#✓fully proved

For points \(p = (p_1, p_2)\) and \(q = (q_1, q_2)\) of the coordinate plane, the squared Euclidean distance between them is \((p_1 - q_1)^2 + (p_2 - q_2)^2\).

This uses the Euclidean distance, not the sup metric of the product \(\mathbb{R} \times \mathbb{R}\).

def euclideanDistSq (p q : Plane) : ℝ := (p.1 - q.1) ^ 2 + (p.2 - q.2) ^ 2

Uses 1 · Used by 1

Statement usesCoordinate plane for Hippocrates' lunes

Used byClosed half-disk on a diameter

DefinitionClosed half-disk on a diameter#✓fully proved

Given points \(p\) and \(q\) of the coordinate plane and a property \(S\) of real numbers, this is the set of points \(x\) such that the squared Euclidean distance from \(x\) to the midpoint of \(p\) and \(q\) is at most one quarter of the squared Euclidean distance from \(p\) to \(q\) (so \(x\) lies in the closed disk with diameter \(pq\)), and \(S\) holds of the planar determinant \(\det(q - p, x - p)\). For \(p \ne q\), taking \(S(t)\) to be \(t \ge 0\) (respectively \(t \le 0\)) selects the closed half of that disk to the left (respectively right) of the directed line from \(p\) to \(q\).

def closedHalfDisk (p q : Plane) (side : ℝ → Prop) : Set Plane :=
  {x | euclideanDistSq x (midpoint p q) ≤ euclideanDistSq p q / 4 ∧
    side (det2 (vec p q) (vec p x))}

Uses 5 · Used by 3

Statement usesCoordinate plane for Hippocrates' lunes · Planar determinant for Hippocrates' lunes · Squared Euclidean distance in the plane · Midpoint of two points in the plane · Displacement vector between two points of the plane

Used byLune on the horizontal leg · Half-disk on the hypotenuse · Hippocrates lune on the vertical leg

DefinitionRight-angle vertex of the lune triangle#✓fully proved

The point \(A = (0, 0)\), the origin of the coordinate plane; it is the right-angle vertex of the triangle in Hippocrates' theorem on lunes.

def A : Plane := (0, 0)

Uses 1 · Used by 3

Statement usesCoordinate plane for Hippocrates' lunes

Used byLune on the horizontal leg · Right triangle with legs on the axes · Hippocrates lune on the vertical leg

DefinitionHorizontal leg endpoint of the lune triangle#✓fully proved

For a real number \(a\), the point \(B = (a, 0)\) on the \(x\)-axis of the coordinate plane; it is the endpoint of the horizontal leg of the right triangle in Hippocrates' theorem on lunes.

def B (a : ℝ) : Plane := (a, 0)

Uses 1 · Used by 3

Statement usesCoordinate plane for Hippocrates' lunes

Used byLune on the horizontal leg · Half-disk on the hypotenuse · Right triangle with legs on the axes

DefinitionVertical leg endpoint of the lune triangle#✓fully proved

For a real number \(b\), the point \(C = (0, b)\) on the \(y\)-axis of the coordinate plane; it is the endpoint of the vertical leg of the right triangle in Hippocrates' theorem on lunes.

def C (b : ℝ) : Plane := (0, b)

Uses 1 · Used by 3

Statement usesCoordinate plane for Hippocrates' lunes

Used byHalf-disk on the hypotenuse · Right triangle with legs on the axes · Hippocrates lune on the vertical leg

DefinitionHalf-disk on the hypotenuse#✓fully proved

For real numbers \(a\) and \(b\), let \(B = (a, 0)\) and \(C = (0, b)\). The half-disk on the hypotenuse is the set of points \(x = (x_1, x_2)\) of the closed disk with diameter \(BC\) satisfying \(\det(C - B, x - B) \ge 0\), that is, \(b x_1 + a x_2 \le ab\). For \(a, b > 0\) this is the half of the disk on the side of the line \(BC\) containing the right-angle vertex \((0, 0)\).

def hypotenuseSemidisk (a b : ℝ) : Set Plane :=
  closedHalfDisk (B a) (C b) (fun t => 0 ≤ t)

Uses 4 · Used by 2

Statement usesHorizontal leg endpoint of the lune triangle · Vertical leg endpoint of the lune triangle · Coordinate plane for Hippocrates' lunes · Closed half-disk on a diameter

Used byLune on the horizontal leg · Hippocrates lune on the vertical leg

DefinitionLune on the horizontal leg#✓fully proved

For real numbers \(a\) and \(b\), let \(A = (0, 0)\), \(B = (a, 0)\) and \(C = (0, b)\). The lune on the horizontal leg is the set of points \(x = (x_1, x_2)\) of the closed disk with diameter \(AB\) satisfying \(a x_2 \le 0\) that do not lie in the half-disk on the hypotenuse, the set of points of the closed disk with diameter \(BC\) satisfying \(b x_1 + a x_2 \le ab\). For \(a, b > 0\) this is the set of points of the closed lower half-disk on the leg \(AB\) that lie outside the closed disk with diameter \(BC\).

def horizontalLune (a b : ℝ) : Set Plane :=
  closedHalfDisk A (B a) (fun t => t ≤ 0) \ hypotenuseSemidisk a b

Uses 5 · Used by 1

Statement usesRight-angle vertex of the lune triangle · Horizontal leg endpoint of the lune triangle · Coordinate plane for Hippocrates' lunes · Closed half-disk on a diameter · Half-disk on the hypotenuse

Used byHippocrates' theorem on lunes

DefinitionHippocrates lune on the vertical leg#✓fully proved

For real numbers \(a\) and \(b\), the vertical lune is the set of points \((x, y) \in \mathbb{R}^2\) with \(x^2 + (y - b/2)^2 \le b^2/4\) and \(bx \le 0\) that do not satisfy both \((x - a/2)^2 + (y - b/2)^2 \le (a^2 + b^2)/4\) and \(bx + ay \le ab\).

For \(a, b > 0\) this is the closed half-disk on the segment from \((0, 0)\) to \((0, b)\), on the side away from \((a, 0)\), minus the closed half-disk on the hypotenuse from \((a, 0)\) to \((0, b)\), on the side of the origin.

def verticalLune (a b : ℝ) : Set Plane :=
  closedHalfDisk A (C b) (fun t => 0 ≤ t) \ hypotenuseSemidisk a b

Uses 5 · Used by 1

Statement usesRight-angle vertex of the lune triangle · Vertical leg endpoint of the lune triangle · Coordinate plane for Hippocrates' lunes · Closed half-disk on a diameter · Half-disk on the hypotenuse

Used byHippocrates' theorem on lunes

DefinitionRight triangle with legs on the axes#✓fully proved

For real numbers \(a\) and \(b\), the right triangle \(T(a, b)\) is the convex hull in the plane \(\mathbb{R}^2\) of the three points \((0, 0)\), \((a, 0)\) and \((0, b)\).

def rightTriangle (a b : ℝ) : Set Plane :=
  convexHull ℝ ({A, B a, C b} : Set Plane)

Uses 4 · Used by 1

Statement usesRight-angle vertex of the lune triangle · Horizontal leg endpoint of the lune triangle · Vertical leg endpoint of the lune triangle · Coordinate plane for Hippocrates' lunes

Used byHippocrates' theorem on lunes

TheoremHippocrates' theorem on lunes#●ready to prove

Let \(a, b > 0\) and consider the right triangle with vertices \(A = (0, 0)\), \(B = (a, 0)\) and \(C = (0, b)\). The Lebesgue measure of the lune on the horizontal leg plus the Lebesgue measure of the lune on the vertical leg equals the Lebesgue measure of the triangle, that is, of the convex hull of \(A\), \(B\) and \(C\).

public theorem_wanted hippocrates_lunes (a b : ℝ) (ha : 0 < a) (hb : 0 < b) :
    volume (horizontalLune a b) + volume (verticalLune a b) =
      volume (rightTriangle a b)

Sources

• Hippocrates of Chios (c. 440 BC). Knill, §166. Problem hippocrates_lunes of the lean-eval benchmark.

Uses 4

Statement usesCoordinate plane for Hippocrates' lunes · Lune on the horizontal leg · Right triangle with legs on the axes · Hippocrates lune on the vertical leg

13 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.