Wkp U deriv ELp Norm add le

lemma WkpU.derivELpNorm_add_le {d : ℕ+} {k : ℕ} {p : ℝ≥0∞}    {U : Set (Fin d → ℝ)} {hU : IsOpen U} (hp1 : 1 ≤ p)    (f g : WkpU d k p U hU) (n : ℕ) (s : Fin n → Fin d) :    WkpU.derivELpNorm (f + g) n s ≤      WkpU.derivELpNorm f n s + WkpU.derivELpNorm g n s := by  match n with  | 0 =>    simp only [WkpU.derivELpNorm]    have hcoe : ((f + g).val : (Fin d → ℝ) → ℝ)        =ᵐ[μU d U]        (f.val : (Fin d → ℝ) → ℝ) + (g.val : (Fin d → ℝ) → ℝ) :=      AEEqFun.coeFn_add f.val.1 g.val.1    rw [eLpNorm_congr_ae hcoe]    exact eLpNorm_add_le      (WkpU.aestronglyMeasurable f)      (WkpU.aestronglyMeasurable g) hp1  | n + 1 =>    simp only [WkpU.derivELpNorm]    split_ifs with hn    · set nm : ℕ+ := ⟨n + 1, Nat.succ_pos n⟩      obtain ⟨_, eq_add⟩ := WeakmultiDerivU_add U hU s f.val g.val        (WkpU.hasWeakDeriv f nm hn s) (WkpU.hasWeakDeriv g nm hn s)      have heq :          (WkpU.weakDeriv (f + g) nm hn s : (Fin d → ℝ) → ℝ)          =ᵐ[μU d U]          (WkpU.weakDeriv f nm hn s : (Fin d → ℝ) → ℝ)            + (WkpU.weakDeriv g nm hn s : (Fin d → ℝ) → ℝ) :=        eq_add.trans (AEEqFun.coeFn_add _ _)      rw [eLpNorm_congr_ae heq]      exact eLpNorm_add_le        (WkpU.weakDeriv_memLp f nm hn s).aestronglyMeasurable        (WkpU.weakDeriv_memLp g nm hn s).aestronglyMeasurable hp1    · exact le_self_add