Raising absolute values to powers

Stream: Is there code for X?

[Adam Topaz]

Does anyone know of a simple way to prove the following?

import analysis.special_functions.pow

open_locale big_operators

example
  (ι : Type*) [fintype ι] (a : ι → ℝ) (p : ℝ)
  (h1 : 0 ≤ p) (h2 : p ≤ 1) :
  | ∑ i, a i |^p ≤ ∑ i, | a i |^p := sorry

I'm fairly flexible with the spelling... for example, I'm happy to use nnnorm or norm instead of the absolute value, etc.

More generally, does mathlib know that raising an absolute value to a real power $p$ with $0 \le p \le 1$ gives another absolute value?

[Yaël Dillies]

docs#finset.le_sum_of_subadditive

[Adam Topaz]

That's a start...

[Adam Topaz]

the api seach comes up empty with pow subadditive

[Yaël Dillies]

Surely that would rather be pow_add_le?

[Adam Topaz]

ha we have docs#nnreal.rpow_add_le_add_rpow

[Adam Topaz]

(contrary to the assumption there, it's also true for p = 0 ;)

[Eric Rodriguez]

(got bored and fixed that #15823)

[Johan Commelin]

Adam Topaz said:

More generally, does mathlib know that raising an absolute value to a real power $p$ with $0 \le p \le 1$ gives another absolute value?

LTE knows that you can rescale has_p_norm (or whatever it is called) like that.