NNReal rpow sum le sum

lemma NNReal.rpow_sum_le_sum {p : ℝ} (hp : 1 ≤ p) :    ∀ n : ℕ, 1 ≤ n → ∀ a : Fin n → ℝ≥0,    Real.rpow (∑ i : Fin n, Real.rpow (a i : ℝ) p) (1 / p) ≤ ∑ i : Fin n, (a i : ℝ) := by  intro n hn a  have hp0 : p ≠ 0 := by linarith  induction n, hn using Nat.le_induction with  | base =>    simp only [Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton]    show ((a 0 : ℝ) ^ p) ^ (1 / p) ≤ (a 0 : ℝ)    rw [← Real.rpow_mul (NNReal.coe_nonneg _), mul_one_div, div_self hp0, Real.rpow_one]  | succ n hn ih =>    rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc]    set A := ∑ i : Fin n, (a i.castSucc : ℝ) ^ p    set B := (a (Fin.last n) : ℝ)    have hA : 0 ≤ A := Finset.sum_nonneg fun i _ => Real.rpow_nonneg (NNReal.coe_nonneg _) _    have hB : 0 ≤ B := NNReal.coe_nonneg _    have hApow : (A ^ (1 / p)) ^ p = A := by      rw [← Real.rpow_mul hA, one_div, inv_mul_cancel₀ hp0, Real.rpow_one]    have hsub : (A + B ^ p) ^ (1 / p) ≤ A ^ (1 / p) + B := by      have h := Real.rpow_add_rpow_le_add (Real.rpow_nonneg hA (1 / p)) hB hp      rwa [hApow] at h    calc (A + B ^ p) ^ (1 / p)        ≤ A ^ (1 / p) + B := hsub      _ ≤ ∑ i : Fin n, (a i.castSucc : ℝ) + B :=          add_le_add_left            (show A ^ (1 / p) ≤ ∑ i : Fin n, (a i.castSucc : ℝ) from ih (a ∘ Fin.castSucc)) _