Continuous bilinear forms #

@[reducible, inline]

abbrev ContinuousBilinForm (𝕜 : Type u_1) (E : Type u_2) [NormedAddCommGroup E] [RCLike 𝕜] [NormedSpace 𝕜 E] :

Type (max u_2 u_1 u_2)

Equations

ContinuousBilinForm 𝕜 E = (E →L[𝕜] E →L[𝕜] 𝕜)

Instances For

def ContinuousBilinForm.toBilinForm {𝕜 : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [RCLike 𝕜] [NormedSpace 𝕜 E] (f : ContinuousBilinForm 𝕜 E) :

LinearMap.BilinForm 𝕜 E

The underlying bilinear form of a continuous bilinear form

Equations

f.toBilinForm = { toFun := fun (x : E) => ↑(f x), map_add' := ⋯, map_smul' := ⋯ }

Instances For

source

@[simp]

theorem ContinuousBilinForm.toBilinForm_apply {𝕜 : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [RCLike 𝕜] [NormedSpace 𝕜 E] (f : ContinuousBilinForm 𝕜 E) (x y : E) :

(f.toBilinForm x) y = (f x) y

source

theorem ContinuousBilinForm.ext_basis {𝕜 : Type u_1} {E : Type u_2} {n : Type u_3} [NormedAddCommGroup E] [RCLike 𝕜] [NormedSpace 𝕜 E] (b : Basis n 𝕜 E) {f g : ContinuousBilinForm 𝕜 E} (h : ∀ (i j : n), (f (b i)) (b j) = (g (b i)) (b j)) :

f = g

source

structure ContinuousBilinForm.IsSymm {𝕜 : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [RCLike 𝕜] [NormedSpace 𝕜 E] (f : ContinuousBilinForm 𝕜 E) :

Prop

A continuous bilinear form f is symmetric if for any x, y we have f x y = f y x.

map_symm (x y : E) : (f x) y = (f y) x

Instances For

source

theorem ContinuousBilinForm.isSymm_def {𝕜 : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [RCLike 𝕜] [NormedSpace 𝕜 E] (f : ContinuousBilinForm 𝕜 E) :

f.IsSymm ↔ ∀ (x y : E), (f x) y = (f y) x

source

theorem ContinuousBilinForm.IsSymm.polarization {𝕜 : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [RCLike 𝕜] [NormedSpace 𝕜 E] {f : ContinuousBilinForm 𝕜 E} (x y : E) (hf : f.IsSymm) :

(f x) y = ((f (x + y)) (x + y) - (f x) x - (f y) y) / 2

Polarization identity: a symmetric continuous bilinear form can be expressed through values it takes on the diagonal.

source

theorem ContinuousBilinForm.ext_of_isSymm {𝕜 : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [RCLike 𝕜] [NormedSpace 𝕜 E] {f g : ContinuousBilinForm 𝕜 E} (hf : f.IsSymm) (hg : g.IsSymm) (h : ∀ (x : E), (f x) x = (g x) x) :

f = g

A symmetric continuous bilinear form is characterized by the values it takes on the diagonal.

source

theorem ContinuousBilinForm.ext_iff_of_isSymm {𝕜 : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [RCLike 𝕜] [NormedSpace 𝕜 E] {f g : ContinuousBilinForm 𝕜 E} (hf : f.IsSymm) (hg : g.IsSymm) :

f = g ↔ ∀ (x : E), (f x) x = (g x) x

A symmetric continuous bilinear form is characterized by the values it takes on the diagonal.

source

theorem ContinuousBilinForm.isSymm_iff_basis {𝕜 : Type u_1} {E : Type u_2} {n : Type u_3} [NormedAddCommGroup E] [RCLike 𝕜] [NormedSpace 𝕜 E] (f : ContinuousBilinForm 𝕜 E) (b : Basis n 𝕜 E) :

f.IsSymm ↔ ∀ (i j : n), (f (b i)) (b j) = (f (b j)) (b i)

source

noncomputable def ContinuousBilinForm.toMatrix {𝕜 : Type u_1} {E : Type u_2} {n : Type u_3} [NormedAddCommGroup E] [RCLike 𝕜] [NormedSpace 𝕜 E] (f : ContinuousBilinForm 𝕜 E) (b : Basis n 𝕜 E) [Fintype n] [DecidableEq n] :

Matrix n n 𝕜

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

source

@[simp]

theorem ContinuousBilinForm.toMatrix_apply {𝕜 : Type u_1} {E : Type u_2} {n : Type u_3} [NormedAddCommGroup E] [RCLike 𝕜] [NormedSpace 𝕜 E] (f : ContinuousBilinForm 𝕜 E) (b : Basis n 𝕜 E) [Fintype n] [DecidableEq n] (i j : n) :

f.toMatrix b i j = (f (b i)) (b j)

source

theorem ContinuousBilinForm.dotProduct_toMatrix_mulVec {𝕜 : Type u_1} {E : Type u_2} {n : Type u_3} [NormedAddCommGroup E] [RCLike 𝕜] [NormedSpace 𝕜 E] (f : ContinuousBilinForm 𝕜 E) (b : Basis n 𝕜 E) [Fintype n] [DecidableEq n] (x y : n → 𝕜) :

x ⬝ᵥ (f.toMatrix b).mulVec y = (f (b.equivFun.symm x)) (b.equivFun.symm y)

source

theorem ContinuousBilinForm.apply_eq_dotProduct_toMatrix_mulVec {𝕜 : Type u_1} {E : Type u_2} {n : Type u_3} [NormedAddCommGroup E] [RCLike 𝕜] [NormedSpace 𝕜 E] (f : ContinuousBilinForm 𝕜 E) (b : Basis n 𝕜 E) [Fintype n] [DecidableEq n] (x y : E) :

(f x) y = ⇑(b.repr x) ⬝ᵥ (f.toMatrix b).mulVec ⇑(b.repr y)

source

noncomputable def ContinuousBilinForm.ofMatrix {𝕜 : Type u_1} {E : Type u_2} {n : Type u_3} [NormedAddCommGroup E] [RCLike 𝕜] [NormedSpace 𝕜 E] [Fintype n] [DecidableEq n] (M : Matrix n n 𝕜) (b : Basis n 𝕜 E) :

ContinuousBilinForm 𝕜 E

Equations

ContinuousBilinForm.ofMatrix M b = LinearMap.mkContinuous₂OfFiniteDimensional ((Matrix.toBilin b) M)

Instances For

source

theorem ContinuousBilinForm.ofMatrix_apply' {𝕜 : Type u_1} {E : Type u_2} {n : Type u_3} [NormedAddCommGroup E] [RCLike 𝕜] [NormedSpace 𝕜 E] [Fintype n] [DecidableEq n] (M : Matrix n n 𝕜) (b : Basis n 𝕜 E) (x y : E) :

((ofMatrix M b) x) y = (((Matrix.toBilin b) M) x) y

source

theorem ContinuousBilinForm.ofMatrix_apply {𝕜 : Type u_1} {E : Type u_2} {n : Type u_3} [NormedAddCommGroup E] [RCLike 𝕜] [NormedSpace 𝕜 E] [Fintype n] [DecidableEq n] (M : Matrix n n 𝕜) (b : Basis n 𝕜 E) (x y : E) :

((ofMatrix M b) x) y = ⇑(b.repr x) ⬝ᵥ M.mulVec ⇑(b.repr y)

source

theorem ContinuousBilinForm.ofMatrix_basis {𝕜 : Type u_1} {E : Type u_2} {n : Type u_3} [NormedAddCommGroup E] [RCLike 𝕜] [NormedSpace 𝕜 E] [Fintype n] [DecidableEq n] (M : Matrix n n 𝕜) (b : Basis n 𝕜 E) (i j : n) :

((ofMatrix M b) (b i)) (b j) = M i j

source

theorem ContinuousBilinForm.ofMatrix_orthonormalBasis {𝕜 : Type u_1} {n : Type u_3} [RCLike 𝕜] [Fintype n] [DecidableEq n] (M : Matrix n n 𝕜) {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (b : OrthonormalBasis n 𝕜 E) (i j : n) :

((ofMatrix M b.toBasis) (b i)) (b j) = M i j

source

theorem ContinuousBilinForm.toMatrix_ofMatrix {𝕜 : Type u_1} {E : Type u_2} {n : Type u_3} [NormedAddCommGroup E] [RCLike 𝕜] [NormedSpace 𝕜 E] (f : ContinuousBilinForm 𝕜 E) [Fintype n] [DecidableEq n] (b : Basis n 𝕜 E) :

ofMatrix (f.toMatrix b) b = f

source

theorem ContinuousBilinForm.ofMatrix_toMatrix {𝕜 : Type u_1} {E : Type u_2} {n : Type u_3} [NormedAddCommGroup E] [RCLike 𝕜] [NormedSpace 𝕜 E] [Fintype n] [DecidableEq n] (M : Matrix n n 𝕜) (b : Basis n 𝕜 E) :

(ofMatrix M b).toMatrix b = M

source

structure ContinuousBilinForm.IsPos {𝕜 : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [RCLike 𝕜] [NormedSpace 𝕜 E] (f : ContinuousBilinForm 𝕜 E) :

Prop

A continuous bilinear map f is positive if for any 0 ≤ x, 0 ≤ re (f x x)

nonneg_re_apply_self (x : E) : 0 ≤ RCLike.re ((f x) x)

Instances For

source

theorem ContinuousBilinForm.isPos_def {𝕜 : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [RCLike 𝕜] [NormedSpace 𝕜 E] (f : ContinuousBilinForm 𝕜 E) :

f.IsPos ↔ ∀ (x : E), 0 ≤ RCLike.re ((f x) x)

source

theorem ContinuousBilinForm.isPos_def_real {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ContinuousBilinForm ℝ E) :

f.IsPos ↔ ∀ (x : E), 0 ≤ (f x) x

source

theorem ContinuousBilinForm.IsPos.nonneg_apply_self {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ContinuousBilinForm ℝ E} (hf : f.IsPos) (x : E) :

0 ≤ (f x) x

source

theorem ContinuousBilinForm.isSymm_iff_isHermitian_toMatrix {n : Type u_3} {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ContinuousBilinForm ℝ E) (b : Basis n ℝ E) [Fintype n] [DecidableEq n] :

f.IsSymm ↔ (f.toMatrix b).IsHermitian

source

structure ContinuousBilinForm.IsPosSemidef {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ContinuousBilinForm ℝ E) extends f.IsSymm, f.IsPos :

Prop

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.