Definition Strategy for Angle Bisectors

Stream: Is there code for X?

[Li Jiale]

I'am working on formalizing angle bisector definitions and facing a design choice between specificity and generality.

Option 1: Focus on 2-angle bisectors

def bisectorDir (a b c : P) : V :=
  ‖c -ᵥ b‖ • (a -ᵥ b) + ‖a -ᵥ b‖ • (c -ᵥ b)

Rationale:

• 2-angle bisectors are the most commonly used in geometry
• They have many unique properties (incenter, excenter theorems, etc.)
• Direct computational approach for the most frequent use case

Option 2: General n-angle bisector definition

• More theoretically complete
• 2-angle case becomes a special instance
• Better alignment with mathematical generality principles

Question: What's the recommended approach for mathlib4? Should I prioritize the common use case or go with the more general n-angle definition?

[Kenny Lau]

do both

[Joseph Myers]

I've thought a lot about API design for angle bisectors over the past few years. There are several different definitions that would be relevant in the end, both for inner product spaces (bisectors between vectors and bisectors between oriented subspaces) and for affine spaces over those. Most of my recent PRs have been working towards setting up the link between incenter/excenter and angle bisectors (in n dimensions, not just two dimensions) based on how I think this theory ought to be set up.

I'm not sure what you mean by "n-angle bisector".

If you mean e.g. trisectors - multiplying an angle by some real number other than 1/2 - then those ought to be separate from bisectors (with API linking them, of course). For example, there is a meaningful notion of the submodule of vectors with equal angles to two given vectors (which unfortunately fails to correspond with an informal notion of bisector when the two vectors are in the same direction, when the informal bisector is the span of that vector, not the whole space), but no such trisector submodule.

If you mean bisectors in n dimensions, which is the appropriate general form for relating to incenter and excenter, then various API needs to be set up around orientations of submodules; you have, essentially, a consistent family of orientations for faces of a simplex (in two dimensions these correspond to arrows cycling round the triangle, for example) and can define a submodule (and similarly an affine subspace) bisecting the angle between two such oriented submodules (note than this is an (n-1)-dimensional submodule bisecting the angle between two (n-1)-dimensional oriented submodules, given an (n-2)-dimensional space lying in both submodules and an orthogonal 2-dimensional space with which each has 1-dimensional intersection). (Bisectors between two vectors / three points in n dimensions are also mathematically meaningful, just not what's needed for relating to incenter / excenter.)

But that's probably not the most convenient form for working with in practice in two dimensions, which is why I've been PRing things about the location of touchpoints - knowing betweenness properties relating touchpoints and vertices is on the critical path for being able to prove more concrete lemmas about equality of oriented angles involving vertices and incenter / excenter, which is more likely to be useful if you look at the details of what you actually need for formalizing concrete problems involving those points (I'm working on IMO 2024 P4). (Statements involving bisecting angles where one of the three points is a touchpoint are easy given the API I've set up so far for incenter / excenter. The information about locations of touchpoints is in order to translate that to statements involving vertices and not touchpoints.)

[Joseph Myers]

I don't think bisectorDir should be there; bisectors for vectors should be set up in terms of two vectors rather than three points, and it looks like it gets the wrong result for two vectors pointing in opposite directions. My inclination is that the core definitions for bisectors between vectors should be set up as the kernel of an appropriate linear map (so automatically a submodule), and then ones that do the right thing for vectors in the same direction built on top of that (and results in the oriented case, and bisectors between oriented submodules in n dimensions, also built on top of that).

[Eric Wieser]

Do we already have a definition for the un-oriented bisector,

noncomputable def InnerProductGeometry.bisector (v₁ v₂ : V) : Submodule ℝ V :=
  (LinearMap.eqLocus (‖v₁‖⁻¹ • innerₛₗ ℝ v₁) (‖v₂‖⁻¹ • innerₛₗ ℝ v₂)).copy
    {x | angle v₁ x = angle v₂ x}
    (sorry /- I have a proof of this somewhere -/)

/-- The affine hyperplane bisecting the angle between three points -/
noncomputable def EuclideanGeometry.bisector (p₁ p₂ p₃ : P) : AffineSubspace ℝ P :=
  (InnerProductGeometry.bisector (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)).toAffineSubspace.comap
    (AffineEquiv.vaddConst _ p₂).symm.toAffineMap

[Joseph Myers]

We don't have any of the definitions. My inclination is to treat the property about equal angles in what you have as InnerProductGeometry.bisector as a theorem rather than using copy to get defeq for that property. I also think at least four definitions are needed for bisectors between vectors as submodules, where the one you have would be something like fullIntBisector and then a definition intBisector would be derived from it that corresponds more closely to a conventional informal definition (as in: as long as the two vectors are nonzero, the intersection with any two-dimensional space containing both of them is precisely one-dimensional, so the bisector of the angle between two vectors in the same direction is the span of those two vectors, and the bisector is itself one-dimensional except for the special case of two vectors in opposite directions; equivalently, the oriented angle is bisected in any such two-dimensional subspace). And then two definitions fullExtBisector and extBisector for the external bisectors. And then corresponding affine definitions for all of those.

[Li Jiale]

Thanks for the detailed guidance! Based on your suggestions, I've drafted these core definitions:

-- Layer 1: Complete definitions (kernel-based)
noncomputable def fullIntBisector (u v : V) : Submodule ℝ V :=
  LinearMap.ker ((‖v‖) • innerₛₗ ℝ u - (‖u‖) • innerₛₗ ℝ v)

noncomputable def fullExtBisector (u v : V) : Submodule ℝ V :=
  LinearMap.ker ((‖v‖) • innerₛₗ ℝ u + (‖u‖) • innerₛₗ ℝ v)

-- Layer 2: Practical definitions (branching on same/opposite direction)
noncomputable def intBisector (u v : V) : Submodule ℝ V :=
by
  classical
  by_cases h0 : u = 0 ∨ v = 0
  · exact ⊥
  · by_cases hs : SameRay ℝ u v
    · exact Submodule.span ℝ ({u} : Set V)
    · by_cases ho : SameRay ℝ u (-v)
      · exact fullIntBisector u v
      · exact Submodule.span ℝ ({‖v‖ • u + ‖u‖ • v} : Set V)

noncomputable def extBisector (u v : V) : Submodule ℝ V :=
by
  classical
  by_cases h0 : u = 0 ∨ v = 0
  · exact ⊥
  · by_cases hs : SameRay ℝ u v
    · exact fullExtBisector u v
    · by_cases ho : SameRay ℝ u (-v)
      · exact Submodule.span ℝ ({u} : Set V)
      · exact Submodule.span ℝ ({‖v‖ • u - ‖u‖ • v} : Set V)

-- Layer 3: Affine versions
noncomputable def affineIntBisector (a b c : P) : AffineSubspace ℝ P :=
  through b (intBisector (a -ᵥ b) (c -ᵥ b))

noncomputable def affineExtBisector (a b c : P) : AffineSubspace ℝ P :=
  through b (extBisector (a -ᵥ b) (c -ᵥ b))

Does this layered approach look reasonable?

[Eric Wieser]

I claim the defeq is slightly nicer with eqLocus, but I guess it doesn't matter too much

[Joseph Myers]

I think the affine and vector versions can be distinguished by being in different namespaces rather than needing different names, but I don't know what's most convenient to use in practice.

I'd be inclined to use term-mode if to define intBisector and extBisector rather than defining data in tactic mode. Also, if the definitions are set up correctly, fullExtBisector can be defined in terms of fullIntBisector, and extBisector in terms of intBisector, by negating one of the vectors, and then this can be proved equivalent to other definitions when setting up API.

What's through? We discussed renaming AffineSubspace.mk' (see #23546), but I'm not sure that reached a conclusion.