## Stream: general

### Topic: Lagrange interpolation #2600

#### Kenny Lau (May 20 2020 at 11:07):

What should the type signature be? Should I take f : F \to\0 F with a prescribed domain dom : finset F, or should I take a function f : (\u dom : set F) \to F?

#### Kenny Lau (May 20 2020 at 11:08):

first approach: I did not use F \to F because F \to\0 F has more API (e.g. finsupp.single)

#### Kenny Lau (May 20 2020 at 11:08):

second approach: this allows us to define an equivalence with the polynomials of degree \le n

#### Reid Barton (May 20 2020 at 11:09):

I vote for the second approach

#### Kenny Lau (May 20 2020 at 11:09):

Like this for the first approach.

#### Kenny Lau (May 20 2020 at 11:09):

Like this for the second approach.

#### Reid Barton (May 20 2020 at 11:10):

Wait, I don't think the first approach even works, does it? How would you require the interpolated polynomial to be zero at some points?

#### Reid Barton (May 20 2020 at 11:10):

Do I not understand what you are proposing?

#### Kenny Lau (May 20 2020 at 11:11):

/-- Lagrange interpolation. -/
def interpolate (f : F →₀ F) (dom : finset F) : polynomial F :=
dom.sum \$ λ x, basis dom (f x)


#### Kenny Lau (May 20 2020 at 11:11):

maybe we can define a new type altogether

#### Kenny Lau (May 20 2020 at 11:11):

where a function includes the domain

Oh I see.

#### Reid Barton (May 20 2020 at 11:12):

It seems that your question is basically: if I know \a is finite, should I use \a ->0 \b or \a -> \b.

#### Kenny Lau (May 20 2020 at 11:12):

but F isn't finite

#### Kenny Lau (May 20 2020 at 11:13):

and we hate partial functions

#### Reid Barton (May 20 2020 at 11:13):

But the dom is finite

#### Reid Barton (May 20 2020 at 11:13):

This is stupid, please stop the partial function hate.

#### Reid Barton (May 20 2020 at 11:13):

Seriously they are fine.

#### Kenny Lau (May 20 2020 at 11:31):

@Johan Commelin what did you have in mind when you made the issue?

#### Johan Commelin (May 20 2020 at 12:18):

What I had in mind was that someone who didn't have much experience with lean could try to come up with a statement and PR things (-;

#### Johan Commelin (May 20 2020 at 12:18):

I don't have a preference, and feel free to just do something

#### Johan Commelin (May 20 2020 at 12:23):

Clearly, the topic wasn't claimed for a while... so I don't mind that someonewith experience takes it up.

#### Kenny Lau (May 20 2020 at 12:55):

I don't have more experience than you

#### Johan Commelin (May 20 2020 at 12:55):

You do have more experience than a beginner (-;

#### Kenny Lau (May 20 2020 at 12:56):

oh I misread, I thought you wanted someone with experience to do it

#### Kenny Lau (May 20 2020 at 12:58):

Reid Barton said:

This is stupid, please stop the partial function hate.

the problem is that you run into f x and f \<x.1, x.2\> not being defeq

#### Kenny Lau (May 20 2020 at 13:00):

the third option is that we make something like finsupp but with a specified domain

#### Kenny Lau (May 20 2020 at 13:00):

so essentially a new data structure

Why the finsupp?

#### Johan Commelin (May 20 2020 at 13:03):

Why not just a function + a finset

#### Kenny Lau (May 20 2020 at 13:03):

you can only interpolate finitely many points

#### Kenny Lau (May 20 2020 at 13:03):

oh that's because finsupp has better API

#### Johan Commelin (May 20 2020 at 13:03):

finset.sum also take a function

not a finsupp

#### Kenny Lau (May 20 2020 at 13:04):

and you can decompose a finsupp into singles

#### Kenny Lau (May 20 2020 at 13:04):

it just feels nicer to me

#### Johan Commelin (May 20 2020 at 13:04):

I don't really care, like I said. (-;

#### Kenny Lau (May 20 2020 at 13:04):

but maybe I'll just use partial functions

#### Sebastien Gouezel (May 20 2020 at 13:11):

Partial functions are especially bad when you start intersecting the domains, like you do all the time in manifolds, as (A ∩ B) ∩ C is not defeq to A ∩ (B ∩ C) nor to B ∩ (A ∩ C) and so on, so you spend all your time casting from one of them to the other.

#### Kenny Lau (May 20 2020 at 13:12):

oh no, lagrange interpolation is a sheaf now?

#### Kenny Lau (May 20 2020 at 13:12):

yeah I might run into this problem if I do the Newton interpolations

#### Reid Barton (May 20 2020 at 15:14):

It seems to me the statement is: for every finite subset s of cardinality n, there's an F-linear map from {polynomials of degree less than n} to {functions s -> F}, given by evaluation; this map is a bijection/isomorphism/(linear) equivalence.

#### Mario Carneiro (May 20 2020 at 15:23):

how about something even more explicitly computable, e.g. finmap?

#### Mario Carneiro (May 20 2020 at 15:23):

the input is just a list of pairs here

#### Reid Barton (May 20 2020 at 15:24):

The set s needs to be fixed anyways though, for this statement

why?

#### Mario Carneiro (May 20 2020 at 15:24):

given a map, produce a polynomial

#### Mario Carneiro (May 20 2020 at 15:25):

you can build all the more noncomputable representations on top of this

#### Reid Barton (May 20 2020 at 15:28):

Yes, you can also phrase it in this low-level way but in the end you will want to have the k-linear isomorphism.

#### Reid Barton (May 20 2020 at 15:38):

Another useful way to say it is that for a fixed s of size n, there's a basis of {polynomials of degree less than n} indexed on s whose values on s are the characteristic functions of the various elements of s.

#### Reid Barton (May 21 2020 at 10:42):

Reid Barton said:

It seems to me the statement is: for every finite subset s of cardinality n, there's an F-linear map from {polynomials of degree less than n} to {functions s -> F}, given by evaluation; this map is a bijection/isomorphism/(linear) equivalence.

This formulation also makes the proof trivial: the original map has kernel zero, and both sides have an obvious basis of size n.

Last updated: Dec 20 2023 at 11:08 UTC