Inner product space on Hᵐᵒᵖ

This file defines the inner product space structure on Hᵐᵒᵖ where we define the inner product naturally. We also define OrthonormalBasis.mulOpposite.

@[instance_reducible]

instance MulOpposite.instInner {𝕜 : Type u_1} {H : Type u_2} [Inner 𝕜 H] : Inner 𝕜 Hᵐᵒᵖ

The inner product of Hᵐᵒᵖ is given by ⟪x, y⟫ ↦ ⟪x.unop, y.unop⟫.

Equations

• MulOpposite.instInner = { inner := fun (x y : Hᵐᵒᵖ) => inner 𝕜 (MulOpposite.unop x) (MulOpposite.unop y) }

@[simp]

theorem MulOpposite.inner_unop {𝕜 : Type u_1} {H : Type u_2} [Inner 𝕜 H] (x y : Hᵐᵒᵖ) : inner 𝕜 (unop x) (unop y) = inner 𝕜 x y

@[simp]

theorem MulOpposite.inner_op {𝕜 : Type u_1} {H : Type u_2} [Inner 𝕜 H] (x y : H) : inner 𝕜 (op x) (op y) = inner 𝕜 x y

@[instance_reducible]

instance MulOpposite.instInnerProductSpace {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup H] [InnerProductSpace 𝕜 H] : InnerProductSpace 𝕜 Hᵐᵒᵖ

Equations

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

theorem Module.Basis.mulOpposite_is_orthonormal_iff {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup H] [InnerProductSpace 𝕜 H] {ι : Type u_3} (b : Basis ι 𝕜 H) : Orthonormal 𝕜 ⇑b.mulOpposite ↔ Orthonormal 𝕜 ⇑b

noncomputable def OrthonormalBasis.mulOpposite {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_3} {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [Fintype ι] (b : OrthonormalBasis ι 𝕜 H) : OrthonormalBasis ι 𝕜 Hᵐᵒᵖ

The multiplicative opposite of an orthonormal basis b, i.e., b i ↦ op (b i).

Equations

• b.mulOpposite = b.toBasis.mulOpposite.toOrthonormalBasis ⋯

@[simp]

theorem OrthonormalBasis.toBasis_mulOpposite {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_3} {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [Fintype ι] (b : OrthonormalBasis ι 𝕜 H) : b.mulOpposite.toBasis = b.toBasis.mulOpposite