ContinuousBilinForm in Mathlib

Stream: Brownian motion

[Etienne Marion]

I've written some API for continuous bilinear forms, as they are an essential component of Gaussian measures on infinite-dimensional Banach spaces, because of the covariance operator. Following the message of Rémy about starting to PR some of the project to Mathlib, I thought this was a good start.
However, I am a bit afraid by the duplication it might create. A large part of what I introduced is not at all specific to continuous bilinear forms, and works well for LinearMap.BilinForm. On the other hand, I really want to be able to write things like f.IsSymm when f is a continuous bilinear form, and this does not work if I don't define IsSymm for ContinuousBilinForm. It does not either trigger a coercion to BilinForm, although LinearMap.BilinForm.IsSymm already exists.

import Mathlib

variable {𝕜 E : Type*} [NormedAddCommGroup E] [RCLike 𝕜] [NormedSpace 𝕜 E]

variable (𝕜 E) in
/- The type of continuous bilinear forms. -/
abbrev _root_.ContinuousBilinForm := E →L[𝕜] E →L[𝕜] 𝕜

variable (f : ContinuousBilinForm 𝕜 E)

/-- The underlying bilinear form of a continuous bilinear form -/
@[coe]
def ContinuousBilinForm.toBilinForm : LinearMap.BilinForm 𝕜 E where
  toFun x := f x
  map_add' x y := by simp
  map_smul' m x := by simp

instance : Coe (ContinuousBilinForm 𝕜 E) (LinearMap.BilinForm 𝕜 E) := ⟨toBilinForm⟩

#check f.IsSymm -- fails
#check LinearMap.BilinForm.IsSymm f -- fails
#check LinearMap.BilinForm.IsSymm (↑f) -- fails
#check LinearMap.BilinForm.IsSymm (f : LinearMap.BilinForm 𝕜 E) -- works, but lengthy, and explicit coercion
#check f.toBilinForm.IsSymm -- works, but lengthy, and explicit coercion

So here are my questions: can you think of a better way to define things so that the coercion does trigger automatically? If not, then do you think it's ok if I duplicate some API? (In the end I do not need much of what already exists for BilinForm, it's more a matter of principle. I also intend to define concepts for ContinuousBilinForm which would still make sense for BilinForm, but I'm not sure I want to define them for BilinForm because that would just duplicate things I have no use for.)

[David Ledvinka]

#check LinearMap.BilinForm.IsSymm (R := 𝕜) (M := E) f works (although obviously not a good solution). I believe it may be an instance of this issue. The last option you listed f.toBilinForm.IsSymm doesn't seem that bad to me tbh.

[Rémy Degenne]

The choice seems to be between duplication and adding toBilinForm. The latter does not sound too bad?

[Etienne Marion]

Then I would also write f.toBilinForm.toMatrix. It feels a bit heavy to me, but I agree it's better than duplication. I think I'll go with that.

[Etienne Marion]

Actually I can't even write f.toBilinForm.toMatrix for some reason, I think that's because toMatrix is an equiv so it does not support dot notation. I think I'll keep things as they are.

[Etienne Marion]

I opened #26274. In the end I stuck with f.toBilinForm.IsSymm but I redefined toMatrix to allow for dot notation.

[Etienne Marion]

I went back to this today but honestly I am at a loss as to what to do. I have #28052 defining positive semidefinite sesquilinear maps and #26315 for continuous ones, but I am worried that relying too much on abbreviations will lead to lots of duplication. But I also think that I do not want to work with ContinuousSesquilinForm when the map is actually bilinear.

[Rémy Degenne]

Perhaps you should post a question about that issue in a more visible channel, with a summary of all the abbreviations that could possibly be involved (and the ones that are already there), and the long expressions that one should write if the abbreviations are not used.
I won't have much time to look at that question for a week at least, but this is something that is not specific to our project and I think others who are not in this project channel could give valuable advice on how to proceed.

[Rémy Degenne]

Etienne wrote a description of the issue here: #mathlib4 > Duplication for sesquilinear forms and bilinear forms

[Etienne Marion]

I went for duplicating code from sesquilinear forms but won't do the duplication for continuous bilinear forms, so I wont introduce a ContinuousBilinForm abbreviation like I did in the project. I wrote the PRs in #Brownian motion > Mathlib PRs, it's mostly about sesquilinear forms, which we don't really need but positive semidefinite forms and their links with positive semidefinite matrices make sense in that generality so it would not be great to restrain the definition to the bilinear case only.