I completely agree. Lemmas are simple, obvious, and yet they completely change how you think.
How many proofs cite the Axiom of Choice? How many cite Zorn's Lemma? Which is more important, the axiom that we're relying on, or the restatement of the axiom that allows us to actually prove things?
It is not just mathematics that values simple and obvious ideas that change how you think. We all should value that. Like Stein's Law, "Things that can't go on forever, don't." And Davies' Corollary, "Things that can't go on forever, can go on longer than you think they can."
signa11 20 hours ago [-]
> Lemmas are simple, obvious, and yet they completely change how you think.
speak only for yourself :o) , they are the reason we have:
lemma now, dilemma later
ForceBru 19 hours ago [-]
Yeah, I can't say lemmas are (generally, or even often) simple and obvious. To me, they often seem arbitrary: what do you mean before we prove this grand theorem we have to prove these completely unrelated lemmas? Okay, proved the lemmas. Now the proof of the theorem has "according to such and such lemmas..." sprinkled around, but I've already forgotten what the lemmas were and why they're applicable. I also can't name any lemmas that changed how I think.
btilly 12 hours ago [-]
My first ever paper was a pretty good entry at this. https://dspace.library.uvic.ca/server/api/core/bitstreams/66... 16 lemmas, one theorem. The theorem makes all of the lemmas obvious. Though, in retrospect, I should have separated out the characteristic 0 case into a second theorem.
But the fact that most lemmas are like this, does not mean that all are. Whether we call it a lemma, or something else, the more important ideas are the ones that result in thinking differently. And something like Zorn's lemma, makes us think differently.
emil-lp 22 hours ago [-]
I'm not sure your choice is the best. Axiom of choice is an axiom, not a theorem. In addition, axiom of choice is frequently stated (contrary to most other axioms) in proofs and assumptions.
The division of lemmas and theorems is really a bit artificial for these things. But yeah I think the spirit is that a theorem is an object that you aim to study, while a lemma is something you use to do that. Fermat's last theorem was a target, but the techniques including lemmas used and developed for it are the real prize for a working mathematician. Sculptures are kind of the point, but there's no question the tools used for sculpting are more useful and "worth" more in that sense.
trostaft 14 hours ago [-]
Ah the JL lemma. Probably one of my favorite too. I'm teaching a mathematics of data course next semester, and even though we don't assume probability as a prerequisite I'm going to find a way to talk about that idea.
srean 13 hours ago [-]
I am sure you know this, but inner-products are not preserved, the el_2 distance is (approximately).
So it needs judicious care when used along with algorithm s that work with inner-products
dchftcs 11 hours ago [-]
If you preserve the l2 distance you preserve the inner product, that's somewhat tautological in an L2 space. Just that the degree you can preserve inner products can be misleading, main problem is that orthogonal vectors may only become near-orthogonal which is sometimes a big deal, though perfect correlations are preserved because the JL transform is linear. Both can be seen looking at: https://en.wikipedia.org/wiki/Polarization_identity
srean 11 hours ago [-]
> If you preserve the l2 distance you preserve the inner product
That's trivially untrue. You can move the origin around and that doesn't change the el_2 metric but will change the inner product.
This would not happen for random rotations of course because they do not change the origin. However random Euclidean motions can change the origin.
dchftcs 11 hours ago [-]
Right, indeed you need to first preserve the origin, but also that is trivially true for a linear map like JL.
srean 11 hours ago [-]
As far as I can recall JL holds for affine transformations too, in any case it's an existence result. Have to double check on the affine bit.
The popular proof does uses random linear transforms and they indeed will not change the origin, but that's just one class of transforms with the JL property.
practal 22 hours ago [-]
> Even more important than lemmas are observations, but that is another story.
In my book about abstraction logic (http://abstractionlogic.com) I have definitions, theorems, lemmas, and even observations :-) Just did a count of the frequency. Of course, not sure what those frequencies say about the relative importance.
-----------
Definitions 78
Theorems 20
Lemmas 76
Observations 41
whateveracct 1 days ago [-]
coyoneda lemma has been helping me out (in prod - at FAANG even!) for over a decade
LPisGood 1 days ago [-]
How has it helped in production software? Are you writing a lot of Haskell?
whateveracct 23 hours ago [-]
yes
nxobject 24 hours ago [-]
I guess homological algebra must be worth at least a million theorems, then?
How many proofs cite the Axiom of Choice? How many cite Zorn's Lemma? Which is more important, the axiom that we're relying on, or the restatement of the axiom that allows us to actually prove things?
It is not just mathematics that values simple and obvious ideas that change how you think. We all should value that. Like Stein's Law, "Things that can't go on forever, don't." And Davies' Corollary, "Things that can't go on forever, can go on longer than you think they can."
speak only for yourself :o) , they are the reason we have:
But the fact that most lemmas are like this, does not mean that all are. Whether we call it a lemma, or something else, the more important ideas are the ones that result in thinking differently. And something like Zorn's lemma, makes us think differently.
Johnson–Lindenstrauss lemma
https://en.wikipedia.org/wiki/Johnson%E2%80%93Lindenstrauss_...
Isolation lemma
https://en.wikipedia.org/wiki/Isolation_lemma
Schwartz–Zippel lemma
https://en.wikipedia.org/wiki/Schwartz%E2%80%93Zippel_lemma
Lovász local lemma
https://en.wikipedia.org/wiki/Lov%C3%A1sz_local_lemma
So it needs judicious care when used along with algorithm s that work with inner-products
That's trivially untrue. You can move the origin around and that doesn't change the el_2 metric but will change the inner product.
This would not happen for random rotations of course because they do not change the origin. However random Euclidean motions can change the origin.
The popular proof does uses random linear transforms and they indeed will not change the origin, but that's just one class of transforms with the JL property.
In my book about abstraction logic (http://abstractionlogic.com) I have definitions, theorems, lemmas, and even observations :-) Just did a count of the frequency. Of course, not sure what those frequencies say about the relative importance.
-----------
Definitions 78
Theorems 20
Lemmas 76
Observations 41