ChebyshevLobattoPositiveWeights: mathematical reading route

Mathematical statement

For every integer J≥2, every real h>0 and every j in Fin J, with t_i=(h/2)(1-cos(i*pi/(J-1))) and ell_j=Lagrange.basis univ t j, the actual momentum weight omega_j=integral_0^h ell_j(s) ds is nonnegative.

theorem nonnegative_momentum_weights {J : ℕ} (hJ : 2 ≤ J) {h : ℝ} (hh : 0<h) :
    let t := fun i : Fin J => h/2*(1-Real.cos ((i : ℝ)/(J-1 : ℝ)*Real.pi))
    let ell := fun j : Fin J => Lagrange.basis univ t j
    ∀ j, 0 ≤ ∫ s in (0 : ℝ)..h, (ell j).eval s

Proof roadmap

1. 1Work with the actual extrema, keeping endpoint factors

   Put n=J-1≥1, theta_i=i*pi/n and c_i=1 at i=0,n and2 otherwise. Define C_n(a)=2 sum_(k=0)^n cos(ka)-1-cos(na). A finite sine telescope gives sin(a/2)C_n(a)=cos(a/2)sin(na). At all integer multiples m*pi/n with0≤m≤2n, C_n is2n at m=0,2n and0 otherwise. The interior sine factor is strictly positive, so division is justified. Negative differences use evenness.

2. 2Derive the finite cardinal polynomial, rather than assume it

   The cosine product identity gives twice the product sum as C_n(a-b)+C_n(a+b). Hence P_i(x)=c_i/(2n)[2 sum_(k=0)^n cos(k theta_i)T_k(x)-1-cos(n theta_i)T_n(x)] has degree≤n and value1 at its own cos(theta_i) node and0 at every other node. Both endpoint factors and n=1 are included. Chebyshev T_k(cos a)=cos(ka) is a pinned Mathlib fact.

3. 3Compute ordinary Lebesgue moments by an antiderivative

   For integer k different from ±1, F_k=T_(k+1)/(2(k+1))-T_(k-1)/(2(k-1)) has derivative T_k, using the polynomial derivative/U recurrence. The genuine FTC on[-1,1] yields I_k=integral T_k=(1+(-1)^k)/(1-k²). The exceptional k=1 integral is zero directly; I_0=2. Thus odd positive moments vanish, and even k≥2 give -2/(k²-1). No Chebyshev weighted measure or Gauss zeros are substituted.

4. 4Keep both parities in the strict absolute-moment budget

   For A_m=sum_(k=1)^m |I_k|, the even moments telescope since2/(4r²-1)=1/(2r-1)-1/(2r+1). Two-step induction proves A_m=1-1/(m+1) if m is even, and1-1/m if m is odd. It includes m=0, with A_0=0, and gives A_m<1 for every m.

5. 5Integrate the actual finite cardinal polynomial and prove positivity

   Continuity supplies all interval-integrability conditions for finite-sum and subtraction linearity. The integrated bracket is B_i=2+2 sum_(k=1)^(n-1) cos(k theta_i)I_k+cos(n theta_i)I_n. Since |cos|≤1, B_i≥2-2 A_(n-1)-|I_n|≥2-2 A_n>0. Multiplying by the strictly positive c_i/(2n) proves integral_(-1)^1 P_i>0 for every actual node. The empty interior sum handles n=1.

6. 6Identify the exact source basis and scale its actual integral

   Use x=1-2s/h. P_i(1-2s/h) has degree≤J-1 and the actual source cardinal values. The existing compiled coefficient producer supplies injectivity of the original t_i; polynomial interpolation uniqueness then identifies P_i(1-2s/h)=ell_i(s), with all natural/real J-1 casts checked. The genuine interval-integral affine substitution, including reversed extrema ordering, gives omega_i=(h/2) integral_(-1)^1 P_i>0 and hence the source nonnegativity conclusion. h>0 justifies the affine inverse.