rudin_ineq

lemma rudin_ineq (hp : 2 ≤ p) (f : G → ℂ) (hf : AddDissociated <| support <| cft f) :    ‖f‖ₙ_[p] ≤ 4 * exp 2⁻¹ * sqrt p * ‖f‖ₙ_[2] := by  have hp₁ : (1 : ℝ≥0∞) ≤ p := by exact_mod_cast one_le_two.trans hp  calc    (‖f‖ₙ_[p] : ℝ) = ‖(fun a ↦ ((f a).re : ℂ)) + I • (fun a ↦ ((f a).im : ℂ))‖ₙ_[p]      := by congr with a; simp [mul_comm I]    _ ≤ ‖fun a ↦ ((f a).re : ℂ)‖ₙ_[p] + ‖I • (fun a ↦ ((f a).im : ℂ))‖ₙ_[p]      := cLpNorm_add_le hp₁    _ = ‖re ∘ f‖ₙ_[p] + ‖re ∘ ((-I) • f)‖ₙ_[p] := by        rw [cLpNorm_const_smul, Complex.norm_I, one_mul, ← Complex.cLpNorm_coe_comp,          ← Complex.cLpNorm_coe_comp]        congr        ext a : 1        simp    _ ≤ 2 * exp 2⁻¹ * sqrt p * ‖f‖ₙ_[2] + 2 * exp 2⁻¹ * sqrt p * ‖(-I) • f‖ₙ_[2]      := add_le_add (rudin_ineq_aux hp _ hf) <| rudin_ineq_aux hp _ <| by        rwa [cft_smul, support_const_smul_of_ne_zero]; simp    _ = 4 * exp 2⁻¹ * sqrt p * ‖f‖ₙ_[2] := by        rw [cLpNorm_const_smul, norm_neg, Complex.norm_I, one_mul]; ring