Inscribed rectangle problem

DefinitionAxis-aligned rectangle#✓fully proved

For points \(a = (a_1, a_2)\) and \(b = (b_1, b_2)\) of \(\mathbb{R}^2\), the axis-aligned (possibly degenerate) rectangle with opposite corners \(a\) and \(b\) is the list of its four vertices \((a_1, a_2)\), \((b_1, a_2)\), \((b_1, b_2)\), \((a_1, b_2)\), in this order.

noncomputable def axisAlignedRectangleCorners (a b : ℝ × ℝ) : Fin 4 → ℝ × ℝ :=
  ![(a.1, a.2), (b.1, a.2), (b.1, b.2), (a.1, b.2)]

Used by 1

Used byRotated rectangle

DefinitionRotated rectangle#✓fully proved

For points \(a, b \in \mathbb{R}^2\) and an angle \(\theta \in \mathbb{R}\), the rotated rectangle given by \(a\), \(b\) and \(\theta\) is the list of four points obtained by applying the rotation \((x, y) \mapsto (x \cos\theta + y \sin\theta, -x \sin\theta + y \cos\theta)\) about the origin to each vertex, in order, of the axis-aligned rectangle with opposite corners \(a\) and \(b\).

noncomputable def rectangleCorners (a b : ℝ × ℝ) (θ : ℝ) : Fin 4 → ℝ × ℝ :=
  ContinuousLinearMap.rotation θ ∘ axisAlignedRectangleCorners a b

Uses 1 · Used by 1

Statement usesAxis-aligned rectangle

Used byInscribed rectangle

DefinitionInscribed rectangle#✓fully proved

Let \(\gamma\) be a map from the unit circle to \(\mathbb{R}^2\). For points \(a, b \in \mathbb{R}^2\) and an angle \(\theta \in \mathbb{R}\), the rotated rectangle given by \(a\), \(b\) and \(\theta\) is inscribed in \(\gamma\) when its four vertices are pairwise distinct and each lies in the image of \(\gamma\).

The map \(\gamma\) need not be smooth, or even a Jordan curve, for this definition.

def IsInscribedRectangle (a b : ℝ × ℝ) (θ : ℝ) (γ : Circle → ℝ × ℝ) : Prop :=
  Function.Injective (rectangleCorners a b θ) ∧ ∀ i : Fin 4, rectangleCorners a b θ i ∈ Set.range γ

Uses 1 · Used by 1

Statement usesRotated rectangle

Used byAspect-ratio parameters of inscribed rectangles

DefinitionAspect ratio#✓fully proved

For points \(a = (a_1, a_2)\) and \(b = (b_1, b_2)\) of \(\mathbb{R}^2\), the aspect ratio of the axis-aligned rectangle with opposite corners \(a\) and \(b\) is \(|a_1 - b_1| / |a_2 - b_2|\), the ratio of its horizontal side length to its vertical side length; it is \(0\) when \(a_2 = b_2\).

noncomputable def aspectRatio (a b : ℝ × ℝ) : ℝ :=
  |a.1 - b.1| / |a.2 - b.2|

Used by 1

Used byAspect-ratio parameters of inscribed rectangles

DefinitionAspect-ratio parameters of inscribed rectangles#✓fully proved

For a map \(\gamma\) from the unit circle to \(\mathbb{R}^2\), let \(X(\gamma)\) be the set of all \(r \in [0, 1]\) for which there are points \(a, b \in \mathbb{R}^2\) and an angle \(\theta \in \mathbb{R}\) such that the rotated rectangle given by \(a\), \(b\) and \(\theta\) is inscribed in \(\gamma\) and the axis-aligned rectangle with opposite corners \(a\) and \(b\) has aspect ratio \(\tan(r\pi/4)\).

noncomputable def X (γ : Circle → ℝ × ℝ) : Set ℝ :=
  {r : ℝ | r ∈ Set.Icc 0 1 ∧ ∃ a b : ℝ × ℝ, ∃ θ : ℝ,
    aspectRatio a b = tan (r * π / 4) ∧ IsInscribedRectangle a b θ γ}

Uses 2 · Used by 1

Statement usesInscribed rectangle · Aspect ratio

Used byHugelmeyer's theorem on aspect ratios of inscribed rectangles

TheoremHugelmeyer's theorem on aspect ratios of inscribed rectangles#●ready to prove

Let \(\gamma\) be a smooth Jordan curve, that is, a map from the unit circle to \(\mathbb{R}^2\) that is a \(C^\infty\) immersion and a topological embedding, and let \(X\) be the set of all \(r \in [0, 1]\) such that some rectangle inscribed in \(\gamma\) has aspect ratio \(\tan(r\pi/4)\). Then the Lebesgue measure of \(X\) is at least \(1/3\).

public theorem_wanted theorem_1 (γ : Circle → ℝ × ℝ) (hγ : IsSmoothEmbedding (𝓡 1) 𝓘(ℝ, ℝ × ℝ) ∞ γ) :
    volume (X γ) ≥ 1/3

Sources

• C. Hugelmeyer, Inscribed rectangles in a smooth Jordan curve attain at least one third of all aspect ratios, Annals of Math, 194 (2) 2021. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_inscribed_rectangles of the lean-eval benchmark.

Uses 1

Statement usesAspect-ratio parameters of inscribed rectangles

DefinitionRotated rectangle with given opposite corners#✓fully proved

For \(z, w \in \mathbb{C}\) and an angle \(\theta\), \(R(z, w, \theta)\) is the list of four points \(z e^{i\theta}\), \((\operatorname{Re} w + i \operatorname{Im} z) e^{i\theta}\), \(w e^{i\theta}\), \((\operatorname{Re} z + i \operatorname{Im} w) e^{i\theta}\): the vertices, in order, of the axis-parallel rectangle with opposite corners \(z\) and \(w\), rotated about the origin by \(\theta\). The rectangle is degenerate when \(z\) and \(w\) have the same real part or the same imaginary part.

noncomputable def R (z w : ℂ) (θ : Angle) : Fin 4 → ℂ :=
  ![z * θ.toCircle, (w.re + z.im * I) * θ.toCircle, w * θ.toCircle, (z.re + w.im * I) * θ.toCircle]

Used by 1

Used byRectangular peg theorem (Greene–Lobb)

TheoremRectangular peg theorem (Greene–Lobb)#●ready to prove

Let \(\gamma : S^1 \to \mathbb{C}\) be a \(C^\infty\) embedding of the unit circle (a smooth Jordan curve in the plane). For \(z, w \in \mathbb{C}\) and an angle \(\theta\), write \(R(z, w, \theta)\) for the list of the four points \(z e^{i\theta}\), \((\operatorname{Re} w + i \operatorname{Im} z) e^{i\theta}\), \(w e^{i\theta}\), \((\operatorname{Re} z + i \operatorname{Im} w) e^{i\theta}\), in this order: the vertices of the (possibly degenerate) axis-parallel rectangle with opposite corners \(z\) and \(w\), rotated about the origin by \(\theta\). Then for all \(z\), \(w\), \(\theta\) there exist \(z'\), \(w'\), \(\theta'\) such that \(R(z, w, \theta)\) is similar to \(R(z', w', \theta')\), meaning that for some real \(r > 0\) the distance between the \(i\)-th and \(j\)-th vertices of \(R(z, w, \theta)\) is \(r\) times the distance between the \(i\)-th and \(j\)-th vertices of \(R(z', w', \theta')\) for all \(i, j\), and all four vertices of \(R(z', w', \theta')\) lie on \(\gamma\).

public theorem_wanted theorem_1 (γ : Circle → ℂ) (z w : ℂ) (θ : Real.Angle)
    (hγ : IsSmoothEmbedding (𝓡 1) 𝓘(ℝ, ℂ) ∞ γ) :
    ∃ (θ' : Real.Angle), ∃ (z' w' : ℂ), Similar (R z w θ) (R z' w' θ') ∧
    ∀ i : Fin 4, R z' w' θ' i ∈ Set.range γ

Sources

• J. E. Greene and A. Lobb, The rectangular peg problem, Annals of Math, 194 (2) 2021. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_rectangular_peg_problem of the lean-eval benchmark.

Uses 1

Statement usesRotated rectangle with given opposite corners

6 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.