English
Auxiliary lemma: under a condition H about supports, (x * single m r) at m1 equals x(m2) · r for suitable m1,m2; this assists convolution computations.
Русский
Вспомогательная лемма: при условии H о опорах, (x * single m r) в m1 равно x(m2) · r для подходящих m1,m2; служит для вычислений свёртки.
LaTeX
$$$\bigl( x * \operatorname{single}(m,r) \bigr)_{m_1} = x(m_2) \cdot r$ под условием $H$$$
Lean4
@[to_additive (dont_translate := R) mul_single_apply_aux]
theorem mul_single_apply_aux (H : ∀ m' ∈ x.support, m' * m = m₁ ↔ m' = m₂) : (x * single m r) m₁ = x m₂ * r := by
classical
calc
(x * single m r) m₁
_ = x.sum fun m' r' ↦ if m' * m = m₁ then r' * r else 0 := by simp [mul_apply]
_ = x.sum fun m' r' ↦ if m' = m₂ then r' * r else 0 := by dsimp [Finsupp.sum]; congr! 2; simp [*]
_ = x m₂ * r := by simp +contextual [Finsupp.sum_eq_single m₂]
