rudin_exp_ineq

lemma rudin_exp_ineq (f : G → ℂ) (hf : AddDissociated <| support <| cft f) :    𝔼 a, exp (f a).re ≤ exp (‖f‖ₙ_[2] ^ 2 / 2) := by  have (z : ℂ) : exp (re z) ≤ cosh ‖z‖ + re (z / ‖z‖) * sinh ‖z‖ :=    calc      _ = _ := by obtain rfl | hz := eq_or_ne z 0 <;> simp [*]      _ ≤ _ := exp_mul_le_cosh_add_mul_sinh (by simpa using z.abs_re_div_norm_le_one) _  choose c hc hcf using fun ψ ↦ Complex.exists_norm_mul_eq_self (cft f ψ)  have hc₀ (ψ) : c ψ ≠ 0 := fun h ↦ by simpa [h] using hc ψ  have (a : G) :    exp (f a).re ≤ ∏ ψ, (cosh ‖cft f ψ‖ + (c ψ * sinh ‖cft f ψ‖ * ψ a).re) :=    calc      _ = ∏ ψ, exp ((cft f ψ * ψ a).re) := by simp_rw [← exp_sum, ← Complex.re_sum, cft_inversion]      _ ≤ _ := prod_le_prod (fun _ _ ↦ by positivity) fun _ _ ↦ this _      _ = ∏ ψ, (cosh ‖cft f ψ‖ + (c ψ * (cft f ψ * ψ a)            / (c ψ * ↑‖cft f ψ‖)).re * sinh ‖cft f ψ‖) := by          simp_rw [norm_mul, AddChar.norm_apply, mul_one, mul_div_mul_left _ _ (hc₀ _)]      _ = _ := by          congr with ψ          obtain hψ | hψ := eq_or_ne (cft f ψ) 0          · simp [hψ]          · simp only [hcf, mul_left_comm (c _), mul_div_cancel_left₀ _ hψ, ← Complex.re_mul_ofReal,              mul_right_comm]  calc    _ ≤ 𝔼 a, ∏ ψ, (cosh ‖cft f ψ‖ + (c ψ * sinh ‖cft f ψ‖ * ψ a).re) :=        expect_le_expect fun _ _ ↦ this _    _ = ∏ ψ, cosh ‖cft f ψ‖ :=        AddDissociated.randomisation _ _ <| by simpa [-Complex.ofReal_sinh, hc₀]    _ ≤ ∏ ψ, exp (‖cft f ψ‖ ^ 2 / 2) :=        prod_le_prod (fun _ _ ↦ by positivity) fun _ _ ↦ cosh_le_exp_half_sq _    _ = _ := by simp_rw [← exp_sum, ← sum_div, ← dL2Norm_cft, dL2Norm_sq_eq_sum_norm]