Rudin's inequality

theorem rudin_exp_ineq {G : Type u_1} [Fintype G] [AddCommGroup G] [MeasurableSpace G] [DiscreteMeasurableSpace G] (f : G → ℂ) (hf : AddDissociated (Function.support (cft f))) : (Finset.univ.expect fun (a : G) => Real.exp (f a).re) ≤ Real.exp (‖f‖ₙ_[2] ^ 2 / 2)

Rudin's inequality, exponential form.

theorem rudin_exp_abs_ineq {G : Type u_1} [Fintype G] [AddCommGroup G] [MeasurableSpace G] [DiscreteMeasurableSpace G] (f : G → ℂ) (hf : AddDissociated (Function.support (cft f))) : (Finset.univ.expect fun (a : G) => Real.exp |(f a).re|) ≤ 2 * Real.exp (‖f‖ₙ_[2] ^ 2 / 2)

Rudin's inequality, exponential form with absolute values.

theorem rudin_ineq {G : Type u_1} [Fintype G] [AddCommGroup G] {p : ℕ} [MeasurableSpace G] [DiscreteMeasurableSpace G] (hp : 2 ≤ p) (f : G → ℂ) (hf : AddDissociated (Function.support (cft f))) : ‖f‖ₙ_[↑p] ≤ 4 * Real.exp 2⁻¹ * √↑p * ‖f‖ₙ_[2]

Rudin's inequality, usual form.