Continuity of Energy Functionals

This file establishes the continuity properties of energy functionals that appear in the RH criterion and Γ-convergence theory.

theorem Frourio.norm_sq_le_of_norm_le {x : ℂ} {C : ℝ} (h : ‖x‖ ≤ C) : ‖x‖ ^ 2 ≤ C ^ 2

If the norm is bounded by C, then the squared norm is bounded by C^2

theorem Frourio.zeta_bounded_on_radius [ZetaLineAPI] (R₀ : ℝ) : ∃ (C₀ : ℝ), ∀ (τ : ℝ), |τ| ≤ R₀ → ‖ZetaLineAPI.zeta_on_line τ‖ ≤ C₀

For any fixed radius, there exists a bound on the zeta function