Correct formulation: Existence statement for canonical elts

Stream: mathlib4

[Stefan Kebekus]

Dear all,

I would greatly appreciate any help you can give me in formulating an existence statement for a canonical element. I have little experience in lean4 and wonder about the most idiomatic (and valuable) formulation.

Long story: If $E$ is a finite-dimensional inner product space, then there exists a canonical element $s \in E \otimes E$. The element is the image of the inner product under the natural identification $(E \otimes E)^*$ and can be computed from any orthonormal basis $v_i$ as $s = \sum_i v_i \otimes v_i$.

The fact that $s$ is canonical allows me to write down the Laplacian in a coordinate-free manner: if $f$ is a function on $E$, then $(\Delta f) = f''(s)$. Analogous coordinate-free presentations exist for gradients and other differential operators.

Should I write an existence statement, "There exists $s$ such that …", or should I be writing a map from "finite-dimensional inner product spaces" to "their elements"? Is there a formulation allowing me to take a space E and write something like E.canonicalTensor?

Best,

Stefan.

[Sébastien Gouëzel]

Note that currently second derivatives are defined as bilinear maps, not as maps on the tensor product (and this is genuinely different, since the former approach also works in infinite dimension while the latter only makes sense in finite dimension). So it means you will need some manipulations to follow this approach.

As for your question, the answer is the second approach: construct an element associated to the space. And then show that whatever basis you use, it gives rise to the same element. A good example of this, already in mathlib, is the canonical volume form on a finite-dimensional inner product space. It is defined in docs#measureSpaceOfInnerProductSpace using one specific choice of a basis, but there are several lemmas (see e.g. docs#Orientation.volumeForm_robust or docs#OrthonormalBasis.addHaar_eq_volume) showing that it is in fact independent of the choice.

[Stefan Kebekus]

@Sébastien Gouëzel Understood. I will proceed as you suggested. I learned that you use a "def" in your example while I was unsuccessfully experimenting with an "instance" instead. Copying your code solved all my problems.

As usual, Thank you for your incredibly prompt and helpful reply!