David Gross

Stream: new members

[David Gross]

First post. Hi Everyone!

I'm David Gross, a theoretical physicist working on quantum information and mathematical physics. (There's a Nobel laureate by the same name. For better or worse, that's not me).

I got interested in formal methods last year. As a medium-term project, I decided to have a go at formalization a general "de Finetti theorem".

Background:

The de Finetti Theorem of classical probability states that if a distribution of an infinite sequence of random variables is permutation-invariant, then it is a mixture of iid distributions.

Importantly for my day job, there are quantum analogues of this result. They find applications in many-body theory (mean field limit), quantum communication (security proofs for key distribution), and computational methods (convergence of semi-definite programming hierarchies).

What makes de Finetti's theorem an attractive formalization target is that it can be stated in the very general language of "ordered vector spaces with order unit". Here's an early example of this genre. It doesn't use much structure beyond plain vector spaces and convex cones, but still specializes to both the quantum and the classical case.

About a year ago, I've teamed up with Davood Tehrani to work out the details.

(BTW: Davood has been active around here as @Paradoxy. He, and by extension me, have benefitted a lot from the very welcoming atmosphere of this space! Thanks everybody!)

One piece of structure that is required is the notion of "tensors with infinite index set, which are equal to a distinguished element on all but finitely many indices". It's a well-known construction, e.g. in the theory of "infinite tensor products" of unital algebras, or of the "local observable algebra" of quantum statistical mechanics. A common realization is as an inductive limit of tensors indexed by finite subsets of some infinite set.

When trying to express this in Lean, we ran into a TODO item of PiTensorProduct.lean: "an API for the ways in which the index type can be split into subsets".

So to get off the ground, Davood and me had to put this piece of plumbing into place.

We feel that our efforts are now ready for community review. PRs are about to be
posted. (Big moment! :-))

On the one hand, the majority of the PRs is what I would think of as basic interface code. On the other hand, designing a useful API is hard, so we're looking forward to everybody's comments!

[Yaël Dillies]

David Gross said:

One piece of structure that is required is the notion of "tensors with infinite index set, which are equal to a distinguished element on all but finitely many indices"

Hey! This looks a lot like the restricted product construction that @Kevin Buzzard has been pushing for for FLT for a while now

[Kevin Buzzard]

It's a bit different and it's something we've not got in mathlib, it's restricted tensor product and like restricted product it's a colimit.

[David Gross]

Kevin Buzzard said:

It's a bit different and it's something we've not got in mathlib, it's restricted tensor product and like restricted product it's a colimit.

"Restricted tensor product" -- excellent, now we've got a good name for it! We didn't know what to choose before, because the C^* people call it (or its norm closure) the "infinite tensor product" (emphasizing that there's no bound on the size of the sets), while the physicists call it the "local algebra" (emphasizing the exact opposite aspect, namely that each set is finite). :slight_smile:

[Kevin Buzzard]

the Langlands people call it restricted tensor product (I didn't just make the term up!); it's how you make automorphic representations (representations of restricted products of groups) from local components.

[David Gross]

Our PRs have now been posted. We've broken the contribution into four pieces, with 32609 referencing the earlier ones.

Actually, a first question if I may: We've created each subsequent PR by branching off of the previous one. This led to each PR including the commits of the PR it depends on. Is that how things should be handled? I imagine it makes code review difficult.

We've checked existing PRs in the queue, and some show the same effect (32594), some don't (32534).

[Kevin Buzzard]

Just looking at the place where I learnt about this stuff (Flath's "decomposition of representations into tensor products") and he claims that the concept is introduced in Jacquet-Langlands "Automorphic forms on GL(2)" (a book which is really quite hard to read IMO). Here's some Flath:

Screenshot from 2025-12-08 21-30-30.png

[Kevin Buzzard]

PRs look good to me; nobody will review a PR with a depenency on an earlier one, they'll review the earlier ones first, so as things get merged you can merge master into the newer PRs. First one seems to be #32598 .

[David Gross]

Thanks!

In physics, people sometimes use the term "incomplete tensor product", after this early and lengthy paper by von Neumann on the Hilbert space version.

[David Gross]

Kevin Buzzard said:

First one seems to be #32598 .

That's right!

[Matt Diamond]

David Gross said:

Our PRs have now been posted. We've broken the contribution into four pieces, with 32609 referencing the earlier ones.

Actually, a first question if I may: We've created each subsequent PR by branching off of the previous one. This led to each PR including the commits of the PR it depends on. Is that how things should be handled? I imagine it makes code review difficult.

We've checked existing PRs in the queue, and some show the same effect (32594), some don't (32534).

In GitHub you can specify the "base" branch of your PR. If you set the "base" to the one that you branched off of, it should display only the commits in that PR. However, I'm not sure if this is possible when it's a PR from a forked repo, and it might not be worth the trouble here (especially since fixing Git mishaps can be tricky).

[Ruben Van de Velde]

You should not do that, and instead keep the target branch as master. We will not review pull requests before their dependencies have been landed anyway

[Ruben Van de Velde]

If the prs are independent rather than building up each on top of the other, you could (depending on your git proficiency) drop the previous work from the subsequent prs, though

[David Gross]

Thanks, Matt & Ruben! I think I understand your workflow better now.

As a result of the discussion, we have simplified the dependencies of our PRs. Things now look like this:

Two short independent PRs:

Dependent subsingletonEquiv
Composition of multilinear maps

Two longer ones depending on these:

"Set API" for tensor indices
Nested PiTensorProducts

(There's also two chores we addressed along the way.)