nonempty spectrum

Stream: maths

[Jireh Loreaux]

I am working my way towards proving that the spectrum of an element in a Banach algebra over ℂ is nonempty. The standard argument uses the fact that resolvent function is analytic, and if it were entire, then by Liouville's theorem it would be constant (and by limiting arguments it would be zero), which is a contradiction. Therefore the resolvent set is not equal to ℂ, and hence the spectrum is nonempty. We don't have Liouville's theorem yet, right? How close are we to this? How might I help contribute to this?

[Scott Morrison]

I think, unfortunately, still a long way. @Yury G. Kudryashov is the person to answer where help would be useful.

[Eric Rodriguez]

one day we'll have complex integrals :pray:

[Scott Morrison]

https://math.stackexchange.com/a/2334921/28 points to a proof that uses no complex analysis! It doesn't look to be super hard to formalise, but it's unclear if it's worth the detour.

[Heather Macbeth]

@Jireh Loreaux I wrote a file on the Rayleigh quotient last month which basically gives us this result in one special case (compact self-adjoint operators on a Hilbert space): see docs#is_self_adjoint.has_eigenvector_of_is_max_on

[Yury G. Kudryashov]

Once we have #10000 merged, proving Liouville thm is easy. I'll try to make #10000 ready for review tonight.

[Jireh Loreaux]

@Scott Morrison fascinating. I had never seen that proof before, but it seems like it won't be necessary.

[Scott Morrison]

Nor me. I like that you can "still see why it only works over C, not R", through the essential dependence on the algebraic behaviour of roots of unity, rather than through analytic behaviour.

[Yury G. Kudryashov]

I went to bed earlier than I expected. I'll have some time tonight.

[Jireh Loreaux]

@Yury G. Kudryashov, thanks, but I'm in no big rush, so don't feel pressured on my account to get it done. I still have a few things to do before I get there. I was just surveying the landscape.

[Jireh Loreaux]

@Frédéric Dupuis, just FYI, I am starting a file on the spectrum in Banach algebras, in normed_space. I'll have a small PR in a few days to get us started.

[Jireh Loreaux]

@Frédéric Dupuis and @Heather Macbeth, when you get the chance, maybe have a look at #10476 and #10530. I probably need some help in computing the derivative of the resolvent function. I had to do some gross calc stuff and I bet there is an easier way, but I'm not sure what it is. We should be pretty much ready to show that the spectrum is nonempty once we have Liouville's theorem. After that, we should be able to prove the Gelfand-Mazur theorem, which is the basis for Gelfand theory.

[Heather Macbeth]

Reviewed!

[Frédéric Dupuis]

I just had a look as well -- I didn't have much to add over Heather's comments, it looks good!

[Jireh Loreaux]

@Heather Macbeth, you mentioned using ⨆ k ∈ spectrum 𝕜 a, ∥k∥, which is supr instead of Sup, and admittedly the notation is much nicer, and yes, they seem to be almost the same thing. But I'm confused about something.

#check @supr
-- supr : Π {α : Type u_1} [_inst_1 : has_Sup α] {ι : Sort u_2}, (ι → α) → α
#print @spectral_radius
/-
noncomputable def spectral_radius : Π (𝕜 : Type u_1) {A : Type u_2}
 [_inst_1 : normed_field 𝕜] [_inst_2 : ring A] [_inst_3 : algebra 𝕜 A],
  A → ℝ :=
λ (𝕜 : Type u_1) {A : Type u_2} [_inst_1 : normed_field 𝕜] [_inst_2 : ring A]
[_inst_3 : algebra 𝕜 A] (a : A),
  ⨆ (k : 𝕜) (H : k ∈ spectrum 𝕜 a), ∥k∥
-/

I can't seem to unify (in my head) the application of ⨆ in #print @spectral_radius with the type of supr. Namely, what is the index type ι in @spectral_radius? Is it the subtype { x : 𝕜 // x ∈ spectrum 𝕜 a} and the definition you provided is just syntactic sugar for this, or am I missing something entirely?

[Heather Macbeth]

@Jireh Loreaux Excellent question, I don't know :) The notation is defined here:

notation `⨆` binders `, ` r:(scoped f, supr f) := r

but I don't understand that. Maybe someone else can give a layperson's explanation?

[Yakov Pechersky]

binders is syntax for something like i or (i : ι) or (i : ι) (h : 0 < i). r:(scoped f, supr f) means that a function is defined in that local scope, with access to the arguments given in binders, and that that whole function f is provided to supr. That given the binders, supr f, is what the whole notation means. That's my understanding.

[Reid Barton]

There are two applications of supr corresponding to the two binders k and H

[Reid Barton]

You can set pp.notation false and then #print again

[Heather Macbeth]

If I understand correctly,

 ⨆ (k : 𝕜) (H : k ∈ spectrum 𝕜 a), ∥k∥

is taking nested suprs. Firstly for each k : 𝕜 we take a supr with index type k ∈ spectrum 𝕜 a, then we take a supr with index type 𝕜.

[Jireh Loreaux]

Yes, this makes sense now. Thanks all.

[Jireh Loreaux]

Okay, after thinking about it further, I've confused myself again, but possibly for a different reason. What is the value of ⨆ (r : ℝ) (hr : r ≤ -1), r? I think it should be 0, but that would mean the notation is very confusing. I'll explain my reasoning. This is defeq to supr (λ (r : ℝ), supr (λ (hr : r ≤ -1), r)) which itself unfolds to: supr (λ (r : ℝ), Sup (set.range (λ (hr : r ≤ -1), r))). Now, when r ≤ -1, we should have set.range (λ (hr : r ≤ -1), r) = {r} since the type r ≤ -1 is inhabited, and then Sup (set.range (λ (hr : r ≤ -1), r)) = Sup {r} = r. But for r > -1, we should have set.range (λ (hr : r ≤ -1), r) = ∅ since the type r ≤ -1 is uninhabited, and hence Sup (set.range (λ (hr : r ≤ -1), r)) = Sup ∅ = 0 (the latter being the definition of Sup on ℝ). Thus, wouldn't the outer supremum then be 0?

[Reid Barton]

Oh yeah, this kind of notation is only good if you have something like a complete lattice where supr always makes sense

[Jireh Loreaux]

Okay, at least I understand what's going on. In this case, even though we are working over ℝ, I think it might be okay because our function takes nonnegative values, so nothing gets screwed up. @Heather Macbeth, what do you think?

[Heather Macbeth]

Jireh Loreaux said:

In this case, even though we are working over ℝ, I think it might be okay because our function takes nonnegative values, so nothing gets screwed up.

I agree with this point. I'll leave it up to you whether to use the notation or not!

[Heather Macbeth]

By the way, I should have mentioned that there's another trove of lemmas about supr in "conditionally complete lattices" (such as ℝ) in
https://leanprover-community.github.io/mathlib_docs/order/conditionally_complete_lattice.html
Keyword here is csupr.

[Jireh Loreaux]

Thanks, yes, I found that.

[Heather Macbeth]

Oh, one other option is to let the spectral radius be of type docs#nnreal (nonnegative real) rather than ℝ. This (in fact, with docs#ennreal) is what is done for the radius of convergence of a power series, which is somewhat analogous: docs#formal_multilinear_series.radius

[Jireh Loreaux]

That seems like it might be the best decision. I'll use ⨆ k ∈ spectrum 𝕜 a, ∥k∥₊

[Jireh Loreaux]

I think I've made all the changes, I replied to some of the conversations and then marked them as resolved. @Frédéric Dupuis, I gave reasons for ennreal, and @Heather Macbeth, you should look at the reasons too, because they are even more significant than we realized last night (namely, the spectrum can be unbounded, just not in a Banach algebra; but the algebra can even be "complete" relative to another topology, like convergence in measure).

[Jireh Loreaux]

also, should I request that someone in algebra reviews the other PR #10476? I don't know what the standard protocol is, and I would prefer not to start out by stepping on toes or pushing people's buttons. If there is documentation about this kind of thing, then I managed to miss it.

[Scott Morrison]

It's completely fine to prompt people for reviews on PRs if a few days have passed without progress. Usually best is to open a topic in #PR reviews stream (you may not be subscribed yet). Just saying "This PR is ready for review, does XYZ, and I've followed the suggestions made by A" will be enough to remind people to go have a look at it!