Documentation

Mathlib.Analysis.InnerProductSpace.MulOpposite

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.

source
@[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
source
@[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
source
@[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
source
@[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.
source
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
source
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
Instances For
    source
    @[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