Duplication for sesquilinear forms and bilinear forms

Stream: mathlib4

[Etienne Marion]

Hi! In the Brownian Motion project we proved a few results about bilinear forms. In particular we consider positive semidefinite continuous bilinear forms. I want to add positive semidefinite bilinear forms to mathlib, and from my point of view the definition should be (pseudo-code):

structure IsPosSemidef (B : M →ₛₗ[I] M →ₗ[R] R) : Prop where
  eq : ∀ x y, I (B x y) = B y x
  nonneg : ∀ x, 0 ≤ B x x

which is what I did in #28162, by extending LinearMap.IsSymm and LinearMap.Nonneg which I define in #28162. But as I said in our context we are dealing with bilinear maps, so having to deal with a RingHom.id due to the symmetry is a bit annoying. I thought I would just write a lemma for the specific case where I = RingHom.id. But then I noticed that LinearMap.BilinForm.IsSymm already exists, and the file is roughly a copy of the one for sesquilinear forms. I was surprised by such duplication.

I ended up wondering whether duplication was fine if it allowed to deal with bilinear forms without ever having to mention sesquilinear forms. In particular, should I define positive semidefinite bilinear forms, i.e. duplicating the above definition for LinearMap.BilinForm?

I am a bit lost and I don't know which is better: duplicating definitions feels wrong, but keeping only one definition still requires duplicating some lemmas for the special case, so in the end maybe duplicating definitions is not so bad so that when dealing only with bilinear forms you don't have to worry about sesquilinear forms at all.

But then there is also the issue that we want continuous bilinear forms in the project, so should I keep on duplicating and create a special definition for continuous bilinear forms as well? This feels like it would lead to too much duplication.

I am sorry if the message is not clear, I have been struggling with these questions for some time now and I still cannot decide what is the right way to go.

[Etienne Marion]

Unless somebody thinks it's better otherwise, I think what I will do is duplicate IsPosSemidef for bilinear forms as the duplicate already exists for IsSymm, but I won't duplicate for continuous bilinear forms and just introduce a ContinuousLinearMap.toBilinForm.

[Antoine Chambert-Loir]

It seems one might wish for a BilinFormClass.

[Etienne Marion]

This might be the best solution for dealing with continuous bilinear forms. But it does not solve the question of bilinear forms vs sesquilinear forms.