feat(geometry/euclidean/ceva) : Ceva's Theorem, problem 61 on Freek's list

[MantasBaksys]

Prove Ceva's Theorem in the interior case.

---

• depends on: [Merged by Bors] - feat(linear_algebra/affine_space/basis): reindex API #18190

The exterior case can easily be stated and proved once we have signed distances and the biratio of three points.

[jsm28]

Results in mathlib should generally be given in appropriately general form.

Ceva's theorem (+ converse, which I'm generally considering together) is essentially an affine result; it should work in any affine space (for a vector space over any field), with no restriction to the reals, as long as you express things without involving the notion of "distance". Even with distance involved, nothing should depend on the space being Euclidean (that is, an inner product being involved); everything should work for an arbitrary real normed_add_torsor. Furthermore, nothing about the statement of Ceva should depend on the ambient space being two-dimensional as you have here; it's just as true for triangles embedded in a higher-dimensional space. (There is a genuinely Euclidean, genuinely ambient-two-dimensional version of Ceva: the version based on ratios of sines of oriented angles rather than of signed lengths. That one can be ignored for now; we don't yet have oriented angles, though I'm working towards adding them.) In fact, you shouldn't need the feet of the cevians in the interior of the sides either; the products will still be equal when those feet are anywhere on the side lines (even if they coincide with vertices, I think), whether you use distance or something chosen to reflect that the result holds for signed distances. It's only for the converse, if you want "concurrent" rather than "concurrent or parallel" as the conclusion, that being in the interiors of the sides may be relevant (it could be stated more generally based on some quantity being positive, but the specific case of interiors of sides is a useful special case there).

Then, there are n-dimensional versions of Ceva. So it would seem most appropriate to prove results in an n-dimensional case and only then deduce 2-dimensional versions.

Note that the appropriate conditions may differ between the various general results and their converses. If you want to prove a converse (hypothesis on ratios, conclusion of lines being concurrent or parallel), you don't need the points given to be affinely independent; they can be an arbitrary indexed family of points (might need to be a finite indexed family until affine combinations are refactored to use finsupp, but in principle I don't think it even needs to be finite). You're looking at conditions for lines through the points in such a family to be concurrent or parallel, where the lines are expressed (a) in terms of having a direction given by a weighted_vsub of points in the family (this version is the most general because it allows for lines that never meet the opposite face at all) or (b) as an affine span of a point and an affine_combination of the points in the family (I don't think you need to say that the point in question is weighted 0, but if you even do then that would be a third variant). Then if the weights are all appropriately consistent with some (finitely supported) choice of weights for all the points in the family, then you have "concurrent or parallel" (over a field, maybe even over a division ring if things are expressed correctly, but quite possibly you do need commutativity); which of "concurrent" and "parallel" it is depends on whether the weights you get for all the points add to zero (parallel) or nonzero (concurrent). Furthermore, if you structure things as "concurrent at thing given point" or "parallel to this given direction", it's quote possible that versions that can be given that work over rings without needing inverses.

For "concurrent or parallel implies weights consistent", it's also likely that things can be done over a ring (maybe needing commutativity, maybe not), but you do need affine independence.

So I expect you get lots of different n-dimensional variants each with the weakest hypotheses that work for that result (and then some iff results that may need stronger hypotheses than the individual directions), before getting onto specific versions for three points (still in a general affine context), before getting onto three-point versions using an ordered ring or field to apply positivity of various expressions to get "concurrent" and not "parallel", before getting onto versions in a real normed_add_torsor. You might well end up with rather more Lean code than you have at present, because of having so many variants, but I also expect pretty much all the proofs of individual lemmas should be much shorter as a result of splitting things up into such lemmas.

[jsm28]

It's possible that structuring things like I suggest will mean some of your current lemmas are no longer used in the proof, but it's quite possible that such lemmas (in whatever their most general form is) are still mathlib-appropriate somewhere.

[jsm28]

Also note that any PR adding a result from Freek's list should make sure to update docs/100.yaml.

[MantasBaksys]

Thanks for the comments @jsm28 and for pointing out the shortcomings of my work. It seems like there's a hell of a lot more work to do and I cannot help but feel a bit lost while thinking about how to structure my work next. Perhaps there is a resource on Ceva's Theorem in its full generality somewhere?

[jsm28]

I don't know of such a resource. A lot of doing things for the weakest type classes is working out as you go along what the weakest type class some fragment of the result is true for is (and you might e.g. try proving for ring, and only discover during the proof that actually you need comm_ring, division_ring or field), rather than having a statement in the literature that actually says what type class should be used at each step.

Note that this includes stating things in the way that's true most generally. Sometimes multiple statements may be obviously (to a human mathematician) equivalent for fields, but not equivalent for a weaker type class, in which case it's appropriate to give the statement in whichever form allows the weakest hypotheses, and then maybe deduce the other variants (where useful) that need stronger hypotheses. This is where my point about working with arbitrary indexed families of points comes in: some things don't need affine independence, and nothing needs the points to span the whole space. That in turn indicates that formulating lemmas and proofs to express things using affine combinations rather than barycentric coordinates is more appropriate: the two are very similar mathematically, but barycentric coordinates introduce both a requirement for affine independence (only needed for some results) and one for the points spanning the whole space (not needed for any results).

(It's possible to use barycentric coordinates in a proof of a result that only requires the family of points to be independent but not necessarily spanning, by passing back and forth between the original space and the affine_span of those points. However, if you want to do that, first you need to set up a load of API for moving between an affine space and an affine subspace. Or, rather, you need to define the affine map from the subtype for a subspace to the whole space (an obvious missing piece of API, which would be modelled on the API for submodule.subtype), then I expect most of the rest of the API would be about moving across affine maps, or injective affine maps, as appropriate, rather than restricted to this one particular affine map. But, while that would certainly be a worthwhile addition to the API for affine subspaces, I don't really expect the proofs using barycentric coordinates on a subspace would generally end up simpler than just using affine combinations directly in the original space.)

Similarly, the idiomatic way of talking about the line through two points is to talk about the affine_span of those two points. That also allows expressing things more generally than talking about collinear, given that collinear is only defined over a field. (Since some things about dimensions of vector spaces have been reworked to apply to more general modules, it's possible some things in affine_space.finite_dimensional could also be adapted to work more generally than just for field. But I think collinear, at least with the present definition, would still be more awkward to work with over general rings than the affine span of two points; over a general ring, you can have sets that are collinear but don't lie in the affine span of any two points.)

Indeed, a fair number of lemmas involved in doing things in general would I think be lemmas about a single cevian, before you get onto configurations with multiple such lines: talking about when a point lies on such a cevian, before talking about when it lies on all cevians. And in turn those would likely be based on lemmas about the affine_span and vector_span of two points, not expressed in terms of an indexed family at all; we don't have any such lemmas at present, but there are certainly things to be said about such spans (see the various span_singleton lemmas for submodules, from which results about spans of two points in an affine space would probably be deduced), some of which are likely to be of use when working with the intersection of such spans.

All those lemmas should be pretty trivial, with proofs of at most a few lines. But mathematically, Ceva's theorem itself is pretty trivial; in terms of affine combinations / barycentric coordinates, it's just talking about proportions among n-tuples of numbers, and if it takes more than a few lines of manipulation to translate between different forms of the result, that suggests some lemmas to help with that manipulation are missing. (Indeed, for the converse or iff form of the triangle version, there is probably some result to be stated and proved for fields (if not anything more general) with nothing geometric or affine at all: a necessary and sufficient condition to have three numbers that are pairwise in the same ratios as three pairs of numbers. Or maybe there is a case for defining some notion or notions of subsets of indexed families of numbers being in the same ratios, and proving basic things about such notions, in order to use them in various forms of Ceva.)

[jsm28]

It might make sense to put this form of Ceva in archive/ until we have more general versions in mathlib, but various lemmas that suggest more general results should be split out to go into mathlib proper (in their appropriately general forms) first. I think it's best to put such lemmas in separate PRs (one PR for each lemma, or group of closely related lemmas in the same part of mathlib) for convenience of review. I'll comment separately on those lemmas that seem particularly well suited to splitting out API into mathlib proper (in one case I've already PRed a set of relevant lemmas that seem more general and so more suitable for mathlib than the specific one in this file).

[jsm28]

This one might be appropriate for mathlib more or less as is, when stated over an arbitrary field and put in linear_algebra.affine_space.finite_dimensional. However, note that a name starting affine.simplex. might be more useful than one starting affine_span. because it would enable use of the lemma with dot notation.

[YaelDillies]

It requires linear_algebra.affine_space.finite_dimensional and linear_algebra.affine_space.independent, and neither imports the other. Is there a common child file close enough?

[jsm28]

linear_algebra.affine_space.finite_dimensional imports linear_algebra.affine_space.independent.

[MantasBaksys]

It might make sense to put this form of Ceva in archive/ until we have more general versions in mathlib, but various lemmas that suggest more general results should be split out to go into mathlib proper (in their appropriately general forms) first. I think it's best to put such lemmas in separate PRs (one PR for each lemma, or group of closely related lemmas in the same part of mathlib) for convenience of review. I'll comment separately on those lemmas that seem particularly well suited to splitting out API into mathlib proper (in one case I've already PRed a set of relevant lemmas that seem more general and so more suitable for mathlib than the specific one in this file).

Hey @jsm28! I've been super busy for the past two weeks, sorry for not responding to your suggestions. Unfortunately, the earliest I can come back to work on this properly will be by late January. I'm interested in formalizing the higher generality Ceva's theorems, as you've suggested, but that will of course take some time. In the meantime, I'd agree with putting the current version in archive/.

[robertylewis]

Not a full review, just some minor stylistic points.

[anders-was-here]

For reference, as Yaël Dillies mentioned this PR in Zulip.

I have tried to adapt the Ceva theorem proof from Metamath.

Available at: https://gist.github.com/anders-was-here/d786450daba4c01e40bbc5f81c681feb

The Metamath proof/formalization by Saveliy Skresanov: http://us.metamath.org/mpeuni/cevath.html

(It's totally unpolished, it was mostly for learning Lean and Metamath and for fun. Maybe the sigar* lemmas could have some use elsewhere in Mathlib).

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(linear_algebra/affine_space/basis): reindex API #18190
  By Dependent Issues (🤖). Happy coding!

[YaelDillies]

@jsm28, could you state (in Lean, if possible!) the higher dimensional version you're thinking of? Also, should we use intrinsic_interior instead of interior, to allows arbitrary codimension (as opposed to the current codimension 0 restriction)?

[jsm28]

The following is for any affine space over a field, with no requirements for any order on the field (and thus not involving distance or interior), and some lemmas may well be true in more general contexts, such as rings or division rings, in which case they should be proved in such contexts. Appropriate nondegeneracy conditions will need to be added for each result. Results may be true in some form for infinite indexed families or they may require the families to be finite; they're probably simpler to state and prove in the finite case. It's never required for the families to span the whole space.

Forward direction (concurrent or parallel implies ratios): consider some indexed affinely independent family of points (simplex, if finite). For each point p in that family, consider the line through it and some affine combination of the points (sum of weights equals 1; there might be a nonzero weight on p); that is, the affine_span (notation line) of the two points. (a) If the lines concur, there is some choice of weights for all the points in the family, sum 1, such that, for each point p in the family, if we look at the weights for the other point on the line through p, then, disregarding the weight on p itself, the other weights are proportional to the relevant weights in the global choice of weights for all the points in the family. Also, the affine combination with that global choice of weights is where the lines concur. (b) If the lines are parallel, the same conclusion arises, but this time the global choice of weights has sum 0 and the direction of all the lines is the span of the weighted_vsub with those weights.

Reverse direction (ratios imply concurrent or parallel): consider some indexed family of points, which doesn't need to be affinely independent. Suppose we are given some global allocation of weights to the points. (a) Suppose the sum of the weights is 1 (or more generally nonzero); then if we take lines through each point p in the family and some affine combination, sum of weights 1, weights on the other points proportional to the global weights, then those lines concur at the affine combination given by the global weights (scaled as necessary if we allow an arbitrary nonzero sum of weights). (b) Suppose the sum of the weights is 0; then those lines are parallel, in the direction spanned by the weighted_vsub with the global weights.

It should be clear how, with three points and appropriate nondegeneracy conditions, pairwise weights being proportional to a global choice of weights is equivalent to the product of three ratios being 1. (And as a further special case, in a real normed_add_torsor you can talk about ratios of distances rather than weights, for points on the side lines; results should still generally be true when the point of concurrence is outside the triangle.)

When you have an ordered field, positive weights would allow you to exclude the "parallel" case in the reverse direction, as a special case. The point of concurrence would indeed be in the intrinsic interior, if that's worth mentioning. I'm not sure you get anything much useful with (intrinsic) interior as a hypothesis in the forward direction, unless it's as a convenient alternative to other nondegeneracy conditions.