A median, and a power-mean inequality

Two elementary facts with no cube in them:

• exists_median — a real function on a nonempty finite type has a median m: at least half of the points have f ≤ m, and at least half have m ≤ f (Lemma 7.8 of the paper);
• sum_sq_cube_le — (∑ z²)^3 ≤ #s · (∑ |z|^3)^2, that is, (E z²)^3 ≤ (E |z|^3)^2 (Lemma 7.9 of the paper).

theorem AaronsonAmbainis.Level.exists_median {X : Type u_1} [Fintype X] [Nonempty X] (f : X → ℝ) : ∃ (m : ℝ), Fintype.card X ≤ 2 * {x : X | f x ≤ m}.card ∧ Fintype.card X ≤ 2 * {x : X | m ≤ f x}.card

A real function on a nonempty finite type has a median (Lemma 7.8 of the paper).

theorem AaronsonAmbainis.Level.sum_sq_cube_le {α : Type u_1} (s : Finset α) (z : α → ℝ) : (∑ i ∈ s, z i ^ 2) ^ 3 ≤ ↑s.card * (∑ i ∈ s, |z i| ^ 3) ^ 2

A power-mean inequality: (∑ z²)^3 ≤ #s · (∑ |z|^3)^2 (Lemma 7.9 of the paper).