English
The difference between evaluating f at a and at a piecewise-altered b is the sum over i in s of f applied to a perturbation pattern.
Русский
Разность значений f на a и на заменённом b по подмножеству s равна сумме по i∈s отпаттернов, применяемых к a и b.
LaTeX
$$f(a) - f(s.piecewise(b,a)) = sum_{i in s} f( … ),$$
Lean4
theorem map_sub_map_piecewise [LinearOrder ι] (a b : (i : ι) → M₁ i) (s : Finset ι) :
f a - f (s.piecewise b a) = ∑ i ∈ s, f (fun j ↦ if j ∈ s → j < i then a j else if i = j then a j - b j else b j) :=
by
refine s.induction_on_min ?_ fun k s hk ih ↦ ?_
· rw [Finset.piecewise_empty, sum_empty, sub_self]
rw [Finset.piecewise_insert, map_update, ← sub_add, ih, add_comm, sum_insert (lt_irrefl _ <| hk k ·)]
simp_rw [s.mem_insert]
congr 1
· congr; ext i; split_ifs with h₁ h₂
· rw [update_of_ne, Finset.piecewise_eq_of_notMem]
· exact fun h ↦ (hk i h).not_gt (h₁ <| .inr h)
· exact fun h ↦ (h₁ <| .inl h).ne h
· cases h₂
rw [update_self, s.piecewise_eq_of_notMem _ _ (lt_irrefl _ <| hk k ·)]
· push_neg at h₁
rw [update_of_ne (Ne.symm h₂), s.piecewise_eq_of_mem _ _ (h₁.1.resolve_left <| Ne.symm h₂)]
· apply sum_congr rfl
grind
