noncomputable def GaussianHypercontractivity.stdGaussianMeasure (n : ℕ) : MeasureTheory.Measure (Fin n → ℝ)

noncomputable def GaussianHypercontractivity.gaussianLpNorm (n : ℕ) (p : ℝ) (f : (Fin n → ℝ) → ℝ) : ℝ

noncomputable def GaussianHypercontractivity.hermiteEval (k : ℕ) (x : ℝ) : ℝ

noncomputable def GaussianHypercontractivity.multiHermiteEval (n : ℕ) (α : Fin n → ℕ) (x : Fin n → ℝ) : ℝ

def GaussianHypercontractivity.HasGaussianDegreeAtMost (n d : ℕ) (f : (Fin n → ℝ) → ℝ) : Prop

theorem GaussianHypercontractivity.gaussian_hypercontractivity (n d : ℕ) (q : ℝ) (hq : 2 ≤ q) (f : (Fin n → ℝ) → ℝ) (hf_meas : Measurable f) (hf_deg : HasGaussianDegreeAtMost n d f) : gaussianLpNorm n q f ≤ (q - 1) ^ (↑d / 2) * gaussianLpNorm n 2 f