Add

@[fun_prop]lemma add {d : ℕ} {f g : Space d → F}    (hf : IsDistBounded f) (hg : IsDistBounded g) : IsDistBounded (f + g) := by  rcases hf with ⟨hae1, ⟨n1, c1, g1, p1, c1_nonneg, p1_bound, bound1⟩⟩  rcases hg with ⟨hae2, ⟨n2, c2, g2, p2, c2_nonneg, p2_bound, bound2⟩⟩  refine ⟨by fun_prop, n1 + n2, Fin.append c1 c2, Fin.append g1 g2, Fin.append p1 p2, ?_, ?_, ?_⟩  · intro i    induction i using Fin.addCases with    | left i => simpa using c1_nonneg i    | right i => simpa using c2_nonneg i  · intro i    induction i using Fin.addCases with    | left i => simpa using p1_bound i    | right i => simpa using p2_bound i  · intro x    refine ((norm_add_le _ _).trans (add_le_add (bound1 x) (bound2 x))).trans_eq ?_    simp [Fin.sum_univ_add]