Working with finite sums of SchwartzMaps

Stream: new members

[Gregory Loges]

I am struggling to manipulate finite sums of Schwartz maps. Consider the following simple examples:

import Mathlib.Analysis.Distribution.SchwartzSpace
open SchwartzMap

example (f : Fin n → ℝ → ℂ): (∑ i, f i) x = ∑ i, f i x := Fintype.sum_apply _ _

example (f : Fin n → ℝ →L[ℝ] ℂ): (∑ i, f i) x = ∑ i, f i x := ContinuousLinearMap.sum_apply _ _ _

example (f : Fin n → 𝓢(ℝ, ℂ)): (∑ i, f i) x = ∑ i, f i x := by sorry

The .sum_apply type theorems don't seem to help in the last case. Any help would be appreciated!

[Yongxi Lin (Aaron)]

try simp only [sum_apply]

[Yongxi Lin (Aaron)]

SchwartzMap.sum_apply

[Gregory Loges]

I get simp made no progress... Am I missing some import, perhaps?

[Yongxi Lin (Aaron)]

It is working on live.lean-lang.org, so I am not sure what happend on your side.

[Moritz Doll]

You are probably on a too old version of mathlib given that you import the deprecated Distribution.SchwartzSpace not Distribution.SchwartzSpace.Basic

[Moritz Doll]

The lemma Aaron mentioned was included rather recently

[Gregory Loges]

Thanks, problem solved!