Zulip Chat Archive

Stream: maths

Topic: Linear algebra


view this post on Zulip Sebastien Gouezel (Nov 04 2019 at 22:09):

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!

view this post on Zulip Mario Carneiro (Nov 04 2019 at 22:32):

imports?

view this post on Zulip Reid Barton (Nov 04 2019 at 22:34):

No, start with a copyright header

view this post on Zulip Mario Carneiro (Nov 04 2019 at 22:35):

import apache

view this post on Zulip Reid Barton (Nov 04 2019 at 22:38):

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

view this post on Zulip Reid Barton (Nov 04 2019 at 22:45):

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

view this post on Zulip Sebastien Gouezel (Nov 05 2019 at 10:46):

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

view this post on Zulip Miguel Raz Guzmán Macedo (Nov 14 2019 at 03:58):

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

view this post on Zulip Johan Commelin (Nov 14 2019 at 05:05):

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.)

view this post on Zulip Miguel Raz Guzmán Macedo (Nov 14 2019 at 20:59):

Yup that same one @Johan Commelin


Last updated: May 14 2021 at 19:21 UTC