Complex numbers sums

Stream: new members

[Gabriel Moise]

Hello! I was playing with some sums over real and complex numbers, but I got stuck at the following:

import data.real.basic
import data.complex.basic

open_locale big_operators

universe u
variables {V : Type u} [fintype V] [decidable_eq V]
variables (r : V → ℝ) (c : V → ℂ)

lemma test_lemma : ∑ i : V, (c i * r i) = ∑ i : V, (r i * c i) :=
begin
  have key : ∀ i : V, (c i * r i) = (r i * c i),
  {intro i, exact mul_comm (c i) ↑(r i)},
  simp[key],
end

def test_real : ℝ := ∑ i : V, r i
def test_complex : ℂ := ∑ i : V, c i -- definition 'test_complex' is noncomputable, it depends on 'complex.field'

def sum_elems (c : V → ℂ) := ∑ i : V, c i -- same

def product_elems : ℂ := ∑ j : V, c j * r j -- same

I was trying to create a function that would do a "dot_product" between a real and a complex vector, but I got an error, and apparently I can't have a definition that, given a complex vector, returns the sum of its elements. The explanation I see is that the part where we prove that the set of complex numbers is a field is noncomputable, but from what I saw (correct me if I'm wrong), this is also the case for the set of real numbers. However, for real numbers everything is fine. Additionally, I could work in a lemma with the sum I wanted to obtain (and I tested it on a simple lemma to see how it behaves) without any complains. What should I do?

[Anne Baanen]

Quick answer: you can put noncomputable theory after the imports, then Lean will stop warning you about noncomputability.

[Anne Baanen]

You need to warn that a def is noncomputable because normally, Lean produces executable code for a def. For lemmas, it only checks that the lemma proof has the type of the lemma statement.

[Anne Baanen]

The reason why it happens to work for reals and not for complex numbers is kind of technical: in principle both test_real and test_complex should be computable, since addition, subtraction and multiplication of real numbers are computable, so are the equivalent operations for complex numbers: there is a computable comm_ring ℝ structure in mathlib (called docs#real.comm_ring). But for complex numbers, there is only a field ℂ structure available, docs#complex.field, and mathlib's division operator is not computable for real or complex numbers. This noncomputability also "infects" the add_comm_monoid ℂ structure used by the summation over V, making it noncomputable too.

[Gabriel Moise]

But if I want to continue working with the sum_elems and product_elems definitons, is it ok to make them noncomputable and then carry on using them?

[Anne Baanen]

Yes, there should be no problem marking them noncomputable.

[Gabriel Moise]

Ultimately, I am trying to work with the eigenvalues of a real-valued matrix, and since they can be complex, my plan is to define eigenvectors as complex and this would imply a (real)matrix-(complex)vector multiplication operation. I don't know if this is a good approach, but might get more experience from it.

[Anne Baanen]

That sounds like a good start if you are doing the project to practice. If you want to contribute to mathlib, be sure to check out docs#module.End.has_eigenvector as well, so you don't do too much duplicate work :)

[Gabriel Moise]

I consulted that as well, but it seems a little too complicated for me at the moment, as I am not a very experienced mathematician :( . I don't really see how to apply the definition

def eigenspace (f : End R M) (μ : R) : submodule R M :=
(f - algebra_map R (End R M) μ).ker

to my case with f being a matrix (linear transformation) with coefficients in ℝ and μ a complex value. So that's why I wanted to make something more restricted (even though I am using noncomputable to every definition I create :laughing: ), but obviously the best way would be to use the already existing model and build from it.

[Yakov Pechersky]

You can interpret the real matrix as being in C, then the types match up

[Yakov Pechersky]

Would you rather work with matrix ... or linear_map?

[Gabriel Moise]

I am not sure what would be the best option. I already have some work with matrices and I wanted to develop that more with some eigenvalue properties, so that's why I wanted to work with matrices. Can I juggle between them easily/efficiently?

[Yakov Pechersky]

docs#matrix.to_lin' and docs#linear_map.to_matrix'

[Yakov Pechersky]

So easy interconversion retaining the linear structure

[Yakov Pechersky]

And you can use a coe that is a linear_map to express your linear map on R as a linear map on C

[Gabriel Moise]

Thank you! I'll see how I can work with those!

[Yakov Pechersky]

I'm sure somewhere in mathlib we have the linear_map, or even linear_isometry of the embedding of R into C

[Yakov Pechersky]

Then you get your End C C iiuc

[Gabriel Moise]

How would a lemma like "Eigenvalues of a symmetric real matrix are real" be stated using linear maps then?

[Yakov Pechersky]

for all mu such that End.has_eigenvalue (real_to_complex f) mu, mu.im = 0 or something more neat

[Gabriel Moise]

And where does the symmetry come into place?

[Yakov Pechersky]

Well, it's a constraint on what f you provide

[Yakov Pechersky]

If you're working on End, you might use linear_equiv

[Gabriel Moise]

I see, and btw if I have a noncomputable definition test_def, I can't have a command "unfold test_def" I suppose, right?

[Yakov Pechersky]

Yes, you can. noncomputable just means that no VM code is generated for that defn

[Eric Wieser]

(deleted)

[Eric Wieser]

Anne Baanen said:

But for complex numbers, there is only a field ℂ structure available, docs#complex.field,

Citation needed: docs#complex.comm_ring

[Eric Wieser]

It sounds like the action problem is that docs#complex.add_comm_monoid is missing

[Gabriel Moise]

Is there a way to prove that :

lemma sum_complex_re (x : V → ℂ) : (∑ i : V, x i).re = ∑ i : V, (x i).re

I was thinking about using the "add_re" lemma, but I don't see how.

[Eric Wieser]

Previously that would be linear_map.re.map_sum

[Eric Wieser]

But I think docs#linear_map.re got renamed

[Eric Wieser]

docs#complex.re_lm?

[Gabriel Moise]

And how can it be used for the sum?

[Ruben Van de Velde]

You'd need docs#linear_map.map_sum with re_lm as f

[Eric Wieser]

complex.re_lm.map_sum I think is the proof of your lemma

[Gabriel Moise]

Found it, it was linear_map.re.map_sum, thanks!

[Eric Wieser]

Sounds like you're on an old mathlib

[Kevin Buzzard]

There's no such thing as a symmetric linear map -- this is a predicate on matrices, ie it depends on the choice of basis

[Yakov Pechersky]

You can still phrase this about linear_maps in a round-about way via matrix.to_lin, which does require two explicit bases

[Gabriel Moise]

Is there a lemma which states that the sum of nonnegative (real) numbers is 0 iff all the numbers are 0?

[Yakov Pechersky]

That's a lemma about a constant function

[Yakov Pechersky]

docs#finset.sum_const_zero

[Ruben Van de Velde]

That's only one direction of the iff, surely

[Yakov Pechersky]

Or docs#finset.sum_subset

[Gabriel Moise]

Yeah, I am more interested in the => direction. (sum = 0 => numbers are 0)

[Yakov Pechersky]

I don't think the iff is stated anywhere obvious because nonnegative numbers isn't a type.

[Yakov Pechersky]

Unless you're working on nnreal

[Yakov Pechersky]

Or it is, but I can't guess the name at the moment

[Ruben Van de Velde]

docs#finset.sum_eq_zero_iff_of_nonneg ?

[Gabriel Moise]

This one looks helpful

[Ruben Van de Velde]

docs#finset.sum_eq_zero_iff seems to work on nnreal

[Gabriel Moise]

Is there a lemma which states that a polynomial of degree n (with real coefficients) has n (complex) roots?

[Anne Baanen]

Probably the easiest: combine docs#polynomial.degree_eq_card_roots and docs#complex.is_alg_closed, via docs#is_alg_closed.splits

[Gabriel Moise]

And the homomorphism should be from C to C? I am a little confused about the "splits" part

[Johan Commelin]

@Gabriel Moise in general a polynomial only split over a some larger field extension.

[Johan Commelin]

So you have to give the ring hom that describes this extension.

[Johan Commelin]

But that last lemma that Anne linked to shows that id : C -> C will work, because C is alg. closed (2nd link).

[Anne Baanen]

Since your coefficients are real, the specific ring hom will be algebra_map ℝ ℂ.

[Johan Commelin]

Good point, I forgot the actual question :face_palm:

[Anne Baanen]

Hmm, you'll have to do some rewriting (composing algebra_map ℝ ℂ with the identity) to get this to work. Should we define is_alg_closed.splits : ∀ {R S} (f : R →+* S) (p : polynomial R), p.splits f instead?

[Anne Baanen]

That is: keep the definition of is_alg_closed, rename is_alg_closed.splits to is_alg_closed.splits' and add this as a better eliminator.

[Johan Commelin]

@Anne Baanen yes, that seems very reasonable

[Johan Commelin]

Where I assume S is your preferred letter for algebraically closed fields :grinning:

[Anne Baanen]

Ah nevermind, that is literally the next definition docs#polynomial.splits' :P

[Anne Baanen]

Wait no, there f goes in the opposite direction.

[Johan Commelin]

Lol... I guess we want both

[Anne Baanen]

I don't want to call them polynomial.splits' and polynomial.splits'', how about is_alg_closed.splits_domain (the domain of f is alg closed) and is_alg_closed.splits_codomain (the codomain of f is alg closed)?

[Gabriel Moise]

I am a little stuck with these two now:

lemma help_split (P : polynomial ℝ) : splits (algebra_map ℝ ℂ) P := sorry

lemma help_algebra_map (P : polynomial ℝ) : multiset.card (map (algebra_map ℝ ℂ) P).roots = multiset.card P.roots := sorry

[Kevin Buzzard]

I would imagine that multiset.card P.roots is just the roots of P in the reals, so that second one might not be true for something like x^2+1 right?

[Gabriel Moise]

Oh, I see, then this approach doesn't work then?

lemma help_split (P : polynomial ℝ) : splits (algebra_map ℝ ℂ) P := sorry

lemma degree_n_poly_has_n_roots (P : polynomial ℝ) (H_P : P ≠ 0) : P.degree = P.roots.card :=
begin
  let i : ℝ →+* ℂ := algebra_map ℝ ℂ,
  have hsplit : splits i P, {exact help_split P},
  rw degree_eq_card_roots H_P hsplit,
  -- Goal : ↑(⇑multiset.card (map i P).roots) = ↑(⇑multiset.card P.roots)
  sorry,
end

[Anne Baanen]

Question 1:

lemma help_split (P : polynomial ℝ) : splits (algebra_map ℝ ℂ) P :=
by { rw [← (algebra_map ℝ ℂ).id_comp, ← splits_map_iff],
     exact is_alg_closed.splits (P.map (algebra_map ℝ ℂ)) }

(soon it will just be := is_alg_closed.splits_codomain _ _).

[Anne Baanen]

Indeed, degree_n_poly_has_n_roots as is stated now is not true, because P.roots does not include any complex roots.

[Anne Baanen]

PR created: #7187

[Gabriel Moise]

I see, thank you very much for the clarifications!

[Gabriel Moise]

But if I modify P to be a polynomial over C, the degree_n_poly_has_n_roots would be correct, though I don't know how to continue with that:

lemma degree_n_poly_has_n_roots (P : polynomial ℂ) (H_P : P ≠ 0) : P.degree = P.roots.card :=
begin
  let i : ℂ →+* ℂ := algebra_map ℂ ℂ,
  have hsplit : splits i P, {exact help_split P},
  rw degree_eq_card_roots H_P hsplit,
  -- Goal : ↑(⇑multiset.card (map i P).roots) = ↑(⇑multiset.card P.roots)
  sorry,
end

[Kevin Buzzard]

Does refl solve it?

[Johan Commelin]

dsimp [i], simp [map_id] hopefully.

[Eric Wieser]

The original computability problem at the top of this thread will be solved by #8166