Trying to work with tangents to a circumsphere

Stream: new members

[Riley Riles]

Hi! I'd like to prove the alternate segment theorem, which does not appear to currently have a proof in Lean4. Does this formalization seem reasonable? Are there any better tools I should be using? (Currently just browsing Mathlib.Geometry.Euclidean.)

theorem AlternateSegments (A B C K I : Pt) (triangleABC : Triangle ℝ Pt) (H: AffineIndependent ℝ ![A, B, C]): triangleABC = ⟨_, H⟩ → K = triangleABC.circumcenter → ∠ K B I = Real.pi/2 ∧ ∠ K B I = ∠ K B C + ∠ C B I → ∠ B A C = ∠ C B I

[Matt Diamond]

Just a tip: instead of using one backtick, wrap your code with 3 backticks (```), like so:

\```
[code]
\```

but without the backslashes. Also make sure to include any imports. Check out #mwe for more info.

[Riley Riles]

Thanks, let me rewrite that:

import Mathlib.Geometry.Euclidean.Angle.Sphere

open Affine Affine.Simplex EuclideanGeometry FiniteDimensional Module

open scoped Affine EuclideanGeometry Real

variable (V : Type*) (Pt : Type*)

variable [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt]

variable [NormedAddTorsor V Pt]

theorem AlternateSegments (A B C K I : Pt) (triangleABC : Triangle ℝ Pt) (H: AffineIndependent ℝ ![A, B, C]): triangleABC = ⟨_, H⟩ → K = triangleABC.circumcenter → ∠ K B I = Real.pi/2 ∧ ∠ K B I = ∠ K B C + ∠ C B I → ∠ B A C = ∠ C B I

[Matt Diamond]

Make sure that the last 3 ticks are on their own line (and feel free to edit your post instead of making a new one). But that looks much better, thanks!

[Riley Riles]

Gotcha! Thanks for explaining, I'm still new here.

[Joseph Myers]

I have six open PRs adding more geometrical definitions to mathlib (focused at present more on definitions than on theorems); #22483 is the one defining tangents (but not doing anything connecting them to angles).

[Joseph Myers]

The idiomatic way of distinguishing the alternate segment from the one opposite it is to use SOppSide (to say two points are on opposite sides of a chord).

[Joseph Myers]

I expect the result to be easier to prove with oriented angles mod π. Note that we only have angles in the same segment for oriented angles mod π; we don't yet have anything deducing it for angles mod 2π (when you go mod 2π, you start needing to distinguish "angles in same segment" and "opposite angles of a cyclic quadrilateral" as different theorems; mod π, they are the same theorem).

[Joseph Myers]

Working mod π, you also don't need any SOppSide condition in the statement.

[Joseph Myers]

Once you have the result for oriented angles mod 2π, there should be enough existing API for converting between oriented and unoriented angles, and for proving that two angles have the same sign, to enable going to the corresponding result for unoriented angles.

[Joseph Myers]

My inclination would also be to use a sphere containing the three different points that's passed as its own hypothesis rather than directly using circumsphere, since while the spheres will be equal, a general sphere may be more convenient for users.

[Joseph Myers]

When going from oriented to unoriented angles for such a result, there's the additional complication that the oriented angle result is inherently two-dimensional but the unoriented angle result should work in an ambient space of more than two dimensions (given a condition that the centre of the sphere is coplanar with all the other points involved, probably). In principle this can be done by moving between an affine subspace and the full space (using lemmas that isometries preserve various geometrical quantities), but you might find places where we don't have all the lemmas needed about things being preserved by isometries.

[Riley Riles]

Thanks, that helps a lot!