Equichordal point problem

AbbreviationEuclidean plane for the equichordal point problem#✓fully proved

The Euclidean plane is the space \(\mathbb{R}^2\) of pairs of real numbers with the Euclidean inner product and norm.

abbrev Plane := EuclideanSpace ℝ (Fin 2)

Used by 2

Used byEquichordal point theorem · Equichordal point

DefinitionEquichordal point#✓fully proved

Let \(K\) be a subset of the Euclidean plane. A point \(P\) is an equichordal point of \(K\) if \(P\) lies in the interior of \(K\) and there is a real \(L > 0\) such that for every unit vector \(u\) there are reals \(a > 0\) and \(b > 0\) for which \(P + a u\) and \(P - b u\) lie in the boundary (frontier) of \(K\), the open segment between \(P - b u\) and \(P + a u\) lies in the interior of \(K\), and the distance between \(P + a u\) and \(P - b u\) equals \(L\).

The open segment condition makes \(P + a u\) and \(P - b u\) the endpoints of the chord through \(P\) in direction \(u\), ruling out other boundary crossings for nonconvex star-shaped domains.

def IsEquichordalPoint (K : Set Plane) (P : Plane) : Prop :=
  P ∈ interior K ∧
    ∃ L : ℝ, 0 < L ∧
      ∀ u : Plane, u ∈ sphere (0 : Plane) 1 →
        ∃ a b : ℝ,
          0 < a ∧ 0 < b ∧
            P + a • u ∈ frontier K ∧
              P - b • u ∈ frontier K ∧
                openSegment ℝ (P - b • u) (P + a • u) ⊆ interior K ∧
                  dist (P + a • u) (P - b • u) = L

Uses 1 · Used by 1

Statement usesEuclidean plane for the equichordal point problem

Used byEquichordal point theorem

TheoremEquichordal point theorem#●ready to prove

Let \(K\) be a compact convex subset of the Euclidean plane with nonempty interior. Then \(K\) does not have two distinct equichordal points: there are no points \(P \ne Q\) of the plane such that both \(P\) and \(Q\) are equichordal points of \(K\).

public theorem_wanted equichordal_point_unique {K : Set Plane}
    (hK : IsCompact K) (hconv : Convex ℝ K) (hne : (interior K).Nonempty) :
    ¬ ∃ P Q : Plane,
      P ≠ Q ∧ IsEquichordalPoint K P ∧ IsEquichordalPoint K Q

Sources

• M. R. Rychlik, A complete solution to the equichordal point problem of Fujiwara, Blaschke, Rothe and Weizenböck, Invent. Math. 129 (1997). Listed as §205 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Knill, §205. Problem equichordal_point_unique of the lean-eval benchmark.

Uses 2

Statement usesEquichordal point · Euclidean plane for the equichordal point problem

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.