Continuous bilinear forms #
Instances For
The underlying bilinear form of a continuous bilinear form
Equations
- f.toBilinForm = { toFun := fun (x : E) => β(f x), map_add' := β―, map_smul' := β― }
Instances For
A continuous bilinear form f
is symmetric if for any x, y
we have f x y = f y x
.
Instances For
Polarization identity: a symmetric continuous bilinear form can be expressed through values it takes on the diagonal.
A symmetric continuous bilinear form is characterized by the values it takes on the diagonal.
A symmetric continuous bilinear form is characterized by the values it takes on the diagonal.
A continuous bilinear map on a finite dimensional space can be represented by a matrix.
Equations
- f.toMatrix b = (BilinForm.toMatrix b) f.toBilinForm
Instances For
Equations
Instances For
A continuous bilinear map f
is positive if for any 0 β€ x
, 0 β€ re (f x x)
Instances For
A continuous bilinear map is positive semidefinite if it is symmetric and positive. We only define it for the real field, because for the complex case we may want to consider sesquilinear forms instead.
Instances For
The inner product as continuous bilinear form.Β
Equations
- ContinuousBilinForm.inner E = (LinearMap.mkβ β (fun (x y : E) => inner β x y) β― β― β― β―).mkContinuousβ 1 β―