[Merged by Bors] - feat(geometry/euclidean): angles and some basic lemmas

[jsm28]

Define angles (undirected, between 0 and π, in terms of inner
product), and prove some basic lemmas involving angles, for real inner
product spaces and Euclidean affine spaces.

From the 100-theorems list, this provides versions of

• 04 Pythagorean Theorem,
• 65 Isosceles Triangle Theorem and
• 94 The Law of Cosines, with various existing definitions implicitly providing
• 91 The Triangle Inequality.

[jcommelin]

@jsm28 Note: the first post on a PR page becomes the final commit message. You post contains a lot of interesting info, but I think it shouldn't end up in the commit message of this PR. Would you mind reposting it below, and editing the first post?

[jsm28]

It seems reasonable to me for some geometrical results about real
inner product spaces to go in geometry/euclidean.lean rather than
analysis/normed_space/real_inner_product.lean. However, some of the
lemmas about real inner product spaces don't involve angles and aren't
particularly geometrical; quite possibly some of the lemmas should
actually go in analysis/normed_space/real_inner_product.lean.

Note that there are many other basic geometrical concepts not yet
defined in mathlib, and the results proved are strongly biased to
those that can conveniently be stated and proved with only the
definitions present so far. For example, all of the following would
be relevant to more complete support for Euclidean geometry, but are
not yet present (and all of them would need many basic results once
added):

• lines and planes (affine subspaces of a given dimension);

• collinearity and coplanarity of points;

• circles and spheres (I expect it will be useful to have a structure
  type that stores the centre, radius and a proof that the radius is
  positive, not just the sphere as a set of points defined for
  metric spaces), and tangency;

• n-simplexes (n+1 affine-independent points), and thus triangles as
  2-simplexes;

• area and volume (n-dimensional Lebesgue measure) (and also length of
  a curve / area of a surface);

• betweenness, as in Tarski's axioms (although some lemmas added here
  about angles equal to π are equivalent to corresponding results for
  strict betweenness);

• various other kinds of angles (undirected angles between 0 and 2π,
  using some form of disambiguation for which side of the angle is
  wanted; directed angles modulo 2π, in oriented 2-space, as a
  function of a rotation; directed angles modulo π, in oriented
  2-space, as the rotation angle between two lines, which are often
  the most convenient kind of angle to reduce configuration-dependence
  in proofs; solid angles, in any dimension);

• Cartesian and barycentric frames and coordinates (I suspect it will
  be useful to be able to work with frames for a subspace, not just
  for the whole Euclidean space);

• similarity transformations, and properties of similarities and
  isometries in Euclidean space.

[jsm28]

Moved most of it to a comment.

[jcommelin]

A lot of interesting stuff! Thanks a lot!
I left a bunch of comments. (sometimes a bit brief, but they are certainly not meant harsh)
Mostly about naming things.

[jsm28]

I've also now formalised a proof of 27: Sum of the Angles of a Triangle that builds on this PR, but this PR is big enough anyway it seems best to leave that proof for another PR rather than adding it to this one.

[jcommelin]

Moved most of it to a comment.

@jsm28 Now that I think of it... your long todo list should maybe be moved to an "issue" here on github. That way we will be reminded of it, and can easily find it. Once this PR is merged, this page (and it's commit message) will be somewhat lost in the sea of history.

[jcommelin]

Is there anything you still want to work on, or is this ready for request-review again?

[jsm28]

There is an open question above about whether versions of Pythagoras not using angle should be moved to analysis.normed_space.real_inner_product, and @urkud wanted to merge the proof of one form of equality case for Cauchy-Schwarz with the main proof of that result in some form.

[jcommelin]

@urkud Do you still want to work on this one? Or can we merge this, and do other stuff in a follow-up PR?

[jcommelin]

Thanks 🎉

bors merge

[urkud]

I'm sorry for forgetting about this PR. I'll refactor proofs if I'll have time later.

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests and docs