Orthogonality of Chebyshev polynomials

Stream: maths

[Yuval Filmus]

The Chebyshev polynomials of the first kind are orthogonal with respect to the weight function 1/sqrt(1-x^2) restricted to (-1,1). The proof is a simple substitution.
One can then define a corresponding inner product on polynomials, and construct an orthogonal (or even an orthonormal) basis for the linear space of all polynomials (of bounded or arbitrary degree).
Similarly, Chebyshev polynomials of the second kind are orthogonal with respect to the weight function sqrt(1-x^2).

How do I express all of these in Mathlib?
(I got lost looking at the documentation.)
Note that there is a definition of a line integral but (1) it's not clear where the measure is hiding, and (2) it is defined on a half-closed interval, but here it seems we want the open interval (-1, 1).

[Weiyi Wang]

I have never tried this before but my first reaction to this is

• define the weight function as "1/sqrt(1-x^2) if x in (-1, 1), 0 otherwise"
• either docs#MeasureTheory.integral using the volume measure and the weight function multiplied to the integrant
• or use docs#MeasureTheory.Measure.withDensity with the weight function to construct the measure, and integrate using that
  (The two approaches are equivalent, shown by docs#integral_withDensity_eq_integral_smul)

[Yuval Filmus]

It seems extremely difficult due to the complete lack of documentation.
I wouldn't even know how to show that the integral of x^2 from 0 to 1 equals 1/2, let alone working with the Bochner integral rather than the line integral.
Is there an example of how to use these extremely general notions in a simple, concrete situation?
I sometimes feel that Mathlib is too general to be useful in particular cases.

[Ruben Van de Velde]

Yuval Filmus said:

It seems extremely difficult due to the complete lack of documentation.
I wouldn't even know how to show that the integral of x^2 from 0 to 1 equals 1/2, let alone working with the Bochner integral rather than the line integral.
Is there an example of how to use these extremely general notions in a simple, concrete situation?
I sometimes feel that Mathlib is too general to be useful in particular cases.

I don't know either, but I can prove it equals 1/3 :)

import Mathlib

example : ∫ x in (0 : ℝ)..1, x ^ 2 = 1 / 3 := by
  norm_num

[Kim Morrison]

Apologies to everyone who already knows this, but I think every time someone posts "I wouldn't know how to do X" and the following solutions works, it's worth reminding again:

import Mathlib

example : ∫ x in (0 : ℝ)..1, x ^ 2 = 1 / 3 := by try?

which outputs

Try these:
  bound
  norm_num

[Ruben Van de Velde]

I would, if I could remember it myself :sweat_smile:

[Patrick Massot]

Yuval Filmus said:

It seems extremely difficult due to the complete lack of documentation.
I wouldn't even know how to show that the integral of x^2 from 0 to 1 equals 1/2, let alone working with the Bochner integral rather than the line integral.
Is there an example of how to use these extremely general notions in a simple, concrete situation?
I sometimes feel that Mathlib is too general to be useful in particular cases.

I know it is not perfect, but did you look at https://leanprover-community.github.io/mathematics_in_lean/C13_Integration_and_Measure_Theory.html? We should probably revise the first section. It used to contain more computation examples in the Lean 3 days. But when we ported the book in the very early days of Lean 4, the simplifier had bugs that broke those examples. I’m sure they could be restored now.

[Yuval Filmus]

@Patrick Massot Thanks, forgot about that resource!
I ended up hacking together something in #33676.
Not sure what's the best way to document Mathlib.

One option is to add "tutorials" on common topics.
In this case, (interval) integrals would be introduced, with common operations on them, how to show integrability, and more complicated stuff such as integration by parts, substitution, the fundamental theorem of calculus, and so on (basically, going over the different files).
Not sure where such tutorials would fit, and who should write them (probably someone who knows Mathlib better than me!).

[Patrick Massot]

Ideally this would all be discussed in MIL, but they authors are too busy :sad:

[Snir Broshi]

Yuval Filmus said:

Not sure what's the best way to document Mathlib.

One option is to add "tutorials" on common topics.
...
Not sure where such tutorials would fit, and who should write them (probably someone who knows Mathlib better than me!).

Check out #mathlib4 > Mathlib: the Missing Manuals and #mathlib4 > Discussion: Mathlib documentation overview, you can suggest such missing tutorials