adding angles

Stream: Is there code for X?

[Kevin Buzzard]

I'm idly trying to prove angle at centre is twice angle at circumference and I realise that I can't prove angle AOB plus angle BOC = angle AOC with undirected angles, indeed I am having real trouble adding hypotheses which make this statement true. Do I have to make a new definition before I can correctly state this theorem? I want to say something like "any line though O which has A and B on the same side of it, also has C on that same side".

[Mario Carneiro]

what's the theorem statement?

[Kevin Buzzard]

An example of an informal statement is that B is in triangle OAC then AOB+BOC=AOC, which we could probably say right now. But more generally B could be in the "infinite triangle" with vertex O and sides extending OA and OC and I don't know how to say this in lean right now -- the question is if we have this definition

[Mario Carneiro]

I'm asking mostly what actual imports are you working with. Is this a theorem about R^2? Inner product spaces? Hilbert axioms for geometry?

[Kevin Buzzard]

import geometry.euclidean.triangle

universes u v

variables {V : Type u} {𝔼 : Type v} [inner_product_space ℝ V] [metric_space 𝔼]
  [normed_add_torsor V 𝔼] {n : ℕ}

include V

open_locale euclidean_geometry
open_locale real
open finite_dimensional

theorem angles_add (O : 𝔼) (A B C : 𝔼) (h2 : finrank ℝ V = 2) :
  ∠ A O B + ∠ B O C = ∠ A O C :=
begin
  sorry
end

Can't be proved but under some hypotheses which I can't yet express in Lean without making new definitions, it's true

[Kevin Buzzard]

We don't have convex hull for affine spaces :-(

[Mario Carneiro]

One way to describe that infinite triangle is as the sum of the rays OA and OC

[Kevin Buzzard]

there's no sum in an affine space

[Mario Carneiro]

well, sum of the relative vectors with O as base point

[Mario Carneiro]

oh my goodness, docs#norm_sub_sq_eq_norm_sq_add_norm_sq_sub_two_mul_norm_mul_norm_mul_cos_angle

[Mario Carneiro]

which is clearly the law of cosines

[Kevin Buzzard]

you mean docs#inner_product_geometry.norm_sub_sq_eq_norm_sq_add_norm_sq_sub_two_mul_norm_mul_norm_mul_cos_angle

[Kevin Buzzard]

Not as long as docs#eventually_closure_subset_of_is_compact_absorbing_of_is_open_of_omega_limit_subset' according to someone on the discord

[Mario Carneiro]

it's not even possible to #print that without going over the line length limit

[Bhavik Mehta]

Kevin Buzzard said:

Not as long as docs#eventually_closure_subset_of_is_compact_absorbing_of_is_open_of_omega_limit_subset' according to someone on the discord

@Deniz Aydin for the sake of credit!

[Kevin Buzzard]

I think this is true

theorem angle_at_center_equals_twice_angle_at_circumference (O : 𝔼) (A B C : 𝔼)
  (r : ℝ) (hOA : dist O A = r) (hOB : dist O B = r) (hOC : dist O C = r)
  (h : ∠ A B C < π / 2) :
  ∠ A O C = 2 * ∠ A B C :=

but I can't write down the proof because there are two cases depending on whether BAC is < 90 or > 90.

[Kevin Buzzard]

begin
  have hAB : A ≠ B,
    rintro rfl,
    have h := angle_eq_left A C,
    linarith,
  have hAO : A ≠ O,
    rintro rfl,
    rw dist_self at hOA,
    subst hOA,
    apply hAB,
    exact zero_eq_dist.mp (eq.symm hOB),
  have h1 : 0 < r,
  { rw ← hOA,
    exact dist_pos.2 hAO.symm },
  have h2 : ∠ O A B = ∠ O B A,
    apply angle_eq_angle_of_dist_eq,
    rw [hOA, hOB],
  have h3 : ∠ O B C = ∠ O C B,
    apply angle_eq_angle_of_dist_eq,
  rw [hOB, hOC],
  have h4 : ∠ A B C = ∠ A O B + ∠ B O C,
    -- this is not in general true
    sorry,
  sorry
end

[Mario Carneiro]

(That needs open euclidean_geometry)

[Mario Carneiro]

I think the theorem is false, you haven't said that O,A,B,C are coplanar

[Mario Carneiro]

and in particular reasoning about that comes up when you want to add angles

[Mario Carneiro]

also do you want h4 to say have h4 : ∠ A O C = ∠ A O B + ∠ B O C,?

[Kevin Buzzard]

import geometry.euclidean.triangle

universes u v

variables {V : Type u} {𝔼 : Type v} [inner_product_space ℝ V] [metric_space 𝔼]
  [normed_add_torsor V 𝔼] {n : ℕ}

include V

open_locale euclidean_geometry
open_locale real
open finite_dimensional
open euclidean_geometry

/-
              B
                  A'
              O
          A
                  C

hypothesis `h : ABC<pi/2` means `AOC<pi`.
-/
theorem angle_at_center_equals_twice_angle_at_circumference (h2 : finrank ℝ V = 2)
  (O A B C : 𝔼) (r : ℝ) (hOA : dist O A = r) (hOB : dist O B = r) (hOC : dist O C = r)
  (h : ∠ A B C < π / 2) :
  ∠ A O C = 2 * ∠ A B C :=
begin
  have hAB : A ≠ B,
    rintro rfl,
    have h := angle_eq_left A C,
    linarith,
  have hAO : A ≠ O,
    rintro rfl,
    rw dist_self at hOA,
    subst hOA,
    apply hAB,
    exact zero_eq_dist.mp (eq.symm hOB),
  have h1 : 0 < r,
  { rw ← hOA,
    exact dist_pos.2 hAO.symm },
  have h2 : ∠ O A B = ∠ O B A,
    apply angle_eq_angle_of_dist_eq,
    rw [hOA, hOB],
  have h3 : ∠ O B C = ∠ O C B,
    apply angle_eq_angle_of_dist_eq,
  rw [hOB, hOC],
  have h4 : ∠ A B C = ∠ A O B + ∠ B O C,
    -- this is not in general true
    sorry,
  sorry
end

[Kevin Buzzard]

In the case when it's true, this is part of the proof. The other possibility is that it's the difference of these two angles.

[Mario Carneiro]

Is the finrank assumption used elsewhere as a way to say that V is 2 dimensional?

[Kevin Buzzard]

I'm interested in theorems you can't prove without making more definitions. You can state FLT in NNG but you have to define modular forms to prove it. After defining nat, succ_inj and zero_ne_succ are theorems which seem to be only provable after making more definitions (i.e. using the recursor and eliminating into type, rather than induction). Here also I can't write down my proof without making some more definitions.

[Kevin Buzzard]

I have no idea whether the finrank hypothesis is the way to go. It makes the theorem true but there might be other ways to do it (e.g. you can demand that there exist three affine independent points but not four).

[Mario Carneiro]

either way, there needs to be some set of theorems that follow from the dimensionality assumption, which are likely to be crucial in the proof

[Eric Wieser]

The finrank hypothesis doesn't look ideal to me, as it would make it awkward to talk about angles within a plane in 3D space

[Mario Carneiro]

the only thing that I found which looks helpful is docs#euclidean_geometry.eq_of_dist_eq_of_dist_eq_of_finrank_eq_two

[Mario Carneiro]

but I think you want a theorem more along the lines of your adding angles lemma

[Eric Wieser]

docs#euclidean_geometry.eq_of_dist_eq_of_dist_eq_of_mem_of_finrank_eq_two is the subspace lemma

[Eric Wieser]

Which uses finrank ℝ s.direction = 2 instead of finrank ℝ V = 2

[Mario Carneiro]

A simpler version of angles_add which doesn't need new definitions is

theorem angles_add (O : 𝔼) (A B C : 𝔼) (h2 : finrank ℝ V = 2) :
  ∠ A O B + ∠ B O C = ∠ A O C ∨ ∠ A O B + ∠ B O C = ∠ A O C + π

[Eric Wieser]

Maybe the fact that the lemma Mario links to is proved via that one suggests that working in a 2D subspace is easier than working in an ambient 2D space?

[Mario Carneiro]

I agree that asking for the whole space to be 2d is a bit overspecific. It might be possible to lift theorems about 2d space to 2d subspaces though using metric embedding

[Kevin Buzzard]

That version of angles_add isn't true because they might subtract

[Anatole Dedecker]

I have a feeling that the right way to prove that is to go through oriented angles, but I think we don't have these

[Heather Macbeth]

Indeed, we don't have oriented anything. But now that we have determinants of endomorphisms (thanks @Anne Baanen!), it might be time to start building it.

[Eric Wieser]

Am I right in thinking for that we need oriented 2d affine spaces which generalizes to needing oriented submodules to put in affine_subspace.direction (aka the exterior powers)? Or are there better representations?

[Heather Macbeth]

@Eric Wieser The path you describe is the ideal one, but I think that in the short term, you can use docs#multilinear_map docs#alternating_map for a definition of orientation.

[Heather Macbeth]

The space of topdimensional alternating maps from a real vector space is 1-dimensional, and under the natural $\mathbb{R}^+$ action it has two equivalence classes.

[Heather Macbeth]

Define an orientation to be a choice of equivalence class.

[Eric Wieser]

Is docs#alternating_map a closer approximation, since that's equivalent to linear maps from the exterior powers?

[Heather Macbeth]

Yes thanks, fixed! (that's what I meant to say)

[Heather Macbeth]

Also, it would be nice to define a density on a real vector space as an orbit of the natural $\mathbb{Z}/2$-action (by $\pm$) on this 1-dimensional space of topdimensional alternating maps, and then prove that a density determines a measure.

[Heather Macbeth]

Finally (perhaps useful for @Kevin Buzzard) there is a hack for defining oriented angles in dimension 2: work with a real affine space modelled on $\mathbb{C}$ considered as a real vector space!

[Eric Wieser]

I think working in (exterior_algebra.ι R V).range ^ 2 gives you a poor mans exterior power?

[Heather Macbeth]

I don't know that syntax.

[Joseph Myers]

I think working in a two-dimensional subspace is appropriate for two-dimensional geometry results going in mathlib, with the special case where the whole space is two-dimensional then being deduced from the subspace version. If you're doing some random olympiad geometry problem rather than proving a result that might be used in other proofs, then making the whole space two-dimensional seems appropriate.

[Joseph Myers]

Yes, we need orientations of finite-dimensional real vector spaces (or whatever wider class of modules orientations make sense for) before defining oriented angles. I'm not sure offhand if orientations should be defined for submodules, or only for modules with the coercion from submodule to subtype and the module instance on that subtype then being used to get orientations for submodules. Also, I don't know if we have all the instances needed to get a Euclidean affine space structure on an affine subspace of a Euclidean affine space (which we'd need if only modules get orientations), but if we're missing any, they should be easy to add.

[Joseph Myers]

Then you need to decide if oriented angles are real numbers, or use the angle type from analysis.special_functions.trigonometric (real numbers mod 2π). And while oriented angles mod 2π are certainly useful and meaningful, for many geometrical purposes you actually want oriented angles mod π (the angle of a rotation from one undirected line to another) instead.

[Joseph Myers]

As noted above, until we have convexity for affine spaces, it's hard to talk about points being between other points, or on the same / different sides of a line (which is a major reason for not being able to state most olympiad geometry problems yet, as they tend to include such conditions to reduce configuration-dependence). Once we do have convexity for affine spaces (#2910), then I think we should define strict and weak versions of "between" in terms of it - both for a point being strictly or weakly between two points, and for an affine subspace being strictly or weakly between two points.

[Heather Macbeth]

I think one could get quite far with the complex-geometry hack:

import geometry.euclidean.basic

variables {P : Type*} [metric_space P] [normed_add_torsor ℂ P]

noncomputable theory

def oriented_angle (p1 p2 p3 : P) : real.angle :=
complex.arg ((p1 -ᵥ p2) / (p3 -ᵥ p2))

[Heather Macbeth]

Joseph Myers said:

Then you need to decide if oriented angles are real numbers, or use the angle type from analysis.special_functions.trigonometric (real numbers mod 2π). And while oriented angles mod 2π are certainly useful and meaningful, for many geometrical purposes you actually want oriented angles mod π (the angle of a rotation from one undirected line to another) instead.

Although it brings all these problems.

[Joseph Myers]

We should already have all the main pieces needed to construct an isometry between the complex plane and an arbitrary two-dimensional Euclidean affine (sub)space. But to actually use complex numbers to prove geometrical results stated in a more general context, we need a load of lemmas transporting all the geometrical definitions we have across isometries (and maybe an associated tactic to use those lemmas to reduce a general result to be proved to one for the complex plane). We don't have those lemmas at present, though I think they should be straightforward to add.

[Heather Macbeth]

Joseph Myers said:

We should already have all the main pieces needed to construct an isometry between the complex plane and an arbitrary two-dimensional Euclidean affine (sub)space.

Indeed: docs#complex.isometry_euclidean plus docs#linear_isometry_equiv.of_inner_product_space for the linear version, so what's missing is just the linear-to-affine glue.

[Heather Macbeth]

(and in particular, the definition of an affine isometry, as we were discussing the other day)

[Heather Macbeth]

Joseph Myers said:

But to actually use complex numbers to prove geometrical results stated in a more general context, we need a load of lemmas transporting all the geometrical definitions we have across isometries (and maybe an associated tactic to use those lemmas to reduce a general result to be proved to one for the complex plane). We don't have those lemmas at present, though I think they should be straightforward to add.

But all this is certainly missing, and moreover, it seems like an ugly way to prove things! I hope that in the "ideal" state of the library nothing is done this way :)

[Joseph Myers]

It's probably more for when someone wants to formalize a complex-bash solution to an olympiad problem.

[Heather Macbeth]

I see ... I wonder if that will ever be necessary? I think of complex numbers as being a way of doing geometry problems by brute force, in what is sometimes a slightly more human-comprehensible form than in real co-ordinates. But in Lean, I would think you can jump straight to the brute-force non-human-comprehensible version.

[Joseph Myers]

(Transporting across isometries can be useful in non-bash cases - anything where the proof involves reflecting the diagram and looking at the reflected points, for example. Likewise, transporting across similarities.)

[Heather Macbeth]

Yup, no objection to that!

[Kevin Buzzard]

This oriented angle definition is wonderful. I felt very uncomfortable with this random finrank V = 2 assumption, and didn't have a clue how to use it. I played (on paper) with Joseph's idea of defining an ordered angle to be what he called "direct isometries" modulo translations (assuming "direct isometry" means "orientation-preserving" -- we're not choosing an orientation here, we're preserving all of them :-) ) but for dim(V)=n+1 these "ordered angles" now seemed to be rotations of the n-sphere, and I wasn't sure if that was what we wanted them to be in general (angle A + angle B != angle B + angle A in general!).

[Joseph Myers]

Heather Macbeth said:

The space of topdimensional alternating maps from a real vector space is 1-dimensional, and under the natural $\mathbb{R}^+$ action it has two equivalence classes.

I've now implemented this definition of orientations (up to showing that these alternating maps are all multiples of the determinant and thus there are exactly two orientations). I'll do a series of PRs and then attempt to build oriented angles on top of orientations.

[Heather Macbeth]

@Joseph Myers That's great! By the way, @Oliver Nash was asking about the status of related things just the other day:
https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/determinant.20via.20exterior.20algebra

[Oliver Nash]

Incidentally, as Kevin pointed out to me, we can express the fact that $\wedge^n V$ is one-dimensional neatly by saying that $\wedge^n V$ is a multiplicative torsor for the non-zero scalars.

[Joseph Myers]

See #12106 for my work so far on oriented angles. As well as lots of lemmas just to set up the API, this includes a few more substantive geometrical results, e.g.

/-- Angle at center of a circle equals twice angle at circumference, oriented vector angle
form. -/
lemma oangle_eq_two_zsmul_oangle_sub_of_norm_eq {x y z : V} (hxyne : x ≠ y) (hxzne : x ≠ z)
  (hxy : ∥x∥ = ∥y∥) (hxz : ∥x∥ = ∥z∥) : hb.oangle y z = (2 : ℤ) • hb.oangle (y - x) (z - x) :=
begin
  have hy : y ≠ 0,
  { rintro rfl,
    rw [norm_zero, norm_eq_zero] at hxy,
    exact hxyne hxy },
  have hx : x ≠ 0 := norm_ne_zero_iff.1 (hxy.symm ▸ norm_ne_zero_iff.2 hy),
  have hz : z ≠ 0 := norm_ne_zero_iff.1 (hxz ▸ norm_ne_zero_iff.2 hx),
  calc hb.oangle y z = hb.oangle x z - hb.oangle x y : (hb.oangle_sub_left hx hy hz).symm
       ...           = (π - (2 : ℤ) • hb.oangle (x - z) x) -
                       (π - (2 : ℤ) • hb.oangle (x - y) x) :
         by rw [hb.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq hxzne.symm hxz.symm,
                hb.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq hxyne.symm hxy.symm]
       ...           = (2 : ℤ) • (hb.oangle (x - y) x - hb.oangle (x - z) x) : by abel
       ...           = (2 : ℤ) • hb.oangle (x - y) (x - z) :
         by rw hb.oangle_sub_right (sub_ne_zero_of_ne hxyne) (sub_ne_zero_of_ne hxzne) hx
       ...           = (2 : ℤ) • hb.oangle (y - x) (z - x) :
         by rw [←oangle_neg_neg, neg_sub, neg_sub]
end

[Kevin Buzzard]

We finally have a theorem which my kids learnt at the age of 15 :-)

[Joseph Myers]

Note that it took 50 preparatory PRs elsewhere in mathlib to get this far (though some of that is because I prefer to PR dependencies as I go along rather than mixing changes to lots of different bits of mathlib in the main PR).

[Johan Commelin]

@Joseph Myers Which is greatly appreciated! Your PRs are showcases of atomic PRs that do one thing and do it right!

[Heather Macbeth]

I've done a big refactor of oriented angles and 2d rotations which I am now tidying up for PR, and wanted to post about it to check that everyone is ok with the change.

The setting is an oriented real inner product space E of dimension 2. The existing constructions, by @Joseph Myers, first define oriented angles and 2d rotations with respect to an orthonormal basis, docs#orthonormal.oangle and docs#orthonormal.rotation. Then these constructions are proved to be the same for any two orthonormal bases of the same orientation, giving docs#orientation.oangle, docs#orientation.rotation.

Here is my branch for the new construction: https://github.com/leanprover-community/mathlib/compare/volume-form..almost-complex-2d
(I am giving the diff relative to #16487 since that PR itself has a +869 −352 diff.)

My proposed new construction gives a basis-free construction of oangle and rotation, which cuts 600 lines from the file. These lines are mostly made up again by a body of new theory, a new file inner_product_space/area_form. You can read the module docstring of that file for more about the approach. Suffice it to say that one develops the theory of a "rotation-by-90-degrees map" J and an "oriented-area-of-a-parallelogram" map ω -- we don't have oriented area yet but this map ω will also be helpful when it comes to constructing that.

Professional geometers (@Moritz Doll @Patrick Massot @Oliver Nash @Matej Penciak ...) will notice that this is all basically a version of the inner-product/symplectic/almost-complex/Kahler triangle, although for simplicity I have done everything in two dimensions. (I'd be glad of a naming idea for my construction kahler, which betrays its origin in a way which might be confusing for people expecting the more general version.)

This came out of sphere eversion, in some sense. I defined the three-dimensional analogue of all this (cross product, rotation by an angle about an axis) there, and then found the energy to redo the two-dimensional version on the same foundation (#16487).

[Joseph Myers]

Avoiding needing to develop the API for oriented angles twice, with respect to a basis and then a copy of that API with respect to an orientation (and #16279 adds the corresponding affine development for angles between points), is certainly attractive. But I think lemmas should be provided that the two definitions are equivalent, both on general principles of proving that different definitions are equivalent and for use in cases where calculations are more convenient with expressions involving separate complex numbers corresponding to the two vectors. That means four such lemmas (for each of oangle and rotation, providing a general lemma for any orthonormal basis with the right orientation, and a special-case one using fin_orthonormal_basis as the basis). I'd also expect a lemma proving that right_angle_rotation is equal to rotation by π / 2.

[Eric Wieser]

(I just looked at #16487 but couldn't see the titular feature for the trees of reasonable refactors / API lemmas)

[Heather Macbeth]

@Joseph Myers, what would you think of providing a single lemma for each of oangle and rotation, explaining how they can be calculated in a particular oriented orthonormal basis? It's not clear to me that we need to duplicate all the lemmas (but I am open to hearing a different point of view).

[Heather Macbeth]

@Eric Wieser I don't understand your comment (is it a question?)

[Heather Macbeth]

Heather Macbeth said:

Joseph Myers, what would you think of providing a single lemma for each of oangle and rotation, explaining how they can be calculated in a particular oriented orthonormal basis?

Oh, sorry, maybe I misread -- this is what you were proposing.

[Joseph Myers]

I suppose a single lemma for each would work; it would simply need to be used together with the lemma stating the orientation of fin_orthonormal_basis whenever a proof starts by rewriting into the complex number form but doesn't care more specifically about the choice of basis.

[Eric Wieser]

Apologies, I missed that it had a large tree of dependencies due to being on mobile, you can ignore my comment!

[Heather Macbeth]

@Joseph Myers Sorry, of course I don't mind adding 4 lemmas rather than 2; I had misread and thought you wanted to keep duplicate versions of all the dozens of lemmas.

[Heather Macbeth]

Now PR'd as #16596.