spectral theorem for normal endomorphisms and related pain

Stream: maths

[Jireh Loreaux]

I've been thinking about giving someone a short project over the summer to establish the spectral theorem for normal endomorphisms over a finite dimensional inner product space.

In outlining the work, I ran into several problems that are not present for the spectral theorem for symmetric operators.

1. We have a definition of symmetric operators that can be used for both LinearMap and ContinuousLinearMap (since the latter has a coercion to the former), and the type class assumptions are minimal. This is useful.
2. One cannot do a similar thing for normal endomorphisms, because one must reference the adjoint (or star, whichever), but there are no common type class assumptions giving the user access to that (e.g., for E →ₗ[𝕜] E we need FiniteDimensional 𝕜 E, but for E →L[𝕜] E we need CompleteSpace E).
3. As an example of the problems caused by (2), consider that the following statement is true for linear maps on a finite dimensional space as well, but we would need to duplicate the proof.

lemma adjoint_apply_eq_zero_iff {𝕜 E : Type*} [RCLike 𝕜] [NormedAddCommGroup E]
    [InnerProductSpace 𝕜 E] [CompleteSpace E] (f : E →L[𝕜] E) [IsStarNormal f] (x : E) :
    adjoint f x = 0 ↔ f x = 0 :=
  sorry

4. In fact, all the results at the beginning of file#Analysis/InnerProductSpace/Spectrum (except the one that says eigenvalues are real) generalize to normal endomorphisms. BUT, we would need them in triplicate: one for symmetric linear maps, one for normal continuous linear maps on a complete space, and one for normal linear maps on a finite dimensional space ... gross.
5. Moreover, there's really nothing about (4) which needs separate assumptions other than the existence of a suitable adjoint.

I'm happy to solicit solutions to these sorts of problems. One idea I considered was to have a LinearAdjoint class which supplies an adjoint for the appropriate space of endomorphisms. Some downsides: it's subject to the same problems as all of our hom classes: we can't talk about identity maps or composition. A draft implementation:

LinearAdjoint

import Mathlib

section AdjointClass

class LinearAdjoint (𝕜 E F : outParam Type*) (H₁ : Type*) (H₂ : outParam Type*) [RCLike 𝕜]
    [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F]
    [FunLike H₁ E F] [LinearMapClass H₁ 𝕜 E F] [FunLike H₂ F E] [LinearMapClass H₂ 𝕜 F E]
    [AddCommGroup H₁] [Module 𝕜 H₁] [AddCommGroup H₂] [Module 𝕜 H₂] where
  adjoint : H₁ ≃ₗ⋆[𝕜] H₂
  is_adjoint (f : H₁) (x : E) (y : F) : ⟪adjoint f y, x⟫_𝕜 = ⟪y, f x⟫_𝕜

noncomputable instance LinearMap.instLinearAdjoint {𝕜 E F : Type*} [RCLike 𝕜]
    [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E]
    [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] :
    LinearAdjoint 𝕜 E F (E →ₗ[𝕜] F) (F →ₗ[𝕜] E) where
  adjoint := LinearMap.adjoint
  is_adjoint f x y := LinearMap.adjoint_inner_left f x y

noncomputable instance ContinuousLinearMap.instLinearAdjoint {𝕜 E F : Type*} [RCLike 𝕜]
    [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E]
    [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] :
    LinearAdjoint 𝕜 E F (E →L[𝕜] F) (F →L[𝕜] E) where
  adjoint := ContinuousLinearMap.adjoint.toLinearEquiv
  is_adjoint f x y := ContinuousLinearMap.adjoint_inner_left f x y

export LinearAdjoint (adjoint)

namespace LinearAdjoint

scoped[LinearAdjoint] postfix:max "†" => adjoint

variable {𝕜 E F H₁ H₂ :Type*} [RCLike 𝕜]
    [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F]
    [FunLike H₁ E F] [LinearMapClass H₁ 𝕜 E F] [FunLike H₂ F E] [LinearMapClass H₂ 𝕜 F E]
    [AddCommGroup H₁] [Module 𝕜 H₁] [AddCommGroup H₂] [Module 𝕜 H₂]
    [LinearAdjoint 𝕜 E F H₁ H₂] [LinearAdjoint 𝕜 F E H₂ H₁]

/-- The fundamental property of the adjoint. -/
theorem adjoint_inner_left (A : H₁) (x : E) (y : F) : ⟪A† y, x⟫_𝕜 = ⟪y, A x⟫_𝕜 :=
  is_adjoint A x y

/-- The fundamental property of the adjoint. -/
theorem adjoint_inner_right (A : H₁) (x : E) (y : F) : ⟪x, A† y⟫_𝕜 = ⟪A x, y⟫_𝕜 := by
  rw [← inner_conj_symm, adjoint_inner_left, inner_conj_symm]

/-- The adjoint is involutive. -/
@[simp]
theorem adjoint_adjoint (A : H₁) : A†† = A :=
  DFunLike.ext _ _ fun x ↦ ext_inner_left 𝕜 fun y ↦ by rw [adjoint_inner_right, adjoint_inner_left]

open RCLike

theorem apply_norm_sq_eq_inner_adjoint_left (A : H₁) (x : E) :
    ‖A x‖ ^ 2 = re ⟪A† (A x), x⟫_𝕜 := by
  rw [adjoint_inner_left, ← inner_self_eq_norm_sq (𝕜 := 𝕜) _]

theorem apply_norm_eq_sqrt_inner_adjoint_left (A : H₁) (x : E) :
    ‖A x‖ = √(re ⟪A† (A x), x⟫_𝕜) := by
  rw [← apply_norm_sq_eq_inner_adjoint_left, Real.sqrt_sq (norm_nonneg _)]

theorem apply_norm_sq_eq_inner_adjoint_right (A : H₁) (x : E) :
    ‖A x‖ ^ 2 = re ⟪x, A† (A x)⟫_𝕜 := by
  rw [adjoint_inner_right, ← inner_self_eq_norm_sq (𝕜 := 𝕜) _]

theorem apply_norm_eq_sqrt_inner_adjoint_right (A : H₁) (x : E) :
    ‖A x‖ = √(re ⟪x, A† (A x)⟫_𝕜) := by
  rw [← apply_norm_sq_eq_inner_adjoint_right, Real.sqrt_sq (norm_nonneg _)]

/-- The adjoint is unique: a map `A` is the adjoint of `B` iff it satisfies `⟪A x, y⟫ = ⟪x, B y⟫`
for all `x` and `y`. -/
theorem eq_adjoint_iff (A : H₁) (B : H₂) : A = B† ↔ ∀ x y, ⟪A x, y⟫_𝕜 = ⟪x, B y⟫_𝕜 := by
  refine' ⟨fun h x y => by rw [h, adjoint_inner_left], fun h => _⟩
  apply DFunLike.ext _ _ fun x ↦ ?_
  exact ext_inner_right 𝕜 fun y => by simp only [adjoint_inner_left, h x y]

end LinearAdjoint

variable {𝕜 E H : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
    [FunLike H E E] [LinearMapClass H 𝕜 E E] [AddCommGroup H] [Module 𝕜 H] [LinearAdjoint 𝕜 E E H H]

def LinearAdjoint.IsNormal (A : H) := ∀ x, adjoint A (A x) = A (adjoint A x)

namespace LinearAdjoint.IsNormal

lemma adjoint_self_apply_comm {A : H} (hA : IsNormal A) (x : E) :
    A† (A x) = A (A† x) :=
  hA x

lemma adjoint_apply_eq_zero_iff {f : H} (hf : IsNormal f) (x : E) :
    f† x = 0 ↔ f x = 0 := by
  rw [← norm_eq_zero , norm_eq_sqrt_inner (𝕜 := 𝕜), adjoint_inner_left,
    ← hf.adjoint_self_apply_comm, adjoint_inner_right, ← norm_eq_sqrt_inner, norm_eq_zero]

Of course, this doesn't help with LinearPMap at all, but right now I consider it hopeless to unify that too.

[Jireh Loreaux]

The idea would be that LinearAdjoint.adjoint (or just adjoint if we export it) would become the default spelling of both the existing LinearMap.adjoint and ContinuousLinearMap.adjoint. Of course, we would still need docs#ContinuousLinearMap.adjoint since that's also isometric, but we would try to avoid using it in statements.

Even with this proposed class, there still doesn't seem to be a way to unify the symmetric and normal versions of the results at the top of file#LinearAlgebra/InnerProductSpace/Spectrum, because the normal versions will still require additional type class assumptions.

[Frédéric Dupuis]

Wouldn't it be enough to have a prop typeclass IsReasonableStar (or something :-) ) that contains the properties of star that we need for all of this?

[Jireh Loreaux]

No, you need the interaction with the inner product.

[Frédéric Dupuis]

Can't that be baked in? i.e. having an inner product is a necessary prerequisite for IsReasonableStar, along with the properties.

[Jireh Loreaux]

I suppose.

[Jireh Loreaux]

Another possible solution is to define the collection of adjointable operators, and define an adjoint operation on those. In the case of complete spaces or finite dimensional spaces, every operator is adjointable.

[Jireh Loreaux]

The IsReasonableStar approach still doesn't allow you to unify the IsStarNormal results with the IsSymmetric, because the former needs IsReasonableStar, but the IsSymmetric results hold even in the presence of an unreasonable star. I think this is acceptable though, and I prefer the approach to not create new data.

[Frédéric Dupuis]

Yeah, I'm not very enthusiastic at the prospect of creating a second version of star...

[Jireh Loreaux]

Even IsReasonableStar (which I called StarAdjoint) seems doomed to failure. In order for it to be useful, we would have to know that all the operations on this type with a LinearMapClass instance occur pointwise. For example:

class StarAdjoint (𝕜 E : outParam Type*) (H : Type*) [RCLike 𝕜] [NormedAddCommGroup E]
    [InnerProductSpace 𝕜 E] [Ring H] [Module 𝕜 H] [StarRing H] [FunLike H E E]
    [LinearMapClass H 𝕜 E E] : Prop where
  star_is_adjoint (f : H) (x y : E) : ⟪star f y, x⟫_𝕜 = ⟪y, f x⟫_𝕜
  mul_apply (f g : H) (x : E) : (f * g) x = f (g x)

But we would also need the add_apply, sub_apply, etc. as well.

[Jireh Loreaux]

This is also a problem with my proposed LinearAdjoint class too, I just hadn't realized it yet.

[Jireh Loreaux]

I'm leaning towards just accepting the triplicated theorems.

[Frédéric Dupuis]

Is it so bad to have the add_apply and friends?

[Jireh Loreaux]

It makes me feel like I'm doing it wrong. And I suspect I'm just going to keep running into other issues. Maybe I'm wrong.

[Frédéric Dupuis]

Hard to tell without really trying it I guess.

[Jireh Loreaux]

There's also the issue that all the eigenspace and related material is about docs#Module.End, which means that all my statements involving this generic StarAdjoint type (H in the code above) would have to be coerced to a linear map in the statements.

[Jireh Loreaux]

Admittedly, that's a problem for ContinuousLinearMap too. :shrug:

[Yaël Dillies]

Is that related to !3#16351 ?

[Jireh Loreaux]

you mean the pointwise action stuff? Maybe a bit, but I'm not entirely sure how to make any of the proposed solutions there work here (aside from just copying the *_apply fields into the class).

[Yaël Dillies]

Yeah, is that an unreasonable solution?

[Jireh Loreaux]

As I said above, it made me feel like I was doing things wrong, because I just kept needing to add things to say "this really is a linear map, please treat it as such". But maybe these are the only facts I need.

[Antoine Chambert-Loir]

Eigenspaces should be defined for LinearMapClass, shouldn't they?

[Frédéric Dupuis]

Antoine Chambert-Loir said:

Eigenspaces should be defined for LinearMapClass, shouldn't they?

This has been on my todo list since forever!

[Antoine Chambert-Loir]

Suggestion: this kind of stuff should be added to the relevant file, in hope that somebody finds the courage to do it, with some specific enough format that one can gather them automatically to one big informative Todo list.

[Jireh Loreaux]

Frédéric Dupuis said:

Antoine Chambert-Loir said:

Eigenspaces should be defined for LinearMapClass, shouldn't they?

This has been on my todo list since forever!

I think there are two problems with doing this:

1. You have the issue that has come up with other FunLike things of this kind: The eigenvalues / eigenvectors of some element of a LinearMapClass are not defeq to those of it's coercion to a linear map. If you have some lemmas to show they are the same, then it's not so bad, but it is a bit of an annoyance.
2. More importantly, there's no LinearMap.id for elements in a LinearMapClass, which gets pretty annoying when you want to work with f x = μ x and you want to write it like (f - μ • LinearMap.id) x = 0. Even (f - algebraMap 𝕜 F μ) x = 0 is probably not valid for most LinearMapClasses F, and you would still need to apply it to x.

[Jireh Loreaux]

You can do (↑f - μ • LinearMap.id) x = 0 but then you're back to coercing.

[Frédéric Dupuis]

Sure, there are some downsides, but surely this can't be worse than having to coerce all the time when talking about continuous linear maps!

[Eric Wieser]

Jireh Loreaux said:

Even IsReasonableStar (which I called StarAdjoint) seems doomed to failure. In order for it to be useful, we would have to know that all the operations on this type with a LinearMapClass instance occur pointwise. For example:

class StarAdjoint (𝕜 E : outParam Type*) (H : Type*) [RCLike 𝕜] [NormedAddCommGroup E]
    [InnerProductSpace 𝕜 E] [Ring H] [Module 𝕜 H] [StarRing H] [FunLike H E E]
    [LinearMapClass H 𝕜 E E] : Prop where
  star_is_adjoint (f : H) (x y : E) : ⟪star f y, x⟫_𝕜 = ⟪y, f x⟫_𝕜
  mul_apply (f g : H) (x : E) : (f * g) x = f (g x)

But we would also need the add_apply, sub_apply, etc. as well.

Does AddMonoidHomClass deal with the add and sub lemmas?

[Jireh Loreaux]

No, AddMonoidHomClass H E E would tell you that for any f : H and any x y : E, that f (x + y) = f x + f y, but it's not going to tell you that for any f g : H and any x : E, that (f + g) x = f x + g x.

[Antoine Chambert-Loir]

Isn't it a way to add id to all these classes (when possible), and turning them into kind of categories?

[Jireh Loreaux]

Did you mean "Does there exist a way ..."? Not currently. The issue is composition. Given HomClass F X Y, HomClass G Y Z Lean has trouble inferring the ?H in HomClass ?H X Z.

[Jireh Loreaux]

Indeed, a single F could imply many more HomClasses between X and Y.

[Jireh Loreaux]

There's this issue #2202