Linear algebra

Stream: maths

[Sebastien Gouezel]

I need some bits of linear algebra, and I am really struggling. I had forgotten how hard it is to use a part of the library you are not familiar with! Anyway, I am sure everything is already there to get the following statement, but whenever I start with something I begin to unfold and unfold and I am sure I shouldn't (and I guess I am not even writing it in the correct way).

open_locale classical
lemma linear_map.pi_apply_eq {ι : Type u} [fintype ι] {𝕜 : Type u} [discrete_field 𝕜]
  {E : Type v} [add_comm_group E] [vector_space 𝕜 E] (f : (ι → 𝕜) →ₗ[𝕜] E) (x : ι → 𝕜) :
  f x = finset.sum finset.univ (λi:ι, x i • (f (λj, if j = i then 1 else 0))) :=
sorry

Between constr_self (pi.is_basis_fun 𝕜 ι) f or linear_map.std_basis, I don't know where to start!

[Mario Carneiro]

imports?

[Reid Barton]

No, start with a copyright header

[Mario Carneiro]

import apache

[Reid Barton]

More seriously, I think you should first use linearity of f to reduce to the same statement without f

[Reid Barton]

Then I don't know whether it is an existing lemma. It does seem to be std_basis-related somehow. Anyways, it doesn't look very difficult to prove using sum_mul_boole for example

[Sebastien Gouezel]

I ended up doing the following, avoiding completely the linear algebra basis framework, which is a little bit sad. I would be very happy to see the proper way to write it, possibly replacing λj, if i = j then 1 else 0 by something more idiomatic. Imports and header included :) Thanks for the reference to sum_mul_boole.

/- Nice Zulip header -/

import linear_algebra.finite_dimensional

universes u v w
open_locale classical

lemma pi_eq_sum_univ {ι : Type u} [fintype ι] {𝕜 : Type v} [ring 𝕜]
  (x : ι → 𝕜) : x = finset.sum finset.univ (λi:ι, x i • (λj, if i = j then 1 else 0)) :=
begin
  ext k,
  rw pi.finset_sum_apply,
  have : finset.sum finset.univ (λ (x_1 : ι), x x_1 * ite (k = x_1) 1 0) = x k,
  { have := finset.sum_mul_boole finset.univ x k,
    rwa if_pos (finset.mem_univ _) at this },
  rw ← this,
  apply finset.sum_congr rfl (λl hl, _),
  simp only [smul_eq_mul, mul_ite, pi.smul_apply],
  conv_lhs { rw eq_comm },
end

set_option class.instance_max_depth 36

lemma linear_map.pi_apply_eq_sum_univ {ι : Type u} [fintype ι] {𝕜 : Type v} [discrete_field 𝕜]
  {E : Type w} [add_comm_group E] [vector_space 𝕜 E] (f : (ι → 𝕜) →ₗ[𝕜] E) (x : ι → 𝕜) :
  f x = finset.sum finset.univ (λi:ι, x i • (f (λj, if i = j then 1 else 0))) :=
begin
  conv_lhs { rw [pi_eq_sum_univ x, f.map_sum] },
  apply finset.sum_congr rfl (λl hl, _),
  rw f.map_smul
end

[Miguel Raz Guzmán Macedo]

@Kevin Buzzard I believe Terence Tao is unwittingly giving Lean a shoutout...
https://twitter.com/InertialObservr/status/1194826080005148672

Apparently an equivalent result has been used/discovered before, but as Terry Tao states it was never published. ... oops https://twitter.com/InertialObservr/status/1194826080005148672/photo/1

- 〈 Berger | Dillon 〉 (@InertialObservr)

[Johan Commelin]

More specifically, I guess you are referring to the following comment by Tao on his blog: https://terrytao.wordpress.com/2019/08/13/eigenvectors-from-eigenvalues/#comment-528704 where he writes:

(It’s at times like this that I wish we had a good semantic search engine for mathematics – I am not sure how I would have discovered this preprint other than by publishing our own preprint and waiting for someone to notice the connection.)

[Miguel Raz Guzmán Macedo]

Yup that same one @Johan Commelin

[Ruizhe Wan]

For a finite dimensional normed vector space $V$, we could define a linear map from the dual $V*$ to V itself by choosing a specific basis, and this map induce a topology on $V*$. The topology should not depend on the chosen basis so it is canonical. I wonder if there is any theorem in lean that says about this topology in $V*$?

[Kyle Miller]

The dual itself is a normed space: docs#normed_space.dual

After a quick look, I didn't see anything about finite dimensional normed spaces beyond docs#normed_space.dual.finite_dimensional (that the dual is finite dimensional).

Do you have any particular application for the theorem you're talking about @Ruizhe Wan? If I'm not mistaken, there ought to be a stronger statement that any two finite dimensional normed vector spaces of equal dimension over the same normed field are isometric (at least in characteristic zero).

[Ruizhe Wan]

I am considering defining the dual vector bundle of a finite dimensional vector bundle, and first I need to define the topology on the dual vector bundle by defining a map from the dual vector bundle to the vector bundle, and then induce from it the topology. But to define the map I need to choose a specific basis. And I want to show the induced topology is independent of the basis chosen.

[Eric Wieser]

@Ruizhe Wan, can you edit your comment above to use $$V*$$ instead of V*? The asterisks are turning into italics and being lost.

[Junyan Xu]

You can use docs#linear_equiv.to_continuous_linear_equiv, but I think there should be a way to show directly that the topologies on the dual vector spaces are compatible on overlaps of charts if the original vector spaces are, in a basis-free way that generalizes to infinite-dimensional case.
(see also thread 1, thread 2)