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 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 MulOpposite.instInnerProductSpace {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup 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 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] {ι : Type u_3} (b : Basis ι 𝕜 H) : Orthonormal 𝕜 ⇑b.mulOpposite ↔ Orthonormal 𝕜 ⇑b

noncomputable def OrthonormalBasis.mulOpposite {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] {ι : Type u_3} [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 ⋯

theorem MulOpposite.isometry_opLinearEquiv {R : Type u_3} {M : Type u_4} [Semiring R] [SeminormedAddCommGroup M] [Module R M] : Isometry ⇑(opLinearEquiv R)

def MulOpposite.opLinearIsometryEquiv (𝕜 : Type u_1) (H : Type u_2) [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] : H ≃ₗᵢ[𝕜] Hᵐᵒᵖ

The linear isometry equivalence version of the function op.

Equations

• MulOpposite.opLinearIsometryEquiv 𝕜 H = { toLinearEquiv := MulOpposite.opLinearEquiv 𝕜, norm_map' := ⋯ }

@[simp]

theorem MulOpposite.opLinearIsometryEquiv_apply (𝕜 : Type u_1) (H : Type u_2) [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (a✝ : H) : (opLinearIsometryEquiv 𝕜 H) a✝ = op a✝

@[simp]

theorem MulOpposite.opLinearIsometryEquiv_symm_apply (𝕜 : Type u_1) (H : Type u_2) [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (a✝ : Hᵐᵒᵖ) : (opLinearIsometryEquiv 𝕜 H).symm a✝ = unop a✝

@[simp]

theorem MulOpposite.toLinearEquiv_opLinearIsometryEquiv {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] : (opLinearIsometryEquiv 𝕜 H).toLinearEquiv = opLinearEquiv 𝕜

@[simp]

theorem MulOpposite.toContinuousLinearEquiv_opLinearIsometryEquiv {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] : (opLinearIsometryEquiv 𝕜 H).toContinuousLinearEquiv = opContinuousLinearEquiv 𝕜