exists_bound_norm_G_on_tsupport

lemma exists_bound_norm_G_on_tsupport    (hG : ContinuousOn G {s : ℂ | 1 ≤ s.re})    (ψ : CS 2 ℂ) :    ∃ K : ℝ, ∀ t : ℝ, t ∈ tsupport (ψ : ℝ → ℂ) →      ‖G (1 + t * Complex.I)‖ ≤ K := by  let s : Set ℝ := tsupport (ψ : ℝ → ℂ)  have hscompact : IsCompact s := by    simpa [s] using (ψ.h2.isCompact : IsCompact (tsupport (ψ : ℝ → ℂ)))  have hphi_cont : Continuous (fun t : ℝ => (1 : ℂ) + t * Complex.I) := by continuity  have hphi_maps :      Set.MapsTo (fun t : ℝ => (1 : ℂ) + t * Complex.I) s {z : ℂ | 1 ≤ z.re} := by    intro t ht    simp  have hGcomp : ContinuousOn (fun t : ℝ => G ((1 : ℂ) + t * Complex.I)) s :=    hG.comp hphi_cont.continuousOn hphi_maps  have hnorm_contOn : ContinuousOn (fun t : ℝ => ‖G ((1 : ℂ) + t * Complex.I)‖) s := hGcomp.norm  have hbdd : BddAbove ((fun t : ℝ => ‖G ((1 : ℂ) + t * Complex.I)‖) '' s) :=    (hscompact.image_of_continuousOn hnorm_contOn).bddAbove  refine ⟨sSup ((fun t : ℝ => ‖G ((1 : ℂ) + t * Complex.I)‖) '' s), ?_⟩  intro t ht  have : ‖G ((1 : ℂ) + t * Complex.I)‖ ∈      (fun t : ℝ => ‖G ((1 : ℂ) + t * Complex.I)‖) '' s := ⟨t, ht, rfl⟩  exact le_csSup hbdd this