Coefficients Product Bound

Let $a, b, c$ be complex numbers. If for any complex number $z$ satisfying $|z| \le 1$, we have $|az^2 + bz + c| \le 1$, find the maximum possible value of $|bc|$.

Replace sorry in the template below with your solution. Mathlib version used by the checker is v4.34.0.

import Mathlib.Analysis.Complex.Norm

def S : Set ℝ :=
    { t | ∃ a b c : ℂ, (∀ z : ℂ, ‖z‖ ≤ 1 → ‖a * z ^ 2 + b * z + c‖ ≤ 1) ∧ (t = ‖b * c‖) }

def answer : ℝ := sorry

theorem solution : IsGreatest S answer := sorry

Submit Solution

Login to submit a solution.

Recent Submissions