English
A more explicit form of the previous identity expresses the same difference with a finite sum over the index set.
Русский
Более явная форма предыдущего тождества выражает ту же разницу через конечную сумму.
LaTeX
$$$$f(s.piecewise(a,v)) - f(s.piecewise(b,v)) = \sum_{i} f(…);$$$$
Lean4
/-- This calculates the differences between the values of a multilinear map at
two arguments that differ on a finset `s` of `ι`. It requires a
linear order on `ι` in order to express the result. -/
theorem map_piecewise_sub_map_piecewise [LinearOrder ι] (a b v : (i : ι) → M₁ i) (s : Finset ι) :
f (s.piecewise a v) - f (s.piecewise b v) =
∑ i ∈ s, f fun j ↦ if j ∈ s then if j < i then a j else if j = i then a j - b j else b j else v j :=
by
rw [← s.piecewise_idem_right b a, map_sub_map_piecewise]
refine Finset.sum_congr rfl fun i hi ↦ congr_arg f <| funext fun j ↦ ?_
by_cases hjs : j ∈ s
· rw [if_pos hjs]; by_cases hji : j < i
· rw [if_pos fun _ ↦ hji, if_pos hji, s.piecewise_eq_of_mem _ _ hjs]
rw [if_neg (Classical.not_imp.mpr ⟨hjs, hji⟩), if_neg hji]
obtain rfl | hij := eq_or_ne i j
· rw [if_pos rfl, if_pos rfl, s.piecewise_eq_of_mem _ _ hi]
· rw [if_neg hij, if_neg hij.symm]
· rw [if_neg hjs, if_pos fun h ↦ (hjs h).elim, s.piecewise_eq_of_notMem _ _ hjs]
