Coordinatewise conjugation in an orthonormal basis

There is no canonical conjugation on an abstract inner product space, so this file attaches one to an orthonormal basis e by conjugating the coordinates in it: conjugation e x = ∑ i, conj ⟪e i, x⟫ • e i. It is a conjugate-linear isometric involution of V (TauCeti.conjugation_conjugation, TauCeti.inner_conjugation_conjugation), and conjugating an operator by it, A ↦ J ∘ A ∘ J (TauCeti.conjCLM), is the coordinate-free description of conjugating the matrix of A entrywise.

Main definitions

• TauCeti.conjugation: the conjugate-linear isometric involution attached to an orthonormal basis.
• TauCeti.conjCLM: conjugation of a continuous linear operator, A ↦ J ∘ A ∘ J.

Main statements

• TauCeti.conjugation_conjugation and TauCeti.inner_conjugation_conjugation: conjugation is an involution, and reverses the inner product.
• TauCeti.conjugation_basis: the basis it is attached to is fixed vector by vector, which is what makes it the conjugation of that basis.
• TauCeti.inner_conjugation_left_basis: pairing a conjugate against a basis vector swaps the two arguments of the inner product.
• TauCeti.conjCLM_one, TauCeti.conjCLM_mul and TauCeti.conjCLM_conjCLM: conjugation of operators is a multiplicative involution fixing the identity.
• TauCeti.conjCLM_add and TauCeti.conjCLM_smul: it is additive and conjugate-linear, so with the two preceding it is a conjugate-linear ring involution of the operators.
• TauCeti.norm_conjCLM: conjugation of operators preserves the operator norm.

noncomputable def TauCeti.conjugation {𝕜 : Type u_1} {ι : Type u_2} {V : Type u_3} [RCLike 𝕜] [Fintype ι] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (e : OrthonormalBasis ι 𝕜 V) (x : V) : V

Coordinatewise conjugation in an orthonormal basis. A conjugate-linear isometric involution of V, which on coordinates is x i ↦ conj (x i).

Equations

• TauCeti.conjugation e x = ∑ i : ι, (starRingEnd 𝕜) (inner 𝕜 (e i) x) • e i

theorem TauCeti.conjugation_apply {𝕜 : Type u_1} {ι : Type u_2} {V : Type u_3} [RCLike 𝕜] [Fintype ι] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (e : OrthonormalBasis ι 𝕜 V) (x : V) : conjugation e x = ∑ i : ι, (starRingEnd 𝕜) (inner 𝕜 (e i) x) • e i

Conjugation, expanded as the coordinate sum defining it.

@[simp]

theorem TauCeti.inner_conjugation {𝕜 : Type u_1} {ι : Type u_2} {V : Type u_3} [RCLike 𝕜] [Fintype ι] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (e : OrthonormalBasis ι 𝕜 V) (x : V) (j : ι) : inner 𝕜 (e j) (conjugation e x) = (starRingEnd 𝕜) (inner 𝕜 (e j) x)

The coordinates of a conjugate are the conjugated coordinates.

@[simp]

theorem TauCeti.conjugation_zero {𝕜 : Type u_1} {ι : Type u_2} {V : Type u_3} [RCLike 𝕜] [Fintype ι] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (e : OrthonormalBasis ι 𝕜 V) : conjugation e 0 = 0

Conjugation fixes the zero vector.

@[simp]

theorem TauCeti.conjugation_add {𝕜 : Type u_1} {ι : Type u_2} {V : Type u_3} [RCLike 𝕜] [Fintype ι] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (e : OrthonormalBasis ι 𝕜 V) (x y : V) : conjugation e (x + y) = conjugation e x + conjugation e y

Conjugation is additive.

@[simp]

theorem TauCeti.conjugation_smul {𝕜 : Type u_1} {ι : Type u_2} {V : Type u_3} [RCLike 𝕜] [Fintype ι] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (e : OrthonormalBasis ι 𝕜 V) (c : 𝕜) (x : V) : conjugation e (c • x) = (starRingEnd 𝕜) c • conjugation e x

Conjugation is conjugate-linear: a scalar comes out conjugated.

@[simp]

theorem TauCeti.conjugation_neg {𝕜 : Type u_1} {ι : Type u_2} {V : Type u_3} [RCLike 𝕜] [Fintype ι] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (e : OrthonormalBasis ι 𝕜 V) (x : V) : conjugation e (-x) = -conjugation e x

Conjugation commutes with negation.

@[simp]

theorem TauCeti.conjugation_sub {𝕜 : Type u_1} {ι : Type u_2} {V : Type u_3} [RCLike 𝕜] [Fintype ι] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (e : OrthonormalBasis ι 𝕜 V) (x y : V) : conjugation e (x - y) = conjugation e x - conjugation e y

Conjugation commutes with subtraction.

@[simp]

theorem TauCeti.conjugation_conjugation {𝕜 : Type u_1} {ι : Type u_2} {V : Type u_3} [RCLike 𝕜] [Fintype ι] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (e : OrthonormalBasis ι 𝕜 V) (x : V) : conjugation e (conjugation e x) = x

Conjugation is an involution.

@[simp]

theorem TauCeti.conjugation_basis {𝕜 : Type u_1} {ι : Type u_2} {V : Type u_3} [RCLike 𝕜] [Fintype ι] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (e : OrthonormalBasis ι 𝕜 V) (j : ι) : conjugation e (e j) = e j

Conjugation fixes the basis it is attached to. Coordinatewise conjugation is the identity on the vectors whose coordinates are 0 and 1.

@[simp]

theorem TauCeti.inner_conjugation_conjugation {𝕜 : Type u_1} {ι : Type u_2} {V : Type u_3} [RCLike 𝕜] [Fintype ι] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (e : OrthonormalBasis ι 𝕜 V) (x y : V) : inner 𝕜 (conjugation e x) (conjugation e y) = (starRingEnd 𝕜) (inner 𝕜 x y)

Conjugation reverses the inner product: it is conjugate-linear and isometric.

@[simp]

theorem TauCeti.inner_conjugation_left_basis {𝕜 : Type u_1} {ι : Type u_2} {V : Type u_3} [RCLike 𝕜] [Fintype ι] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (e : OrthonormalBasis ι 𝕜 V) (x : V) (j : ι) : inner 𝕜 (conjugation e x) (e j) = inner 𝕜 (e j) x

Pairing a conjugate against a basis vector swaps the arguments. Conjugation fixes e j, so the reversal of the inner product turns ⟪J x, e j⟫ into ⟪e j, x⟫. This is the form in which the conjugation is contracted against a coordinate.

@[simp]

theorem TauCeti.norm_conjugation {𝕜 : Type u_1} {ι : Type u_2} {V : Type u_3} [RCLike 𝕜] [Fintype ι] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (e : OrthonormalBasis ι 𝕜 V) (x : V) : ‖conjugation e x‖ = ‖x‖

Conjugation is isometric, as the reversal of the inner product shows on the diagonal.

noncomputable def TauCeti.conjCLM {𝕜 : Type u_1} {ι : Type u_2} {V : Type u_3} [RCLike 𝕜] [Fintype ι] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (e : OrthonormalBasis ι 𝕜 V) (A : V →L[𝕜] V) : V →L[𝕜] V

Conjugation of a continuous linear operator, A ↦ J ∘ A ∘ J for J the conjugation of e. The two conjugate-linearities of J cancel, so the result is 𝕜-linear, and it is bounded because J is isometric.

Equations

• TauCeti.conjCLM e A = { toFun := fun (x : V) => TauCeti.conjugation e (A (TauCeti.conjugation e x)), map_add' := ⋯, map_smul' := ⋯ }.mkContinuous ‖A‖ ⋯

@[simp]

theorem TauCeti.conjCLM_apply {𝕜 : Type u_1} {ι : Type u_2} {V : Type u_3} [RCLike 𝕜] [Fintype ι] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (e : OrthonormalBasis ι 𝕜 V) (A : V →L[𝕜] V) (x : V) : (conjCLM e A) x = conjugation e (A (conjugation e x))

Evaluation of a conjugated operator.

@[simp]

theorem TauCeti.conjCLM_one {𝕜 : Type u_1} {ι : Type u_2} {V : Type u_3} [RCLike 𝕜] [Fintype ι] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (e : OrthonormalBasis ι 𝕜 V) : conjCLM e 1 = 1

Conjugation fixes the identity, because J is an involution.

@[simp]

theorem TauCeti.conjCLM_mul {𝕜 : Type u_1} {ι : Type u_2} {V : Type u_3} [RCLike 𝕜] [Fintype ι] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (e : OrthonormalBasis ι 𝕜 V) (A B : V →L[𝕜] V) : conjCLM e (A * B) = conjCLM e A * conjCLM e B

Conjugation is multiplicative, again because J is an involution: the two inner copies of J cancel.

@[simp]

theorem TauCeti.conjCLM_conjCLM {𝕜 : Type u_1} {ι : Type u_2} {V : Type u_3} [RCLike 𝕜] [Fintype ι] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (e : OrthonormalBasis ι 𝕜 V) (A : V →L[𝕜] V) : conjCLM e (conjCLM e A) = A

Conjugation of operators is an involution, because J is.

@[simp]

theorem TauCeti.conjCLM_zero {𝕜 : Type u_1} {ι : Type u_2} {V : Type u_3} [RCLike 𝕜] [Fintype ι] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (e : OrthonormalBasis ι 𝕜 V) : conjCLM e 0 = 0

Conjugation kills the zero operator.

@[simp]

theorem TauCeti.conjCLM_add {𝕜 : Type u_1} {ι : Type u_2} {V : Type u_3} [RCLike 𝕜] [Fintype ι] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (e : OrthonormalBasis ι 𝕜 V) (A B : V →L[𝕜] V) : conjCLM e (A + B) = conjCLM e A + conjCLM e B

Conjugation of operators is additive.

@[simp]

theorem TauCeti.conjCLM_neg {𝕜 : Type u_1} {ι : Type u_2} {V : Type u_3} [RCLike 𝕜] [Fintype ι] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (e : OrthonormalBasis ι 𝕜 V) (A : V →L[𝕜] V) : conjCLM e (-A) = -conjCLM e A

Conjugation of operators commutes with negation.

@[simp]

theorem TauCeti.conjCLM_sub {𝕜 : Type u_1} {ι : Type u_2} {V : Type u_3} [RCLike 𝕜] [Fintype ι] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (e : OrthonormalBasis ι 𝕜 V) (A B : V →L[𝕜] V) : conjCLM e (A - B) = conjCLM e A - conjCLM e B

Conjugation commutes with subtraction of operators.

@[simp]

theorem TauCeti.conjCLM_smul {𝕜 : Type u_1} {ι : Type u_2} {V : Type u_3} [RCLike 𝕜] [Fintype ι] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (e : OrthonormalBasis ι 𝕜 V) (c : 𝕜) (A : V →L[𝕜] V) : conjCLM e (c • A) = star c • conjCLM e A

Conjugation of operators is conjugate-linear: a scalar of the operator passes through the outer J only, so it comes out conjugated.

theorem TauCeti.norm_conjCLM_le {𝕜 : Type u_1} {ι : Type u_2} {V : Type u_3} [RCLike 𝕜] [Fintype ι] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (e : OrthonormalBasis ι 𝕜 V) (A : V →L[𝕜] V) : ‖conjCLM e A‖ ≤ ‖A‖

Conjugation does not increase the operator norm.

@[simp]

theorem TauCeti.norm_conjCLM {𝕜 : Type u_1} {ι : Type u_2} {V : Type u_3} [RCLike 𝕜] [Fintype ι] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (e : OrthonormalBasis ι 𝕜 V) (A : V →L[𝕜] V) : ‖conjCLM e A‖ = ‖A‖

Conjugation preserves the operator norm: it does not increase it, and it is an involution.

theorem TauCeti.lipschitzWith_one_conjCLM {𝕜 : Type u_1} {ι : Type u_2} {V : Type u_3} [RCLike 𝕜] [Fintype ι] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (e : OrthonormalBasis ι 𝕜 V) : LipschitzWith 1 (conjCLM e)

Conjugation of operators is a contraction, hence continuous.