theorem BooleanFourier.low_degree_concentration_hypercontractive {n : ℕ} (f : (Fin n → Bool) → ℝ) (d : ℕ) (hdeg : degree f ≤ d) : 1 / 2 ^ n * ∑ x : Fin n → Bool, f x ^ 4 ≤ 9 ^ d * (1 / 2 ^ n * ∑ x : Fin n → Bool, f x ^ 2) ^ 2