MeasureTheory.dLpNorm_translate_sum_sub_le

lemma dLpNorm_translate_sum_sub_le [NormedAddCommGroup E] (hp : 1 ≤ p) {ι : Type*} (s : Finset ι)    (a : ι → G) (f : G → E) : ‖τ (∑ i ∈ s, a i) f - f‖_[p] ≤ ∑ i ∈ s, ‖τ (a i) f - f‖_[p] := by  induction s using Finset.cons_induction with  | empty => simp  | cons i s ih hs =>  calc    _ = ‖τ (∑ j ∈ s, a j) (τ (a i) f - f) + (τ (∑ j ∈ s, a j) f - f)‖_[p] := by      rw [sum_cons, translate_add', translate_sub_right, sub_add_sub_cancel]    _ ≤ ‖τ (∑ j ∈ s, a j) (τ (a i) f - f)‖_[p] + ∑ j ∈ s, ‖(τ (a j) f - f)‖_[p] := by      grw [dLpNorm_add_le hp, hs]    _ = _ := by rw [dLpNorm_translate, sum_cons]