/-- Continuous functions are integrable for the second-kind weight (DLMF Table 18.3.1). -/
theorem integrable_measureU {f : ℝ → ℝ} (hf : ContinuousOn f (Set.Icc (-1) 1)) :
    Integrable f measureU := by
  have hi : IntervalIntegrable (fun x ↦ √(1 - x ^ 2) * f x) volume (-1) 1 :=
    ContinuousOn.intervalIntegrable (by
      rw [Set.uIcc_of_le (by norm_num : (-1 : ℝ) ≤ 1)]
      exact (by fun_prop : ContinuousOn (fun x : ℝ ↦ √(1 - x ^ 2)) _).mul hf)
  rw [intervalIntegrable_iff, Set.uIoc_of_le (by norm_num : (-1 : ℝ) ≤ 1)] at hi
  rw [integrable_measureU_iff]
  rw [IntegrableOn, ← restrict_Ioo_eq_restrict_Ioc] at hi
  exact (integrableOn_iff_comap_subtypeVal measurableSet_Ioo).1 hi

/-- Comparison of weights preserves integrability as well as the integral value. -/
theorem integral_measureU_eq_classicalMeasureT
    (f : IntegrableInput measureU) :
    Integrable (fun x ↦ f.val x * (1 - x ^ 2)) classicalMeasureT ∧
      (∫ x, f.val x ∂measureU) =
        ∫ x, f.val x * (1 - x ^ 2) ∂classicalMeasureT := by
  have h : Integrable (fun x ↦ f.val x * (1 - x ^ 2)) classicalMeasureT := by
    rw [integrable_classicalMeasureT_iff]
    convert (integrable_measureU_iff _).1 f.property using 1
    ext x
    rw [weightU_eq_weightT_mul]
    ring
  refine ⟨h, ?_⟩
  rw [integral_measureU]
  have he := integral_openIntervalWeightMeasure (-1) 1 weightT
    (⟨_, h⟩ : IntegrableInput classicalMeasureT)
  apply Eq.trans _ he.symm
  apply integral_congr_ae
  filter_upwards [] with x
  rw [weightU_eq_weightT_mul]
  ring

/-- Product integral reduction to first-kind Chebyshev moments; DLMF Table 18.3.1
and the trigonometric representations in DLMF 18.5.1--18.5.2. -/
theorem integral_eval_U_real_mul_eval_U_real_measureU (n m : ℤ) :
    ∫ x, (U ℝ n).eval x * (U ℝ m).eval x ∂measureU =
      ((∫ x, (T ℝ (n - m)).eval x ∂classicalMeasureT) -
       (∫ x, (T ℝ (n + m + 2)).eval x ∂classicalMeasureT)) / 2 := by
  rw [classicalMeasureT_eq]
  have h := (integral_measureU_eq_classicalMeasureT
    ⟨fun x ↦ (U ℝ n).eval x * (U ℝ m).eval x, integrable_measureU (by fun_prop)⟩).2
  rw [classicalMeasureT_eq] at h
  rw [h]
  rw [← MeasureTheory.integral_sub (integrable_measureT (by fun_prop))
    (integrable_measureT (by fun_prop)), ← MeasureTheory.integral_div]
  rw [integral_measureT_eq_integral_cos, integral_measureT_eq_integral_cos]
  apply intervalIntegral.integral_congr
  intro θ hθ
  simp only [T_real_cos]
  have hn := U_real_cos (n := n) (θ := θ)
  have hm := U_real_cos (n := m) (θ := θ)
  have hs := Real.sin_sq_add_cos_sq θ
  have hp := Real.two_mul_sin_mul_sin (((n : ℝ) + 1) * θ) (((m : ℝ) + 1) * θ)
  have hsub : ((n : ℝ) + 1) * θ - ((m : ℝ) + 1) * θ = (n - m) * θ := by ring
  have hadd : ((n : ℝ) + 1) * θ + ((m : ℝ) + 1) * θ = (n + m + 2) * θ := by ring
  rw [hsub, hadd] at hp
  push_cast
  calc
    _ = ((U ℝ n).eval (cos θ) * sin θ) * ((U ℝ m).eval (cos θ) * sin θ) := by
      rw [show 1 - cos θ ^ 2 = sin θ ^ 2 by nlinarith [hs]]
      ring
    _ = sin (((n : ℝ) + 1) * θ) * sin (((m : ℝ) + 1) * θ) := by rw [hn, hm]
    _ = _ := by linarith [hp]