/-- A unit-circle point has real part in the approximation interval. -/
theorem unitCircle_re_mem (z : Metric.sphere (0 : ℂ) |(1 : ℝ)|) :
    z.val.re ∈ Set.Icc (-1 : ℝ) 1 := by
  have hn : ‖z.val‖ = 1 := by simpa only [Metric.mem_sphere, dist_zero_right, abs_one] using z.property
  exact abs_le.mp ((Complex.abs_re_le_norm z.val).trans_eq hn)

/-- A unit-circle point is nonzero. -/
theorem unitCircle_ne_zero (z : Metric.sphere (0 : ℂ) |(1 : ℝ)|) : z.val ≠ 0 := by
  apply norm_pos_iff.mp
  have hn : ‖z.val‖ = 1 := by simpa only [Metric.mem_sphere, dist_zero_right, abs_one] using z.property
  rw [hn]
  norm_num

/-- On the unit circle, the Joukowski map is the real-part projection (ATAP Ch. 8). -/
theorem joukowski_unitCircle (z : Metric.sphere (0 : ℂ) |(1 : ℝ)|) :
    joukowski ⟨z.val, unitCircle_ne_zero z⟩ = (z.val.re : ℂ) := by
  have hn : ‖z.val‖ = 1 := by simpa only [Metric.mem_sphere, dist_zero_right, abs_one] using z.property
  change (z.val + z.val⁻¹) / 2 = _
  rw [Complex.inv_eq_conj hn]
  apply Complex.ext <;> simp

/-- The Joukowski map respects negation (ATAP, Chapter 8). -/
@[simp] theorem joukowski_neg (z : {z : ℂ // z ≠ 0}) :
    joukowski ⟨-z.val, neg_ne_zero.mpr z.property⟩ = -joukowski z := by
  simp [joukowski]; ring

/-- The filled Bernstein ellipse is open (ATAP, Chapter 8). -/
theorem isOpen_bernsteinEllipse (ρ : Set.Ioi (1 : ℝ)) : IsOpen (bernsteinEllipse ρ) := by
  apply isOpen_lt _ continuous_const
  fun_prop

/-- Factoring the distance to the left focus (ATAP, Chapter 8). -/
theorem joukowski_add_one (z : {z : ℂ // z ≠ 0}) :
    joukowski z + 1 = (z.val + 1) ^ 2 / (2 * z.val) := by
  unfold joukowski
  field_simp [z.property]
  ring

/-- The focal-distance identity underlying Bernstein ellipses (ATAP, Chapter 8). -/
theorem norm_joukowski_sub_one_add_norm_joukowski_add_one (z : {z : ℂ // z ≠ 0}) :
    ‖joukowski z - 1‖ + ‖joukowski z + 1‖ = ‖z.val‖ + ‖z.val‖⁻¹ := by
  rw [joukowski_sub_one z, joukowski_add_one z]
  simp only [norm_div, norm_pow, norm_mul, norm_ofNat]
  have h : ‖z.val - 1‖ ^ 2 + ‖z.val + 1‖ ^ 2 = 2 * (‖z.val‖ ^ 2 + 1) := by
    simp only [← normSq_eq_norm_sq, normSq_apply, sub_re, sub_im, add_re, add_im,
      one_re, one_im]
    ring
  rw [← add_div, h]
  field_simp

/-- Each circle-image point is approached from inside the ellipse (ATAP, Chapter 8). -/
theorem joukowski_mem_closure_bernsteinEllipse {ρ : ℝ} (hρ : 1 < ρ)
    (z : {z : ℂ // z ≠ 0}) (hz : ‖z.val‖ = ρ) :
    joukowski z ∈ closure (bernsteinEllipse ⟨ρ, hρ⟩) := by
  have hρ0 : 0 < ρ := by linarith
  let g : ℝ → ℂ := fun t => (t : ℂ) / (ρ : ℂ) * z.val
  have hg : g ρ = z.val := by simp [g, ne_of_gt hρ0]
  have hc : ContinuousAt (fun t => (g t + (g t)⁻¹) / 2) ρ := by
    apply (analyticAt_joukowski_expression z.property).continuousAt.comp_of_eq
      (by fun_prop : ContinuousAt g ρ) hg
  have ht : ρ ∈ closure (Set.Ioo (1 : ℝ) ρ) := by
    rw [closure_Ioo (ne_of_lt hρ)]
    exact ⟨le_of_lt hρ, le_rfl⟩
  have hmem := mem_closure_image hc ht
  simp only [hg] at hmem
  change joukowski z ∈ closure ((fun t => (g t + (g t)⁻¹) / 2) '' Set.Ioo 1 ρ) at hmem
  apply closure_mono (s := (fun t => (g t + (g t)⁻¹) / 2) '' Set.Ioo 1 ρ) _ hmem
  rintro _ ⟨t, ht, rfl⟩
  have ht0 : 0 < t := by linarith [ht.1]
  have hnorm : ‖g t‖ = t := by
    simp [g, norm_real, Real.norm_eq_abs, abs_of_pos ht0,
      abs_of_pos hρ0, hz, ne_of_gt hρ0]
  have hg0 : g t ≠ 0 := norm_pos_iff.mp (by rw [hnorm]; exact ht0)
  change joukowski ⟨g t, hg0⟩ ∈ _
  apply (joukowski_mem_bernsteinEllipse_iff hρ ⟨g t, hg0⟩).2
  change ρ⁻¹ < ‖g t‖ ∧ ‖g t‖ < ρ
  rw [hnorm]
  exact ⟨lt_trans ((inv_lt_one₀ hρ0).2 hρ) ht.1, ht.2⟩

/-- The boundary of the open filled ellipse is exactly the circle image (ATAP, Chapter 8). -/
theorem frontier_bernsteinEllipse {ρ : ℝ} (hρ : 1 < ρ) :
    frontier (bernsteinEllipse ⟨ρ, hρ⟩) = joukowski '' {z : {z : ℂ // z ≠ 0} | ‖z.val‖ = ρ} := by
  apply Set.Subset.antisymm
  · rw [image_joukowski_sphere hρ]
    exact frontier_lt_subset_eq (by fun_prop) continuous_const
  · rintro w ⟨z, hz, rfl⟩
    have hn : ‖z.val‖ = ρ := hz
    rw [(isOpen_bernsteinEllipse ⟨ρ, hρ⟩).frontier_eq]
    refine ⟨joukowski_mem_closure_bernsteinEllipse hρ z hn, ?_⟩
    have heq : joukowski z ∈ {w : ℂ | ‖w - 1‖ + ‖w + 1‖ = ρ + ρ⁻¹} :=
      (image_joukowski_sphere hρ).subset ⟨z, hz, rfl⟩
    change ¬ ‖joukowski z - 1‖ + ‖joukowski z + 1‖ < ρ + ρ⁻¹
    exact not_lt.mpr (le_of_eq heq.symm)

/-- Continuity on the actual nonzero domain (ATAP, Chapter 8). -/
theorem continuous_joukowski : Continuous joukowski :=
  (continuous_subtype_val.add (continuous_subtype_val.inv₀ (fun z => z.property))).div_const 2

/-- Continuous complex data are integrable for the first-kind measure (ATAP Ch. 3). -/
theorem integrable_classicalMeasureT_complex {f : ℝ → ℂ}
    (hf : ContinuousOn f (Icc (-1) 1)) : Integrable f classicalMeasureT :=
  integrable_complex_of_re_im
    (integrable_classicalMeasureT (Complex.continuous_re.comp_continuousOn hf))
    (integrable_classicalMeasureT (Complex.continuous_im.comp_continuousOn hf))

@[simp] theorem ComplexCoefficientInput.ofL1_val (f : ComplexIntegrableInput) (n : ℕ) :
    (ofL1 f n).val = f.val := rfl

@[simp] theorem ComplexCoefficientInput.ofContinuousOn_val (f : ℝ → ℂ)
    (hf : ContinuousOn f (Icc (-1) 1)) (n : ℕ) :
    (ofContinuousOn f hf n).val = f := rfl

@[simp] theorem ComplexCoefficientInput.ofReal_val {n : ℕ} (f : CoefficientInput n) :
    (ofReal f).val = fun x ↦ (f.val x : ℂ) := rfl

@[simp] theorem ComplexCoefficientInput.re_val {n : ℕ} (f : ComplexCoefficientInput n) :
    f.re.val = fun x ↦ (f.val x).re := rfl

@[simp] theorem ComplexCoefficientInput.im_val {n : ℕ} (f : ComplexCoefficientInput n) :
    f.im.val = fun x ↦ (f.val x).im := rfl

/-- The complex zero-index domain is precisely L1. -/
theorem complexCoefficientInput_zero_iff (f : ℝ → ℂ) :
    Integrable (fun x ↦ f x * (((T ℝ (0 : ℕ)).eval x : ℝ) : ℂ)) classicalMeasureT ↔
      Integrable f classicalMeasureT := by simp

/-- Cosine representation of complex coefficients (ATAP, Chapter 3). -/
theorem complexCoefficient_eq_integral_cos {f : ℝ → ℂ}
    (hf : ContinuousOn f (Set.Icc (-1) 1)) (n : ℕ) :
    complexCoefficient (ComplexCoefficientInput.ofContinuousOn f hf n) = ((if n = 0 then 1 else 2 : ℝ) / π : ℝ) *
      ∫ θ in 0..π, f (cos θ) * (cos (n * θ) : ℂ) := by
  rw [complexCoefficient_eq_integral, ComplexCoefficientInput.ofContinuousOn_val, integral_measureT_complex_eq_integral_cos
    (f := fun x ↦ f x * (((T ℝ n).eval x : ℝ) : ℂ)) (hf.mul (by fun_prop))]
  simp only [T_real_cos, Int.cast_natCast]

/-- Imaginary parts commute with Chebyshev coefficients (ATAP, Chapter 3). -/
theorem complexCoefficient_im {f : ℝ → ℂ}
    (hf : ContinuousOn f (Set.Icc (-1) 1)) (n : ℕ) :
    (complexCoefficient (ComplexCoefficientInput.ofContinuousOn f hf n)).im = (coefficient (n := n) ⟨(fun x ↦ (f x).im), by first | assumption | apply integrable_classicalMeasureT; fun_prop⟩) := by
  have hi := integrable_measureT_complex (hf.mul (by fun_prop : ContinuousOn
    (fun x : ℝ ↦ (((T ℝ n).eval x : ℝ) : ℂ)) (Set.Icc (-1) 1)))
  have hr := integral_im hi
  change (∫ x, (f x * (((T ℝ n).eval x : ℝ) : ℂ)).im ∂measureT) =
    (∫ x, f x * (((T ℝ n).eval x : ℝ) : ℂ) ∂measureT).im at hr
  simp only [Complex.mul_im, Complex.ofReal_re, Complex.ofReal_im, mul_zero, zero_add] at hr
  rw [complexCoefficient_eq_integral, ComplexCoefficientInput.ofContinuousOn_val]
  simp only [Complex.mul_im, Complex.ofReal_re, Complex.ofReal_im, zero_mul, add_zero, ← hr]
  by_cases hn : n = 0
  · subst n
    simp [coefficient_zero, div_eq_mul_inv, mul_comm]
  · rw [coefficient_of_ne_zero _ hn]
    simp only [hn, ite_eq_right, not_false_eq_true]

/-- An absolutely summable complex Chebyshev series represents its continuous
function on the closed interval (ATAP, Chapters 4 and 8). -/
theorem hasSum_complexCoefficient_mul_eval_T {f : ℝ → ℂ}
    (hf : ContinuousOn f (Icc (-1) 1))
    (ha : Summable (fun n ↦ ‖(complexCoefficient (ComplexCoefficientInput.ofContinuousOn f hf n))‖))
    {x : ℝ} (hx : x ∈ Icc (-1) 1) :
    HasSum (fun n : ℕ ↦ (complexCoefficient (ComplexCoefficientInput.ofContinuousOn f hf n)) * (((T ℝ n).eval x : ℝ) : ℂ)) (f x) := by
  have hr : Summable (fun n ↦ |(coefficient (n := n) ⟨(fun x ↦ (f x).re), by first | assumption | apply integrable_classicalMeasureT; fun_prop⟩)|) :=
    ha.of_norm_bounded fun n ↦ by
      simpa only [Real.norm_eq_abs, abs_abs, ← complexCoefficient_re hf n] using
        Complex.abs_re_le_norm ((complexCoefficient (ComplexCoefficientInput.ofContinuousOn f hf n)))
  have hi : Summable (fun n ↦ |(coefficient (n := n) ⟨(fun x ↦ (f x).im), by first | assumption | apply integrable_classicalMeasureT; fun_prop⟩)|) :=
    ha.of_norm_bounded fun n ↦ by
      simpa only [Real.norm_eq_abs, abs_abs, ← complexCoefficient_im hf n] using
        Complex.abs_im_le_norm ((complexCoefficient (ComplexCoefficientInput.ofContinuousOn f hf n)))
  apply (Complex.hasSum_iff _ _).2
  constructor
  · simpa only [Complex.mul_re, Complex.ofReal_re, Complex.ofReal_im, mul_zero, sub_zero,
      complexCoefficient_re hf] using
      hasSum_coefficient_mul_eval_T (f := fun x ↦ (f x).re) (Complex.continuous_re.comp_continuousOn hf) hr hx
  · simpa only [Complex.mul_im, Complex.ofReal_re, Complex.ofReal_im, mul_zero, zero_add,
      complexCoefficient_im hf] using
      hasSum_coefficient_mul_eval_T (f := fun x ↦ (f x).im) (Complex.continuous_im.comp_continuousOn hf) hi hx

/-- Contour deformation for genuine integrable inputs with the given Laurent
integrands (ATAP, proof of Theorem 8.1). -/
theorem laurent_integral_eq_of_annulus {f : ℂ → ℂ} (r R : Set.Ioi (0 : ℝ))
    (hrR : r.val ≤ R.val)
    (hf : ∀ z ∈ closedBall (0 : ℂ) R.val \ ball 0 r.val, AnalyticAt ℂ f z) (n : ℕ)
    (gR : CircleIntegralInput 0 R.val) (gr : CircleIntegralInput 0 r.val)
    (hR : ∀ z, gR.val z = f z / z.val ^ (n + 1))
    (hrg : ∀ z, gr.val z = f z / z.val ^ (n + 1)) :
    circleIntegralOn gR = circleIntegralOn gr := by
  rw [circleIntegralOn_eq_circleIntegral gR (fun z => f z / z ^ (n + 1))
    (fun z => (hR z).symm),
    circleIntegralOn_eq_circleIntegral gr (fun z => f z / z ^ (n + 1))
    (fun z => (hrg z).symm)]
  exact laurent_integral_eq_of_annulus_circleIntegral r.property hrR hf n

/-- The open-annulus estimate on actual integrable contour inputs, without
assuming analyticity inside the inner circle (ATAP, Theorem 8.1). -/
theorem norm_laurent_integral_le_of_open_annulus {f : ℂ → ℂ} {M : ℝ} (ρ : Set.Ioi (1 : ℝ))
    (hf : ∀ z, 1 ≤ ‖z‖ → ‖z‖ < ρ.val → AnalyticAt ℂ f z)
    (hb : ∀ z, 1 ≤ ‖z‖ → ‖z‖ < ρ.val → ‖f z‖ ≤ M) (n : ℕ)
    (g : CircleIntegralInput 0 1)
    (hg : ∀ z, g.val z = f z / z.val ^ (n + 1)) :
    ‖(2 * Real.pi * I : ℂ)⁻¹ * circleIntegralOn g‖ ≤ M / ρ.val ^ n := by
  rw [circleIntegralOn_eq_circleIntegral g (fun z => f z / z ^ (n + 1))
    (fun z => (hg z).symm)]
  exact norm_laurent_integral_le_of_open_annulus_circleIntegral ρ.property hf hb n

/-- The classical sum is characterized by its partial-sum limit. -/
theorem complexChebyshevSeries_eq_of_tendsto {a : ℕ → ℂ}
    (z : ComplexChebyshevSeriesPoint a) {s : ℂ}
    (hs : Tendsto (fun N : ℕ ↦ ∑ n ∈ Finset.range N, a n * (T ℂ n).eval z.val)
      atTop (𝓝 s)) : complexChebyshevSeries a z = s :=
  tendsto_nhds_unique (tendsto_complexChebyshevSeries a z) hs

/-- Unconditional convergence supplies a point in the classical domain. -/
def ComplexChebyshevSeriesPoint.ofHasSum {a : ℕ → ℂ} {z s : ℂ}
    (hs : HasSum (fun n ↦ a n * (T ℂ n).eval z) s) : ComplexChebyshevSeriesPoint a :=
  ⟨z, s, hs.tendsto_sum_nat⟩

/-- Summability supplies a point in the classical domain. -/
def ComplexChebyshevSeriesPoint.ofSummable {a : ℕ → ℂ} {z : ℂ}
    (hs : Summable (fun n ↦ a n * (T ℂ n).eval z)) : ComplexChebyshevSeriesPoint a :=
  .ofHasSum hs.hasSum

/-- A supplied convergent sum is the classical value. -/
theorem complexChebyshevSeries_ofHasSum {a : ℕ → ℂ} {z s : ℂ}
    (hs : HasSum (fun n ↦ a n * (T ℂ n).eval z) s) :
    complexChebyshevSeries a (ComplexChebyshevSeriesPoint.ofHasSum hs) = s :=
  complexChebyshevSeries_eq_of_tendsto _ hs.tendsto_sum_nat

/-- The closure of a smaller Bernstein ellipse lies inside a larger open one. -/
theorem closure_bernsteinEllipse_subset {r ρ : ℝ} (hr : 1 < r) (hrρ : r < ρ) :
    closure (bernsteinEllipse ⟨r, hr⟩) ⊆ bernsteinEllipse ⟨ρ, hr.trans hrρ⟩ := by
  have hr0 : 0 < r := by linarith
  have hρ0 : 0 < ρ := by linarith
  have hlevel : r + r⁻¹ < ρ + ρ⁻¹ := by
    have heq : (ρ + ρ⁻¹ - (r + r⁻¹)) * (r * ρ) = (ρ - r) * (r * ρ - 1) := by
      field_simp
      ring
    have hp : 0 < (ρ - r) * (r * ρ - 1) := mul_pos (sub_pos.mpr hrρ) (by nlinarith)
    have hmul : 0 < r * ρ := mul_pos hr0 hρ0
    nlinarith
  have hcl : closure (bernsteinEllipse ⟨r, hr⟩) ⊆ {z : ℂ | ‖z - 1‖ + ‖z + 1‖ ≤ r + r⁻¹} :=
    closure_minimal (by
      intro z hz
      change ‖z - 1‖ + ‖z + 1‖ ≤ r + r⁻¹
      exact le_of_lt hz) (isClosed_le (by fun_prop) continuous_const)
  exact fun z hz ↦ (hcl hz).trans_lt hlevel

/-- Closed smaller ellipses are compact (ATAP, Chapter 8). -/
theorem isCompact_closure_bernsteinEllipse (r : Set.Ioi (1 : ℝ)) :
    IsCompact (closure (bernsteinEllipse r)) := by
  apply Metric.isCompact_of_isClosed_isBounded isClosed_closure
  apply Bornology.IsBounded.closure
  apply (Metric.isBounded_closedBall (x := (0 : ℂ)) (r := (r : ℝ) + (r : ℝ)⁻¹ + 1)).subset
  intro z hz
  have hn : ‖z‖ ≤ ‖z - 1‖ + 1 := by
    simpa using norm_add_le (z - 1) (1 : ℂ)
  simp only [Metric.mem_closedBall, dist_zero_right]
  change ‖z - 1‖ + ‖z + 1‖ < (r : ℝ) + (r : ℝ)⁻¹ at hz
  linarith [norm_nonneg (z + 1)]

/-- Chebyshev growth inside an open ellipse (ATAP, Exercise 8.8). -/
theorem norm_eval_T_le_on_bernsteinEllipse {r : ℝ} (hr : 1 < r) {z : ℂ}
    (hz : z ∈ bernsteinEllipse ⟨r, hr⟩) (n : ℕ) : ‖(T ℂ n).eval z‖ ≤ r ^ n := by
  rw [bernsteinEllipse_eq_image_annulus hr] at hz
  obtain ⟨w, hw, rfl⟩ := hz
  have hr0 : 0 < r := by linarith
  have hw0 : 0 < ‖w.val‖ := lt_trans (inv_pos.mpr hr0) hw.1
  have hi : ‖w.val‖⁻¹ < r := (inv_lt_comm₀ hw0 hr0).2 hw.1
  rw [eval_T_joukowski w, norm_div, norm_ofNat]
  apply (div_le_iff₀ (by norm_num : (0 : ℝ) < 2)).2
  have hn := norm_add_le (w.val ^ n) (w.val⁻¹ ^ n)
  rw [norm_pow, norm_pow, norm_inv] at hn
  have h1 := pow_le_pow_left₀ (norm_nonneg w.val) hw.2.le n
  have h2 := pow_le_pow_left₀ (inv_nonneg.mpr (norm_nonneg w.val)) hi.le n
  linarith

/-- Geometric decay gives absolute convergence at each point of the open ellipse. -/
theorem summable_chebyshevSeries_of_geometric {a : ℕ → ℂ} {C ρ : ℝ}
    (hρ : 1 < ρ) (ha : ∀ n, ‖a n‖ ≤ C / ρ ^ n)
    {z : ℂ} (hz : z ∈ bernsteinEllipse ⟨ρ, hρ⟩) :
    Summable (fun n ↦ a n * (T ℂ n).eval z) := by
  obtain ⟨r, hr, hrρ, hzr⟩ := exists_smaller_bernsteinEllipse hρ hz
  exact (summable_norm_chebyshevSeries hρ hr hrρ ha hzr).of_norm

/-- Geometric coefficient bounds supply the classical series domain on an ellipse. -/
noncomputable def ComplexChebyshevSeriesPoint.ofGeometric {a : ℕ → ℂ} {C ρ : ℝ}
    (hρ : 1 < ρ) (ha : ∀ n, ‖a n‖ ≤ C / ρ ^ n)
    (z : bernsteinEllipse ⟨ρ, hρ⟩) : ComplexChebyshevSeriesPoint a :=
  .ofSummable (summable_chebyshevSeries_of_geometric hρ ha z.property)

@[simp] theorem ComplexChebyshevSeriesPoint.ofGeometric_val {a : ℕ → ℂ} {C ρ : ℝ}
    (hρ : 1 < ρ) (ha : ∀ n, ‖a n‖ ≤ C / ρ ^ n) (z : bernsteinEllipse ⟨ρ, hρ⟩) :
    (ComplexChebyshevSeriesPoint.ofGeometric hρ ha z).val = z.val := rfl

/-- The Chebyshev extension is bounded on every strictly smaller ellipse. -/
theorem norm_complexChebyshevSeries_le {a : ℕ → ℂ} {C ρ r : ℝ}
    (hρ : 1 < ρ) (hr : 1 < r) (hrρ : r < ρ) (ha : ∀ n, ‖a n‖ ≤ C / ρ ^ n)
    {z : ComplexChebyshevSeriesPoint a} (hz : z.val ∈ bernsteinEllipse ⟨r, hr⟩) :
    ‖complexChebyshevSeries a z‖ ≤ C / (1 - r / ρ) := by
  have hs := summable_norm_chebyshevSeries hρ hr hrρ ha hz
  rw [complexChebyshevSeries_eq_tsum z hs.of_norm]
  have hq0 : 0 ≤ r / ρ := by positivity
  have hq1 : r / ρ < 1 := (div_lt_one (by linarith : 0 < ρ)).2 hrρ
  calc
    _ ≤ ∑' n, ‖a n * (T ℂ n).eval z.val‖ := norm_tsum_le_tsum_norm hs
    _ ≤ ∑' n, C * (r / ρ) ^ n := hs.tsum_le_tsum
      (fun n ↦ term_norm_le hρ hr ha hz n) ((summable_geometric_of_lt_one hq0 hq1).mul_left C)
    _ = _ := by rw [tsum_mul_left, tsum_geometric_of_lt_one hq0 hq1]; ring

/-- Geometric Chebyshev data are analytic on their typed open ellipse. -/
theorem analyticOnOpen_complexChebyshevSeries {a : ℕ → ℂ} {C ρ : ℝ}
    (hρ : 1 < ρ) (ha : ∀ n, ‖a n‖ ≤ C / ρ ^ n) :
    AnalyticOnOpen ⟨bernsteinEllipse ⟨ρ, hρ⟩, isOpen_bernsteinEllipse ⟨ρ, hρ⟩⟩
      (fun z ↦ complexChebyshevSeries a (ComplexChebyshevSeriesPoint.ofGeometric hρ ha z)) := by
  apply (analyticOnOpen_iff _ _ (fun z ↦ ∑' n : ℕ, a n * (T ℂ n).eval z) ?_).2
    (analyticOnNhd_chebyshev_tsum hρ ha)
  intro z
  have hz : z.val ∈ bernsteinEllipse ⟨ρ, hρ⟩ := z.property
  have hs := summable_chebyshevSeries_of_geometric hρ ha (z := z.val) hz
  exact (complexChebyshevSeries_eq_tsum
    (ComplexChebyshevSeriesPoint.ofGeometric hρ ha ⟨z.val, hz⟩)
    (by simpa only [ComplexChebyshevSeriesPoint.ofGeometric_val] using hs)).symm

/-- Subtraction commutes with complex Chebyshev coefficients (ATAP, Chapter 3). -/
theorem complexCoefficient_sub {f g : ℝ → ℂ}
    (hf : ContinuousOn f (Icc (-1) 1)) (hg : ContinuousOn g (Icc (-1) 1)) (n : ℕ) :
    (complexCoefficient (ComplexCoefficientInput.ofContinuousOn (fun x ↦ f x - g x) (by fun_prop) n)) =
      (complexCoefficient (ComplexCoefficientInput.ofContinuousOn f hf n)) - (complexCoefficient (ComplexCoefficientInput.ofContinuousOn g hg n)) := by
  rw [complexCoefficient_eq_integral_cos (f := fun x ↦ f x - g x) (hf.sub hg), complexCoefficient_eq_integral_cos hf,
    complexCoefficient_eq_integral_cos hg]
  simp_rw [sub_mul]
  rw [intervalIntegral.integral_sub (cosine_integrable hf n) (cosine_integrable hg n), mul_sub]

/-- Complex scalars commute with coefficients (ATAP, Chapter 3). -/
theorem complexCoefficient_const_mul (c : ℂ) {f : ℝ → ℂ}
    (hf : ContinuousOn f (Icc (-1) 1)) (n : ℕ) :
    (complexCoefficient (ComplexCoefficientInput.ofContinuousOn (fun x ↦ c * f x) (by fun_prop) n)) = c * (complexCoefficient (ComplexCoefficientInput.ofContinuousOn f hf n)) := by
  rw [complexCoefficient_eq_integral_cos (f := fun x ↦ c * f x) (continuousOn_const.mul hf),
    complexCoefficient_eq_integral_cos hf]
  simp_rw [mul_assoc]
  rw [intervalIntegral.integral_const_mul]
  ring

/-- Finite sums commute with coefficients (ATAP, Chapter 3). -/
theorem complexCoefficient_sum {ι : Type*} (s : Finset ι) {f : ι → ℝ → ℂ}
    (hf : ∀ i ∈ s, ContinuousOn (f i) (Icc (-1) 1)) (n : ℕ) :
    complexCoefficient (ComplexCoefficientInput.ofContinuousOn
      (fun x ↦ ∑ i ∈ s, f i x) (continuousOn_finsetSum _ hf) n) =
      ∑ i : ↥s, complexCoefficient
        (ComplexCoefficientInput.ofContinuousOn (f i) (hf i i.property) n) := by
  rw [complexCoefficient_eq_integral_cos]
  simp_rw [Finset.sum_mul]
  rw [intervalIntegral.integral_finsetSum (fun i hi ↦ cosine_integrable (hf i hi) n),
    Finset.mul_sum, ← s.sum_attach]
  apply Finset.sum_congr rfl
  intro i hi
  exact (complexCoefficient_eq_integral_cos (hf i i.property) n).symm

/-- A Chebyshev polynomial has exactly its matching complex coefficient. -/
@[simp] theorem complexCoefficient_eval_T (m n : ℕ) :
    (complexCoefficient (ComplexCoefficientInput.ofContinuousOn (fun x : ℝ ↦ (T ℂ m).eval (x : ℂ)) (by fun_prop) n)) = if m = n then 1 else 0 := by
  simp_rw [← complex_ofReal_eval_T]
  have h := (complexCoefficient_ofReal (CoefficientInput.ofContinuousOn
    (fun x ↦ (T ℝ m).eval x) (by fun_prop) n)).trans
      (congrArg (fun r : ℝ ↦ (r : ℂ)) (coefficient_eval_T m n))
  split_ifs with hmn <;> simpa [complexCoefficient, ComplexCoefficientInput.ofContinuousOn, ComplexCoefficientInput.ofL1, ComplexCoefficientInput.ofReal, CoefficientInput.ofContinuousOn, CoefficientInput.ofL1, hmn] using h

/-- A complex polynomial has no Chebyshev coefficient above its degree (ATAP 3). -/
theorem complexCoefficient_polynomial_eq_zero {p : ℂ[X]} {n : ℕ} (hp : p.degree < n) :
    (complexCoefficient (ComplexCoefficientInput.ofContinuousOn (fun x : ℝ ↦ p.eval (x : ℂ)) (by fun_prop) n)) = 0 := by
  classical
  let P := chebyshevTsequence ℂ
  let c := (P.basis P.isUnit_leadingCoeff).repr p
  have he : p = ∑ i : Fin n, c i • T ℂ (i : ℕ) := (P.sum_fin_repr hp).symm
  rw [he]
  simp only [eval_finsetSum, eval_smul, smul_eq_mul]
  rw [complexCoefficient_sum _ (fun i _ ↦ by fun_prop)]
  apply Finset.sum_eq_zero
  intro i _
  rw [complexCoefficient_const_mul _ (by fun_prop), complexCoefficient_eval_T,
    ite_eq_right (ne_of_lt i.val.isLt), mul_zero]