pi_eq_sum_univ for finsupp

Stream: Is there code for X?

[Yaël Dillies]

Is there any equivalent to docs#pi_eq_sum_univ but for docs#finsupp? I guess it could be called finsupp.eq_sum_smul_single, or similar.

[Eric Wieser]

I'd expect the statement to not include a smul

[Eric Wieser]

Something like ∑ x in f.support, single x (f x) = f is the statement I'd expect

[Yaël Dillies]

Interesting...

[Yaël Dillies]

While I'm there, do we not have an equivalent of docs#finset.single_le_sum, and instances pseudo_metric_space (ι →₀ ℝ), topological_space (ι →₀ ℝ) and similar?

[Yaël Dillies]

Are those even sensemaking? In my mind, ι →₀ α behaves basically like ι → α. But maybe I'm topologically wrong.

[Eric Wieser]

docs#finsupp.sum_single is the statement

[Eric Wieser]

Which is defeq to the version I gave above

[Yaël Dillies]

Thanks! This is the lemma I wanted:

lemma finsupp.linear_combi_single_eq {α M : Type*} [semiring M] (f : α →₀ M) :
  f.sum (λ a b, f a • finsupp.single a (1 : M)) = f :=
begin
  simp_rw [finsupp.smul_single, smul_eq_mul, mul_one],
  exact f.sum_single,
end

[Yaël Dillies]

Name suggestions are welcome.

[Eric Wieser]

(deleted)

[Eric Wieser]

Is there anything special about finsupp.single a 1 that makes that useful?

[Yaël Dillies]

Yes, it matches docs#finset.center_mass_eq_of_sum_1

[Eric Wieser]

Also I think you should have b instead of f a there

[Eric Wieser]

Because the whole point in finsupp.sum f g is that g gets called as g a (f a)

[Yaël Dillies]

Hmm... What's that point, actually?

[Yaël Dillies]

Note that I'm redefining docs#std_simplex in terms of docs#finsupp and that I use this lemma at the interface with the non-finsupp land of docs#finset.center_mass. Eventually, finset.center_mass will take in finsupps and maybe that weirdness will disappear?

[Yaël Dillies]

The branch is branch#std_simplex_finsupp. This will be of interest to @Yury G. Kudryashov.

[Yaël Dillies]

(I feel like I'm hitting a wall of bricks, so help is more than welcome!)

[Rémy Degenne]

I think that Eric is suggesting that you lemma should prove f.sum (λ a b, b • finsupp.single a (1 : M)) = f (note the b instead of f a) since f.sum g is the sum over a of g a (f a).

[Yaël Dillies]

Yes yes, I got that and I changed it. What I do not get is why we have g a (f a) in the first place, and not just g a.

[Yaël Dillies]

Ah, is it because we have many lemmas that assume h a 0 = 0, or similar?

[Rémy Degenne]

you are looking for something that uses only the support of f and not its values then? You want to sum g over the support of f

[Rémy Degenne]

with only g a and not g a (f a) it sounds more like a finset affair than finsupp

[Yaël Dillies]

Well, I can ad hoc define g' := λ a, g a (f a). That's using the values of f.

[Rémy Degenne]

indeed, as you did in the code above. That's right.

[Rémy Degenne]

I am not very familiar with finsupp, so I don't have much to add to that :)

[Rémy Degenne]

the lemma docs#finsupp.sum_add_index looks like a good reason for wanting the g a b version (for some applications)