## Stream: maths

### Topic: Linear algebra

#### 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!

imports?

#### Mario Carneiro (Nov 04 2019 at 22:35):

import apache

#### 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

#### 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

#### 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


#### Miguel Raz Guzmán Macedo (Nov 14 2019 at 03:58):

@Kevin Buzzard I believe Terence Tao is unwittingly giving Lean a shoutout...