# Continuous bilinear forms #

source
@[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

source
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 : Module.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 : Module.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 : Module.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 : Module.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 : Module.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 : Module.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 : Module.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 : Module.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 : Module.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 : Module.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 : Module.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 : Module.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 : Module.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.

- map_symm (x y : E) : (f x) y = (f y) x
- nonneg_re_apply_self (x : E) : 0 ≤ RCLike.re ((f x) x)

Instances For

source
theorem ContinuousBilinForm.IsPosSemidef.isSymm {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ContinuousBilinForm ℝ E} (hf : f.IsPosSemidef) :
f.IsSymm
source
theorem ContinuousBilinForm.IsPosSemidef.isPos {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ContinuousBilinForm ℝ E} (hf : f.IsPosSemidef) :
f.IsPos
source
theorem ContinuousBilinForm.isPosSemidef_iff {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ContinuousBilinForm ℝ E) :
f.IsPosSemidef ↔ f.IsSymm ∧ f.IsPos
source
theorem ContinuousBilinForm.isPosSemidef_iff_posSemidef_toMatrix {E : Type u_2} {n : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ContinuousBilinForm ℝ E} (b : Module.Basis n ℝ E) [Fintype n] [DecidableEq n] :
f.IsPosSemidef ↔ (f.toMatrix b).PosSemidef
source
noncomputable def ContinuousBilinForm.inner (E : Type u_2) [NormedAddCommGroup E] [InnerProductSpace ℝ E] :
ContinuousBilinForm ℝ E

The inner product as continuous bilinear form.

Equations

- ContinuousBilinForm.inner E = (LinearMap.mk₂ ℝ (fun (x y : E) => inner ℝ x y) ⋯ ⋯ ⋯ ⋯).mkContinuous₂ 1 ⋯

Instances For

source
@[simp]
theorem ContinuousBilinForm.inner_apply {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x y : E) :
((ContinuousBilinForm.inner E) x) y = inner ℝ x y
source
theorem ContinuousBilinForm.inner_apply' {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x : E) :
⇑((ContinuousBilinForm.inner E) x) = fun (y : E) => inner ℝ x y
source
theorem ContinuousBilinForm.inner_apply'' {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x : E) :
⇑((ContinuousBilinForm.inner E) x) = inner ℝ x
source
theorem ContinuousBilinForm.isPosSemidef_inner {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] :
(ContinuousBilinForm.inner E).IsPosSemidef
source
theorem ContinuousBilinForm.inner_toMatrix_eq_one {E : Type u_2} {n : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fintype n] [DecidableEq n] (b : OrthonormalBasis n ℝ E) :
(ContinuousBilinForm.inner E).toMatrix b.toBasis = 1
source
noncomputable def ContinuousBilinForm.diagonalStrongDual {𝕜 : Type u_1} {ι : Type u_4} [DecidableEq ι] [Fintype ι] {E : ι → Type u_5} [(i : ι) → NormedAddCommGroup (E i)] [RCLike 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] (L : (i : ι) → ContinuousBilinForm 𝕜 (StrongDual 𝕜 (E i))) :
ContinuousBilinForm 𝕜 (StrongDual 𝕜 ((i : ι) → E i))

Given `L i : (E i)' × (E i)' → 𝕜` a family of continuous bilinear forms, `diagonalStrongDual L` is a continuous bilinear form is the continuous bilinear form over `(Π i, E i)'` which maps `(x, y) : (Π i, E i)' × (Π i, E i)'` to `∑ i, L i (fun a ↦ x aᵢ) (fun a ↦ y aᵢ)`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
theorem ContinuousBilinForm.diagonalStrongDual_apply {𝕜 : Type u_1} {ι : Type u_4} [DecidableEq ι] [Fintype ι] {E : ι → Type u_5} [(i : ι) → NormedAddCommGroup (E i)] [RCLike 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] (L : (i : ι) → ContinuousBilinForm 𝕜 (StrongDual 𝕜 (E i))) (x y : StrongDual 𝕜 ((i : ι) → E i)) :
((diagonalStrongDual L) x) y = ∑ i : ι, ((L i) (ContinuousLinearMap.comp x (ContinuousLinearMap.single 𝕜 E i))) (ContinuousLinearMap.comp y (ContinuousLinearMap.single 𝕜 E i))
source
theorem ContinuousBilinForm.isPosSemidef_diagonalStrongDual {ι : Type u_4} [DecidableEq ι] [Fintype ι] {E : ι → Type u_5} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace ℝ (E i)] {L : (i : ι) → ContinuousBilinForm ℝ (StrongDual ℝ (E i))} (hL : ∀ (i : ι), (L i).IsPosSemidef) :
(diagonalStrongDual L).IsPosSemidef