norm_integrand_le_K_mul_norm_psi

lemma norm_integrand_le_K_mul_norm_psi    {x K : ℝ}    (hx : 0 < x)    (hK : ∀ t : ℝ, t ∈ Function.support ψ → ‖G (1 + t * Complex.I)‖ ≤ K) :    ∀ t : ℝ,      ‖(G (1 + t * Complex.I)) * (ψ t) * ((x : ℂ) ^ (t * Complex.I))‖ ≤ K * ‖ψ t‖ := by  intro t  by_cases ht : t ∈ Function.support ψ  · have hxnorm : ‖((x : ℂ) ^ (t * Complex.I))‖ = 1 := norm_x_cpow_it x t hx    calc      ‖(G (1 + t * Complex.I)) * (ψ t) * ((x : ℂ) ^ (t * Complex.I))‖          = ‖G (1 + t * Complex.I)‖ * ‖ψ t‖ * ‖((x : ℂ) ^ (t * Complex.I))‖ := by              simp [mul_left_comm, mul_comm]      _   = ‖G (1 + t * Complex.I)‖ * ‖ψ t‖ * 1 := by simp [hxnorm]      _   ≤ K * ‖ψ t‖ := by            have hGle : ‖G (1 + t * Complex.I)‖ ≤ K := hK t ht            have : ‖G (1 + t * Complex.I)‖ * ‖ψ t‖ ≤ K * ‖ψ t‖ :=              mul_le_mul_of_nonneg_right hGle (norm_nonneg _)            simpa [mul_assoc, mul_left_comm, mul_comm] using this  · have hψ0 : ψ t = 0 := by      by_contra hψ0      exact ht (by simpa [Function.support] using hψ0)    simp [hψ0, mul_comm]