Circles and conics

Configurations of circles and conics, tangency, chains of circles, lunes, and mathematical billiards in elliptic and polygonal tables.

• Casey's theorem
• Lune of Hippocrates
• Mathematical billiards
• Monge's theorem
• Pascal's and Pappus's hexagon theorems

TheoremDescartes' circle theorem#✓fully proved

Let four circles in the Euclidean plane have centers \(c_i\) and radii \(r_i > 0\) for \(i = 1, 2, 3, 4\), let \(d\) be the Euclidean distance, and let \(k_1, k_2, k_3, k_4\) be real numbers. Suppose that either (a) any two of the circles are externally tangent, \(d(c_i, c_j) = r_i + r_j\) for \(i \ne j\), and \(k_i = 1/r_i\) for every \(i\); or (b) for some index \(e\), each other circle is internally tangent to circle \(e\), that is, \(d(c_e, c_j) = r_e - r_j\) for \(j \ne e\); any two circles other than circle \(e\) are externally tangent, \(d(c_i, c_j) = r_i + r_j\) for distinct \(i, j \ne e\); and \(k_e = -1/r_e\) and \(k_j = 1/r_j\) for \(j \ne e\). Then \((k_1 + k_2 + k_3 + k_4)^2 = 2(k_1^2 + k_2^2 + k_3^2 + k_4^2)\).

Proof: Following the Cayley-Menger/Gram-determinant argument in Lagarias, Mallows, and Wilks, Beyond the Descartes circle theorem, Section 3, and Wikipedia's proof sketch, introduce signed radii, expand the planar Gram determinant in coordinates, and clear denominators.

theorem descartes_circle_theorem (c : Fin 4 → EuclideanSpace ℝ (Fin 2))
    (r k : Fin 4 → ℝ) :
    (∀ i, 0 < r i) →
    (((∀ i j, i ≠ j → dist (c i) (c j) = r i + r j) ∧ ∀ i, k i = 1 / r i) ∨
      ∃ e : Fin 4, k e = -1 / r e ∧ (∀ j, j ≠ e → k j = 1 / r j) ∧
        (∀ j, j ≠ e → dist (c e) (c j) = r e - r j) ∧
        ∀ i j, i ≠ e → j ≠ e → i ≠ j → dist (c i) (c j) = r i + r j) →
    (∑ i : Fin 4, k i) ^ 2 = 2 * ∑ i : Fin 4, k i ^ 2

Sources

• https://en.wikipedia.org/wiki/Descartes%27_theorem.

DefinitionLens curvature recurrence#✓fully proved

For real numbers \(K\) and \(A\), a real sequence \((b_n)_{n \ge 0}\) satisfies the lens curvature recurrence with parameters \(K\) and \(A\) when \(1 + K \neq 0\) and, for every \(n \ge 0\),

\[b_{n+2} = \frac{6 - 2K}{1 + K}\, b_{n+1} - b_n + \frac{-8A}{1 + K}.\]

This is the second-order nonhomogeneous recurrence of the source for the curvatures of a chain of circles in a symmetric lens, where \(A\) is the common curvature of the two lens circles.

public def IsLensCurvatureRecurrence (b : ℕ → ℝ) (K A : ℝ) : Prop :=
  1 + K ≠ 0 ∧ ∀ n,
    b (n + 2) = ((6 - 2 * K) / (1 + K)) * b (n + 1) - b n + (-8 * A) / (1 + K)

TheoremMiquel's theorem#✓fully proved

Let \(A\), \(B\), \(C\) be non-collinear points of the Euclidean plane \(\mathbb{R}^2\), and let \(D\), \(E\), \(F\) be points on the lines \(BC\), \(CA\), \(AB\) respectively with \(D \ne B\), \(D \ne C\), \(E \ne C\), \(E \ne A\), \(F \ne A\) and \(F \ne B\). If \(A\), \(E\), \(F\) lie on the circle with center \(O_1\) and radius \(r_1\), \(B\), \(F\), \(D\) lie on the circle with center \(O_2\) and radius \(r_2\), and \(C\), \(D\), \(E\) lie on the circle with center \(O_3\) and radius \(r_3\), then these three circles have a common point.

theorem miquel_theorem (A B C D E F : EuclideanSpace ℝ (Fin 2))
    (hTri : ¬ Collinear ℝ ({A, B, C} : Set (EuclideanSpace ℝ (Fin 2))))
    (hD : D ∈ affineSpan ℝ ({B, C} : Set (EuclideanSpace ℝ (Fin 2))))
    (hE : E ∈ affineSpan ℝ ({C, A} : Set (EuclideanSpace ℝ (Fin 2))))
    (hF : F ∈ affineSpan ℝ ({A, B} : Set (EuclideanSpace ℝ (Fin 2))))
    (hDB : D ≠ B) (hDC : D ≠ C)
    (hEC : E ≠ C) (hEA : E ≠ A)
    (hFA : F ≠ A) (hFB : F ≠ B)
    (O1 O2 O3 : EuclideanSpace ℝ (Fin 2)) (r1 r2 r3 : ℝ)
    (hAEF : A ∈ Metric.sphere O1 r1 ∧ E ∈ Metric.sphere O1 r1 ∧ F ∈ Metric.sphere O1 r1)
    (hBFD : B ∈ Metric.sphere O2 r2 ∧ F ∈ Metric.sphere O2 r2 ∧ D ∈ Metric.sphere O2 r2)
    (hCDE : C ∈ Metric.sphere O3 r3 ∧ D ∈ Metric.sphere O3 r3 ∧ E ∈ Metric.sphere O3 r3) :
    ∃ M, M ∈ Metric.sphere O1 r1 ∧ M ∈ Metric.sphere O2 r2 ∧ M ∈ Metric.sphere O3 r3

Sources

• https://en.wikipedia.org/wiki/Miquel%27s_theorem.

TheoremPizza theorem#✓fully proved

Let \(n \ge 2\) be a natural number, let \(D\) be the open disk of radius \(R > 0\) centered at a point \(c\) of \(\mathbb{R}^2\), let \(p\) be a point of \(D\), and let \(\theta_0\) be a real number. Put \(\alpha = \pi / (2n)\) and, for \(k = 0, 1, \dots, 4n - 1\), let \(S_k\) be the set of points of \(D\) of the form \(p + r(\cos\theta, \sin\theta)\) with \(r \ge 0\) and \(\theta_0 + k\alpha \le \theta < \theta_0 + (k + 1)\alpha\). Then the sum of the Lebesgue measures of the \(S_k\) with \(k\) even equals the sum of the Lebesgue measures of the \(S_k\) with \(k\) odd.

The \(4n\) sectors \(S_k\) are the slices cut from the disk by \(2n\) lines through \(p\) at equal angles, so alternately shading the slices gives equal shaded and unshaded areas.

MetaMathlibExt.pizza_theorem · 15 lines

theorem pizza_theorem (n : ℕ) (hn : 2 ≤ n)
    (c p : ℝ × ℝ) (R : ℝ) (hR : 0 < R)
    (hp : p ∈ {x : ℝ × ℝ | (x.1 - c.1) ^ 2 + (x.2 - c.2) ^ 2 < R ^ 2}) (θ₀ : ℝ) :
    ∑ k ∈ Finset.filter (fun k => k % 2 = 0) (Finset.range (4 * n)),
      MeasureTheory.volume ({x : ℝ × ℝ | (x.1 - c.1) ^ 2 + (x.2 - c.2) ^ 2 < R ^ 2} ∩
        {x | ∃ r θ : ℝ, 0 ≤ r ∧
          θ₀ + (k : ℝ) * (Real.pi / (2 * (n : ℝ))) ≤ θ ∧
          θ < θ₀ + ((k : ℝ) + 1) * (Real.pi / (2 * (n : ℝ))) ∧
          x = p + r • (Real.cos θ, Real.sin θ)}) =
    ∑ k ∈ Finset.filter (fun k => k % 2 = 1) (Finset.range (4 * n)),
      MeasureTheory.volume ({x : ℝ × ℝ | (x.1 - c.1) ^ 2 + (x.2 - c.2) ^ 2 < R ^ 2} ∩
        {x | ∃ r θ : ℝ, 0 ≤ r ∧
          θ₀ + (k : ℝ) * (Real.pi / (2 * (n : ℝ))) ≤ θ ∧
          θ < θ₀ + ((k : ℝ) + 1) * (Real.pi / (2 * (n : ℝ))) ∧
          x = p + r • (Real.cos θ, Real.sin θ)})

Sources

• Pizza theorem, Wikipedia, https://en.wikipedia.org/wiki/Pizza_theorem.

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.