FormalConjectures.ErdosProblems.«1150»

/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

Erdős Problem 1150

Reference: erdosproblems.com/1150

open scoped Polynomialnamespace Erdos1150

Is there some constant $c > 0$ such that, for all large enough $n$ and all polynomials $P$ of degree $n$ with coefficients in ${-1, 1}$, $$\max_{|z|=1} |P(z)| > (1 + c) \sqrt{n}?$$

@[category research open, AMS 12 30]
theorem erdos_1150 :
    answer(sorry) ↔ ∃ c > 0, ∀ᶠ n in Filter.atTop,
      ∀ P : ℂ[X],  (∀ i ≤ P.natDegree, P.coeff i = - 1 ∨ P.coeff i = 1) → P.natDegree = n →
        ⨆ z : Metric.sphere (0 : ℂ) 1, ‖P.eval (z : ℂ)‖ > (1 + c) * Real.sqrt n := by⊢ True ↔
  ∃ c > 0,
    ∀ᶠ (n : ℕ) in Filter.atTop,
      ∀ (P : ℂ[X]),
        (∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1) →
          P.natDegree = n → ⨆ z, ‖Polynomial.eval (↑z) P‖ > (1 + c) * √↑n
  sorryAll goals completed! 🐙

The trivial lower bound from Parseval's identity: for any polynomial $P$ of degree $n$ with coefficients in ${-1, 1}$, we have $\max_{|z|=1} |P(z)| \geq \sqrt{n+1}$.

This follows from Parseval's identity: $$\frac{1}{2\pi} \int_0^{2\pi} |P(e^{i\theta})|^2 d\theta = \sum_{k=0}^{n} |a_k|^2 = n+1$$ since each $|a_k|^2 = 1$. The circle average is bounded by the pointwise supremum squared, so $\max_{|z|=1} |P(z)|^2 \ge n+1$, whence $\max_{|z|=1} |P(z)| \ge \sqrt{n+1}$.


@[category textbook, AMS 12 30]
theorem erdos_1150.variants.parseval_lower_bound (P : ℂ[X]) (n : ℕ)
    (hcoeff : ∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1)
    (hdeg : P.natDegree = n) :
    ⨆ z : Metric.sphere (0 : ℂ) 1, ‖P.eval (z : ℂ)‖ ≥ Real.sqrt (n + 1) := byP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = n⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)
  set N : ℕ := n + 1 with hNP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)
  -- Each coefficient at index $i \le n$ has norm $1$.
  have hcoeff_norm : ∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1 := by
    intro i hiP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1i:ℕhi:i ∈ Finset.range N⊢ ‖P.coeff i‖ = 1P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)
    have hi' : i ≤ n := Nat.lt_succ_iff.mp (Finset.mem_range.mp hi)P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1i:ℕhi:i ∈ Finset.range Nhi':i ≤ n⊢ ‖P.coeff i‖ = 1P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)
    rcases hcoeff i (hdeg ▸ hi') with h | hinlP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1i:ℕhi:i ∈ Finset.range Nhi':i ≤ nh:P.coeff i = -1⊢ ‖P.coeff i‖ = 1inrP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1i:ℕhi:i ∈ Finset.range Nhi':i ≤ nh:P.coeff i = 1⊢ ‖P.coeff i‖ = 1P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1) <;>inlP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1i:ℕhi:i ∈ Finset.range Nhi':i ≤ nh:P.coeff i = -1⊢ ‖P.coeff i‖ = 1inrP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1i:ℕhi:i ∈ Finset.range Nhi':i ≤ nh:P.coeff i = 1⊢ ‖P.coeff i‖ = 1P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1) simp [h]P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)
  -- $P$'s support is exactly $\{0, \dots, n\}$: indices $\le n$ are $\pm 1$, hence nonzero;
  -- indices $> n$ have coefficient $0$ by $P.\text{natDegree} = n$.
  have hsupport : P.support = Finset.range N := by
    ext iP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1i:ℕ⊢ i ∈ P.support ↔ i ∈ Finset.range NP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range N⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)
    simp only [Polynomial.mem_support_iff, Finset.mem_range]P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1i:ℕ⊢ P.coeff i ≠ 0 ↔ i < NP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range N⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)
    refine ⟨fun hne => ?_, fun hi => ?_⟩refine_1P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1i:ℕhne:P.coeff i ≠ 0⊢ i < Nrefine_2P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1i:ℕhi:i < N⊢ P.coeff i ≠ 0P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range N⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)
    ·refine_1P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1i:ℕhne:P.coeff i ≠ 0⊢ i < NP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range N⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1) by_contra hlerefine_1P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1i:ℕhne:P.coeff i ≠ 0hle:¬i < N⊢ FalseP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range N⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)
      push Not at hlerefine_1P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1i:ℕhne:P.coeff i ≠ 0hle:N ≤ i⊢ FalseP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range N⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)
      exact hne <| Polynomial.coeff_eq_zero_of_natDegree_lt (byP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1i:ℕhne:P.coeff i ≠ 0hle:N ≤ i⊢ P.natDegree < iP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range N⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1) omegaAll goals completed! 🐙P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range N⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1))
    ·refine_2P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1i:ℕhi:i < N⊢ P.coeff i ≠ 0P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range N⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1) have h1 : ‖P.coeff i‖ = 1 := hcoeff_norm i (Finset.mem_range.mpr hi)refine_2P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1i:ℕhi:i < Nh1:‖P.coeff i‖ = 1⊢ P.coeff i ≠ 0P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range N⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)
      intro hrefine_2P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1i:ℕhi:i < Nh1:‖P.coeff i‖ = 1h:P.coeff i = 0⊢ FalseP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range N⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1); simp [h] at h1P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range N⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range N⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)
  -- Apply upstream Parseval. The LHS sum evaluates to $N = n + 1$.
  have hParseval : Real.circleAverage (fun z ↦ ‖P.eval z‖ ^ 2) 0 1 = (N : ℝ) := by
    rw [← P.sum_sq_norm_coeff_eq_circleAverage,P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range N⊢ ∑ i ∈ P.support, ‖P.coeff i‖ ^ 2 = ↑NP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range N⊢ ∑ i ∈ Finset.range N, ‖P.coeff i‖ ^ 2 = ↑NP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑N⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1) hsupportP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range N⊢ ∑ i ∈ Finset.range N, ‖P.coeff i‖ ^ 2 = ↑NP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range N⊢ ∑ i ∈ Finset.range N, ‖P.coeff i‖ ^ 2 = ↑NP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑N⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)]P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range N⊢ ∑ i ∈ Finset.range N, ‖P.coeff i‖ ^ 2 = ↑NP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑N⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)
    calc ∑ i ∈ Finset.range N, ‖P.coeff i‖ ^ 2
        = ∑ _i ∈ Finset.range N, (1 : ℝ) := byP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range N⊢ ∑ i ∈ Finset.range N, ‖P.coeff i‖ ^ 2 = ∑ _i ∈ Finset.range N, 1P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑N⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)
          refine Finset.sum_congr rfl fun i hi => ?_P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range Ni:ℕhi:i ∈ Finset.range N⊢ ‖P.coeff i‖ ^ 2 = 1P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑N⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)
          rw [hcoeff_norm i hi,P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range Ni:ℕhi:i ∈ Finset.range N⊢ 1 ^ 2 = 1All goals completed! 🐙P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑N⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1) one_powP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range Ni:ℕhi:i ∈ Finset.range N⊢ 1 = 1All goals completed! 🐙P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑N⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)]All goals completed! 🐙P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑N⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)
      _ = (N : ℝ) := byP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range N⊢ ∑ _i ∈ Finset.range N, 1 = ↑NP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑N⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1) simpP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑N⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑N⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)
  -- Triangle inequality: on the unit sphere, $\|P(z)\| \le N$.
  have hdeg' : P.natDegree < N := by omegaP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < N⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < N⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)
  have htri : ∀ z ∈ Metric.sphere (0 : ℂ) 1, ‖P.eval z‖ ≤ (N : ℝ) := by
    intro z hzP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nz:ℂhz:z ∈ Metric.sphere 0 1⊢ ‖Polynomial.eval z P‖ ≤ ↑NP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑N⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)
    have hz1 : ‖z‖ = 1 := byP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = n⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nz:ℂhz:z ∈ Metric.sphere 0 1hz1:‖z‖ = 1⊢ ‖Polynomial.eval z P‖ ≤ ↑NP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑N⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1) simpa [Metric.mem_sphere, dist_zero_right] using hzP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nz:ℂhz:z ∈ Metric.sphere 0 1hz1:‖z‖ = 1⊢ ‖Polynomial.eval z P‖ ≤ ↑NP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑N⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nz:ℂhz:z ∈ Metric.sphere 0 1hz1:‖z‖ = 1⊢ ‖Polynomial.eval z P‖ ≤ ↑NP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑N⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)
    calc ‖P.eval z‖
        = ‖∑ i ∈ Finset.range N, P.coeff i * z ^ i‖ := byP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nz:ℂhz:z ∈ Metric.sphere 0 1hz1:‖z‖ = 1⊢ ‖Polynomial.eval z P‖ = ‖∑ i ∈ Finset.range N, P.coeff i * z ^ i‖P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑N⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)
          rw [Polynomial.eval_eq_sum_range' hdeg'P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nz:ℂhz:z ∈ Metric.sphere 0 1hz1:‖z‖ = 1⊢ ‖∑ i ∈ Finset.range N, P.coeff i * z ^ i‖ = ‖∑ i ∈ Finset.range N, P.coeff i * z ^ i‖All goals completed! 🐙P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑N⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)]All goals completed! 🐙P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑N⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)
      _ ≤ ∑ i ∈ Finset.range N, ‖P.coeff i * z ^ i‖ := norm_sum_le _ _
      _ = ∑ i ∈ Finset.range N, ‖P.coeff i‖ := byP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nz:ℂhz:z ∈ Metric.sphere 0 1hz1:‖z‖ = 1⊢ ∑ i ∈ Finset.range N, ‖P.coeff i * z ^ i‖ = ∑ i ∈ Finset.range N, ‖P.coeff i‖P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑N⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)
          refine Finset.sum_congr rfl fun i _ => ?_P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nz:ℂhz:z ∈ Metric.sphere 0 1hz1:‖z‖ = 1i:ℕx✝:i ∈ Finset.range N⊢ ‖P.coeff i * z ^ i‖ = ‖P.coeff i‖P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑N⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)
          rw [norm_mul,P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nz:ℂhz:z ∈ Metric.sphere 0 1hz1:‖z‖ = 1i:ℕx✝:i ∈ Finset.range N⊢ ‖P.coeff i‖ * ‖z ^ i‖ = ‖P.coeff i‖All goals completed! 🐙P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑N⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1) norm_pow,P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nz:ℂhz:z ∈ Metric.sphere 0 1hz1:‖z‖ = 1i:ℕx✝:i ∈ Finset.range N⊢ ‖P.coeff i‖ * ‖z‖ ^ i = ‖P.coeff i‖All goals completed! 🐙P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑N⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1) hz1,P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nz:ℂhz:z ∈ Metric.sphere 0 1hz1:‖z‖ = 1i:ℕx✝:i ∈ Finset.range N⊢ ‖P.coeff i‖ * 1 ^ i = ‖P.coeff i‖All goals completed! 🐙P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑N⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1) one_pow,P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nz:ℂhz:z ∈ Metric.sphere 0 1hz1:‖z‖ = 1i:ℕx✝:i ∈ Finset.range N⊢ ‖P.coeff i‖ * 1 = ‖P.coeff i‖All goals completed! 🐙P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑N⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1) mul_oneP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nz:ℂhz:z ∈ Metric.sphere 0 1hz1:‖z‖ = 1i:ℕx✝:i ∈ Finset.range N⊢ ‖P.coeff i‖ = ‖P.coeff i‖All goals completed! 🐙P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑N⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)]All goals completed! 🐙P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑N⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)
      _ = ∑ _i ∈ Finset.range N, (1 : ℝ) :=
          Finset.sum_congr rfl fun i hi => hcoeff_norm i hi
      _ = (N : ℝ) := byP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nz:ℂhz:z ∈ Metric.sphere 0 1hz1:‖z‖ = 1⊢ ∑ _i ∈ Finset.range N, 1 = ↑NP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑N⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1) simpP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑N⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑N⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)
  -- The set of $\|P(z)\|$ over the sphere is bounded above by $N$.
  have hbdd : BddAbove
      (Set.range fun z : Metric.sphere (0 : ℂ) 1 => ‖P.eval (z : ℂ)‖) := by
    refine ⟨(N : ℝ), ?_⟩P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑N⊢ ↑N ∈ upperBounds (Set.range fun z ↦ ‖Polynomial.eval (↑z) P‖)P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑Nhbdd:BddAbove (Set.range fun z ↦ ‖Polynomial.eval (↑z) P‖)⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)
    rintro _ ⟨⟨z, hz⟩, rfl⟩P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑Nz:ℂhz:z ∈ Metric.sphere 0 1⊢ (fun z ↦ ‖Polynomial.eval (↑z) P‖) ⟨z, hz⟩ ≤ ↑NP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑Nhbdd:BddAbove (Set.range fun z ↦ ‖Polynomial.eval (↑z) P‖)⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)
    exact htri z hzP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑Nhbdd:BddAbove (Set.range fun z ↦ ‖Polynomial.eval (↑z) P‖)⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑Nhbdd:BddAbove (Set.range fun z ↦ ‖Polynomial.eval (↑z) P‖)⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)
  set S : ℝ := ⨆ z : Metric.sphere (0 : ℂ) 1, ‖P.eval (z : ℂ)‖ with hSdefP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑Nhbdd:BddAbove (Set.range fun z ↦ ‖Polynomial.eval (↑z) P‖)S:ℝ := ⨆ z, ‖Polynomial.eval (↑z) P‖hSdef:S = ⨆ z, ‖Polynomial.eval (↑z) P‖⊢ S ≥ √(↑n + 1)
  have hS_nonneg : 0 ≤ S := Real.iSup_nonneg fun _ => norm_nonneg _P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑Nhbdd:BddAbove (Set.range fun z ↦ ‖Polynomial.eval (↑z) P‖)S:ℝ := ⨆ z, ‖Polynomial.eval (↑z) P‖hSdef:S = ⨆ z, ‖Polynomial.eval (↑z) P‖hS_nonneg:0 ≤ S⊢ S ≥ √(↑n + 1)
  -- Every $\|P(z)\|^2 \le S^2$ on the sphere.
  have hbound_sq : ∀ z ∈ Metric.sphere (0 : ℂ) 1, ‖P.eval z‖ ^ 2 ≤ S ^ 2 := byP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = n⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑Nhbdd:BddAbove (Set.range fun z ↦ ‖Polynomial.eval (↑z) P‖)S:ℝ := ⨆ z, ‖Polynomial.eval (↑z) P‖hSdef:S = ⨆ z, ‖Polynomial.eval (↑z) P‖hS_nonneg:0 ≤ Shbound_sq:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ^ 2 ≤ S ^ 2⊢ S ≥ √(↑n + 1)
    intro z hzP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑Nhbdd:BddAbove (Set.range fun z ↦ ‖Polynomial.eval (↑z) P‖)S:ℝ := ⨆ z, ‖Polynomial.eval (↑z) P‖hSdef:S = ⨆ z, ‖Polynomial.eval (↑z) P‖hS_nonneg:0 ≤ Sz:ℂhz:z ∈ Metric.sphere 0 1⊢ ‖Polynomial.eval z P‖ ^ 2 ≤ S ^ 2P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑Nhbdd:BddAbove (Set.range fun z ↦ ‖Polynomial.eval (↑z) P‖)S:ℝ := ⨆ z, ‖Polynomial.eval (↑z) P‖hSdef:S = ⨆ z, ‖Polynomial.eval (↑z) P‖hS_nonneg:0 ≤ Shbound_sq:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ^ 2 ≤ S ^ 2⊢ S ≥ √(↑n + 1)
    have hle : ‖P.eval z‖ ≤ S := le_ciSup_of_le hbdd ⟨z, hz⟩ le_rflP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑Nhbdd:BddAbove (Set.range fun z ↦ ‖Polynomial.eval (↑z) P‖)S:ℝ := ⨆ z, ‖Polynomial.eval (↑z) P‖hSdef:S = ⨆ z, ‖Polynomial.eval (↑z) P‖hS_nonneg:0 ≤ Sz:ℂhz:z ∈ Metric.sphere 0 1hle:‖Polynomial.eval z P‖ ≤ S⊢ ‖Polynomial.eval z P‖ ^ 2 ≤ S ^ 2P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑Nhbdd:BddAbove (Set.range fun z ↦ ‖Polynomial.eval (↑z) P‖)S:ℝ := ⨆ z, ‖Polynomial.eval (↑z) P‖hSdef:S = ⨆ z, ‖Polynomial.eval (↑z) P‖hS_nonneg:0 ≤ Shbound_sq:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ^ 2 ≤ S ^ 2⊢ S ≥ √(↑n + 1)
    exact pow_le_pow_left₀ (norm_nonneg _) hle 2P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑Nhbdd:BddAbove (Set.range fun z ↦ ‖Polynomial.eval (↑z) P‖)S:ℝ := ⨆ z, ‖Polynomial.eval (↑z) P‖hSdef:S = ⨆ z, ‖Polynomial.eval (↑z) P‖hS_nonneg:0 ≤ Shbound_sq:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ^ 2 ≤ S ^ 2⊢ S ≥ √(↑n + 1)P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑Nhbdd:BddAbove (Set.range fun z ↦ ‖Polynomial.eval (↑z) P‖)S:ℝ := ⨆ z, ‖Polynomial.eval (↑z) P‖hSdef:S = ⨆ z, ‖Polynomial.eval (↑z) P‖hS_nonneg:0 ≤ Shbound_sq:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ^ 2 ≤ S ^ 2⊢ S ≥ √(↑n + 1)
  -- $\|P(z)\|^2$ is continuous, hence circle-integrable.
  have hCI : CircleIntegrable (fun z ↦ ‖P.eval z‖ ^ 2) 0 1 :=
    (((P.continuous).norm).pow 2).continuousOn.circleIntegrable zero_le_oneP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑Nhbdd:BddAbove (Set.range fun z ↦ ‖Polynomial.eval (↑z) P‖)S:ℝ := ⨆ z, ‖Polynomial.eval (↑z) P‖hSdef:S = ⨆ z, ‖Polynomial.eval (↑z) P‖hS_nonneg:0 ≤ Shbound_sq:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ^ 2 ≤ S ^ 2hCI:CircleIntegrable (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1⊢ S ≥ √(↑n + 1)
  -- Circle-average $\le S^2$.
  have h_avg_le : Real.circleAverage (fun z ↦ ‖P.eval z‖ ^ 2) 0 1 ≤ S ^ 2 := byP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = n⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑Nhbdd:BddAbove (Set.range fun z ↦ ‖Polynomial.eval (↑z) P‖)S:ℝ := ⨆ z, ‖Polynomial.eval (↑z) P‖hSdef:S = ⨆ z, ‖Polynomial.eval (↑z) P‖hS_nonneg:0 ≤ Shbound_sq:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ^ 2 ≤ S ^ 2hCI:CircleIntegrable (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1h_avg_le:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 ≤ S ^ 2⊢ S ≥ √(↑n + 1)
    refine Real.circleAverage_mono_on_of_le_circle hCI ?_P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑Nhbdd:BddAbove (Set.range fun z ↦ ‖Polynomial.eval (↑z) P‖)S:ℝ := ⨆ z, ‖Polynomial.eval (↑z) P‖hSdef:S = ⨆ z, ‖Polynomial.eval (↑z) P‖hS_nonneg:0 ≤ Shbound_sq:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ^ 2 ≤ S ^ 2hCI:CircleIntegrable (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1⊢ ∀ x ∈ Metric.sphere 0 |1|, ‖Polynomial.eval x P‖ ^ 2 ≤ S ^ 2P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑Nhbdd:BddAbove (Set.range fun z ↦ ‖Polynomial.eval (↑z) P‖)S:ℝ := ⨆ z, ‖Polynomial.eval (↑z) P‖hSdef:S = ⨆ z, ‖Polynomial.eval (↑z) P‖hS_nonneg:0 ≤ Shbound_sq:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ^ 2 ≤ S ^ 2hCI:CircleIntegrable (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1h_avg_le:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 ≤ S ^ 2⊢ S ≥ √(↑n + 1)
    simpa [abs_one] using hbound_sqP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑Nhbdd:BddAbove (Set.range fun z ↦ ‖Polynomial.eval (↑z) P‖)S:ℝ := ⨆ z, ‖Polynomial.eval (↑z) P‖hSdef:S = ⨆ z, ‖Polynomial.eval (↑z) P‖hS_nonneg:0 ≤ Shbound_sq:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ^ 2 ≤ S ^ 2hCI:CircleIntegrable (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1h_avg_le:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 ≤ S ^ 2⊢ S ≥ √(↑n + 1)P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑Nhbdd:BddAbove (Set.range fun z ↦ ‖Polynomial.eval (↑z) P‖)S:ℝ := ⨆ z, ‖Polynomial.eval (↑z) P‖hSdef:S = ⨆ z, ‖Polynomial.eval (↑z) P‖hS_nonneg:0 ≤ Shbound_sq:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ^ 2 ≤ S ^ 2hCI:CircleIntegrable (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1h_avg_le:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 ≤ S ^ 2⊢ S ≥ √(↑n + 1)
  rw [hParsevalP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑Nhbdd:BddAbove (Set.range fun z ↦ ‖Polynomial.eval (↑z) P‖)S:ℝ := ⨆ z, ‖Polynomial.eval (↑z) P‖hSdef:S = ⨆ z, ‖Polynomial.eval (↑z) P‖hS_nonneg:0 ≤ Shbound_sq:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ^ 2 ≤ S ^ 2hCI:CircleIntegrable (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1h_avg_le:↑N ≤ S ^ 2⊢ S ≥ √(↑n + 1)P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑Nhbdd:BddAbove (Set.range fun z ↦ ‖Polynomial.eval (↑z) P‖)S:ℝ := ⨆ z, ‖Polynomial.eval (↑z) P‖hSdef:S = ⨆ z, ‖Polynomial.eval (↑z) P‖hS_nonneg:0 ≤ Shbound_sq:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ^ 2 ≤ S ^ 2hCI:CircleIntegrable (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1h_avg_le:↑N ≤ S ^ 2⊢ S ≥ √(↑n + 1)] at h_avg_leP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑Nhbdd:BddAbove (Set.range fun z ↦ ‖Polynomial.eval (↑z) P‖)S:ℝ := ⨆ z, ‖Polynomial.eval (↑z) P‖hSdef:S = ⨆ z, ‖Polynomial.eval (↑z) P‖hS_nonneg:0 ≤ Shbound_sq:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ^ 2 ≤ S ^ 2hCI:CircleIntegrable (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1h_avg_le:↑N ≤ S ^ 2⊢ S ≥ √(↑n + 1)
  -- $N \le S^2$ with $S \ge 0$, so $\sqrt N \le S$.
  have h_sqrt : Real.sqrt ((N : ℝ)) ≤ S := byP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = n⊢ ⨆ z, ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑Nhbdd:BddAbove (Set.range fun z ↦ ‖Polynomial.eval (↑z) P‖)S:ℝ := ⨆ z, ‖Polynomial.eval (↑z) P‖hSdef:S = ⨆ z, ‖Polynomial.eval (↑z) P‖hS_nonneg:0 ≤ Shbound_sq:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ^ 2 ≤ S ^ 2hCI:CircleIntegrable (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1h_avg_le:↑N ≤ S ^ 2h_sqrt:√↑N ≤ S⊢ S ≥ √(↑n + 1)
    calc Real.sqrt ((N : ℝ))
        ≤ Real.sqrt (S ^ 2) := Real.sqrt_le_sqrt h_avg_le
      _ = S := Real.sqrt_sq hS_nonnegP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑Nhbdd:BddAbove (Set.range fun z ↦ ‖Polynomial.eval (↑z) P‖)S:ℝ := ⨆ z, ‖Polynomial.eval (↑z) P‖hSdef:S = ⨆ z, ‖Polynomial.eval (↑z) P‖hS_nonneg:0 ≤ Shbound_sq:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ^ 2 ≤ S ^ 2hCI:CircleIntegrable (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1h_avg_le:↑N ≤ S ^ 2h_sqrt:√↑N ≤ S⊢ S ≥ √(↑n + 1)
  calc Real.sqrt ((n : ℝ) + 1)
      = Real.sqrt ((N : ℝ)) := byP:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑Nhbdd:BddAbove (Set.range fun z ↦ ‖Polynomial.eval (↑z) P‖)S:ℝ := ⨆ z, ‖Polynomial.eval (↑z) P‖hSdef:S = ⨆ z, ‖Polynomial.eval (↑z) P‖hS_nonneg:0 ≤ Shbound_sq:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ^ 2 ≤ S ^ 2hCI:CircleIntegrable (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1h_avg_le:↑N ≤ S ^ 2h_sqrt:√↑N ≤ S⊢ √(↑n + 1) = √↑N push_cast [hN]P:ℂ[X]n:ℕhcoeff:∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1hdeg:P.natDegree = nN:ℕ := n + 1hN:N = n + 1hcoeff_norm:∀ i ∈ Finset.range N, ‖P.coeff i‖ = 1hsupport:P.support = Finset.range NhParseval:Real.circleAverage (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1 = ↑Nhdeg':P.natDegree < Nhtri:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ≤ ↑Nhbdd:BddAbove (Set.range fun z ↦ ‖Polynomial.eval (↑z) P‖)S:ℝ := ⨆ z, ‖Polynomial.eval (↑z) P‖hSdef:S = ⨆ z, ‖Polynomial.eval (↑z) P‖hS_nonneg:0 ≤ Shbound_sq:∀ z ∈ Metric.sphere 0 1, ‖Polynomial.eval z P‖ ^ 2 ≤ S ^ 2hCI:CircleIntegrable (fun z ↦ ‖Polynomial.eval z P‖ ^ 2) 0 1h_avg_le:↑N ≤ S ^ 2h_sqrt:√↑N ≤ S⊢ √(↑n + 1) = √(↑n + 1); ring_nfAll goals completed! 🐙
    _ ≤ S := h_sqrt

end Erdos1150