Pick's theorem

TheoremPick's theorem for lattice triangles with a vertex at the origin#✓fully proved

Let \(u, v \in \mathbb{Z}^2\) with \(u_0 v_1 - u_1 v_0 \neq 0\), and let \(T \subset \mathbb{R}^2\) be the convex hull of \(0\), \(u\) and \(v\). Let \(I\) be the number of points of \(\mathbb{Z}^2\) in the interior of \(T\) and \(B\) the number of points of \(\mathbb{Z}^2\) on the boundary of \(T\). Then the area (two-dimensional Lebesgue measure) of \(T\) equals \(I + B/2 - 1\).

theorem _root_.MeasureTheory.toReal_volume_convexHull_lattice_triangle (u v : Fin 2 → ℤ)
    (h : u 0 * v 1 - u 1 * v 0 ≠ 0) :
    (volume (convexHull ℝ ({0, (fun i ↦ (u i : ℝ)), (fun i ↦ (v i : ℝ))} :
      Set (Fin 2 → ℝ)))).toReal =
      (Set.ncard {z : Fin 2 → ℤ | (fun i ↦ (z i : ℝ)) ∈
        interior (convexHull ℝ ({0, (fun i ↦ (u i : ℝ)), (fun i ↦ (v i : ℝ))} :
          Set (Fin 2 → ℝ)))} : ℝ) +
      (Set.ncard {z : Fin 2 → ℤ | (fun i ↦ (z i : ℝ)) ∈
        frontier (convexHull ℝ ({0, (fun i ↦ (u i : ℝ)), (fun i ↦ (v i : ℝ))} :
          Set (Fin 2 → ℝ)))} : ℝ) / 2 - 1
Used by 1
Used byPick's theorem for convex lattice polygons

TheoremPick's theorem for convex lattice polygons#✓fully proved

Let \(V \subset \mathbb{Z}^2\) be a finite set of lattice points, let \(P \subset \mathbb{R}^2\) be the convex hull of \(V\), and suppose that \(P\) has nonempty interior. Let \(I\) be the number of points of \(\mathbb{Z}^2\) in the interior of \(P\) and \(B\) the number of points of \(\mathbb{Z}^2\) on the boundary of \(P\). Then the area (two-dimensional Lebesgue measure) of \(P\) equals \(I + B/2 - 1\).

Proof: The triangle case counts lattice points in a half-open fundamental parallelogram. A crossing diagonal then cuts larger polygons into two smaller full-dimensional lattice polygons, allowing strong induction on the vertex set.

MetaMathlibExt.pick_convex_lattice_polygon · 15 lines 
theorem pick_convex_lattice_polygon (vertices : Finset (Fin 2 → ℤ))
    (hfull :
      (interior
        (convexHull ℝ ((fun z i => (z i : ℝ)) '' (vertices : Set (Fin 2 → ℤ))))).Nonempty) :
    (volume
      (convexHull ℝ ((fun z i => (z i : ℝ)) '' (vertices : Set (Fin 2 → ℤ))))).toReal =
      (Set.ncard {z : Fin 2 → ℤ |
        (fun i => (z i : ℝ)) ∈
          interior
            (convexHull ℝ ((fun z i => (z i : ℝ)) '' (vertices : Set (Fin 2 → ℤ))))} : ℝ) +
        (Set.ncard {z : Fin 2 → ℤ |
          (fun i => (z i : ℝ)) ∈
            frontier
              (convexHull ℝ
                ((fun z i => (z i : ℝ)) '' (vertices : Set (Fin 2 → ℤ))))} : ℝ) / 2 - 1
Sources
Uses 1
Proof usesPick's theorem for lattice triangles with a vertex at the origin

DefinitionLattice points in the plane#✓fully proved

The map \(\mathbb{Z}^2 \to \mathbb{R}^2\) sending a lattice point \((a, b)\) to the point \((a, b)\) of the real plane.

def toPlane (z : ℤ × ℤ) : ℝ × ℝ := ((z.1 : ℝ), (z.2 : ℝ))
Used by 3
Used byNumber of boundary lattice points · Number of interior lattice points · Lattice polygon

DefinitionLattice polygon#✓fully proved

Given integer points \(v_0, \dots, v_{n-1} \in \mathbb{Z}^2\), the lattice polygon on \(v\) is the polygon in \(\mathbb{R}^2\) with \(n\) vertices whose \(i\)-th vertex is \(v_i\), viewed as a point of \(\mathbb{R}^2\).

def latPoly {n : ℕ} (v : Fin n → ℤ × ℤ) : Polygon (ℝ × ℝ) n :=
  ⟨fun i => toPlane (v i)⟩
Uses 1 · Used by 3
Statement usesLattice points in the plane
Used byNumber of boundary lattice points · Number of interior lattice points · Pick's theorem

DefinitionRegion enclosed by a planar set#✓fully proved

For a set \(S \subseteq \mathbb{R}^2\), the region enclosed by \(S\) is the set of points \(x \notin S\) whose connected component in the complement \(\mathbb{R}^2 \setminus S\) is bounded. For a simple closed curve \(S\) this is the Jordan interior.

def inside (S : Set (ℝ × ℝ)) : Set (ℝ × ℝ) :=
  {x | x ∉ S ∧ Bornology.IsBounded (connectedComponentIn Sᶜ x)}
Used by 2
Used byEnclosed area · Number of interior lattice points

DefinitionEnclosed area#✓fully proved

The area enclosed by a set \(S \subseteq \mathbb{R}^2\) is the Lebesgue measure, as a real number, of the region enclosed by \(S\) (the points \(x \notin S\) whose connected component in \(\mathbb{R}^2 \setminus S\) is bounded); it is taken to be \(0\) when that measure is infinite.

noncomputable def area (S : Set (ℝ × ℝ)) : ℝ := (volume (inside S)).toReal
Uses 1 · Used by 1
Statement usesRegion enclosed by a planar set
Used byPick's theorem

DefinitionCyclically adjacent indices#✓fully proved

Two indices \(i, j \in \{0, \dots, n-1\}\) are adjacent when \(j \equiv i + 1 \pmod n\) or \(i \equiv j + 1 \pmod n\).

def Adjacent {n : ℕ} (i j : Fin n) : Prop :=
  finRotate n i = j ∨ finRotate n j = i
Used by 1
Used bySimple polygon

DefinitionSimple polygon#✓fully proved

A polygon in \(\mathbb{R}^2\) with vertices \(p_0, \dots, p_{n-1}\) (indices taken mod \(n\)) and edges the segments \(e_i = [p_i, p_{i+1}]\) is simple when consecutive vertices are distinct (\(p_i \ne p_{i+1}\) for all \(i\)), any two edges \(e_i\) and \(e_j\) with \(i \ne j\), \(j \not\equiv i + 1\) and \(i \not\equiv j + 1 \pmod n\) are disjoint, and every two consecutive edges meet only in their common vertex: \(e_i \cap e_{i+1} = \{p_{i+1}\}\) for all \(i\).

def IsSimple {n : ℕ} (poly : Polygon (ℝ × ℝ) n) : Prop :=
  poly.HasNondegenerateEdges ∧
  (∀ i j : Fin n, i ≠ j → ¬ Adjacent i j →
      Disjoint (poly.edgeSet ℝ i) (poly.edgeSet ℝ j)) ∧
  (∀ i : Fin n, poly.edgeSet ℝ i ∩ poly.edgeSet ℝ (finRotate n i)
      = {poly (finRotate n i)})
Uses 1 · Used by 1
Statement usesCyclically adjacent indices
Used byPick's theorem

DefinitionNumber of boundary lattice points#✓fully proved

For integer points \(v_0, \dots, v_{n-1} \in \mathbb{Z}^2\), the number of lattice points \(z \in \mathbb{Z}^2\) that lie on the boundary (the union of the edges) of the lattice polygon on \(v\).

noncomputable def boundaryPts {n : ℕ} (v : Fin n → ℤ × ℤ) : ℕ :=
  Nat.card {z : ℤ × ℤ | toPlane z ∈ (latPoly v).boundary (R := ℝ)}
Uses 2 · Used by 1
Statement usesLattice polygon · Lattice points in the plane
Used byPick's theorem

DefinitionNumber of interior lattice points#✓fully proved

For integer points \(v_0, \dots, v_{n-1} \in \mathbb{Z}^2\), the number of lattice points \(z \in \mathbb{Z}^2\) that lie in the region enclosed by the boundary of the lattice polygon on \(v\), that is, the points off the boundary whose connected component in its complement is bounded.

noncomputable def interiorPts {n : ℕ} (v : Fin n → ℤ × ℤ) : ℕ :=
  Nat.card {z : ℤ × ℤ | toPlane z ∈ inside ((latPoly v).boundary (R := ℝ))}
Uses 3 · Used by 1
Statement usesRegion enclosed by a planar set · Lattice polygon · Lattice points in the plane
Used byPick's theorem

TheoremPick's theorem#●ready to prove

Let \(n \ge 3\) and let \(v_0, \dots, v_{n-1} \in \mathbb{Z}^2\) be integer points such that the lattice polygon \(P\) in \(\mathbb{R}^2\) with vertices \(v_0, \dots, v_{n-1}\) is simple. Then the area of the region enclosed by the boundary of \(P\) equals \(I + B/2 - 1\), where \(I\) is the number of lattice points in that region and \(B\) is the number of lattice points on the boundary of \(P\).

public theorem_wanted pick {n : ℕ} (hn : 3 ≤ n) (v : Fin n → ℤ × ℤ)
    (hsimple : IsSimple (latPoly v)) :
    area ((latPoly v).boundary (R := ℝ))
      = (interiorPts v : ℝ) + (boundaryPts v : ℝ) / 2 - 1
Sources
  • G. Pick, Geometrisches zur Zahlenlehre (1899). Knill, Some fundamental theorems in mathematics, §154. Problem pick of the lean-eval benchmark.
Uses 5
Statement usesSimple polygon · Enclosed area · Number of boundary lattice points · Number of interior lattice points · Lattice polygon
10 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.