Lagrange interpolation #2600

Stream: general

[Kenny Lau]

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]

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

[Kenny Lau]

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

[Reid Barton]

I vote for the second approach

[Kenny Lau]

Like this for the first approach.

[Kenny Lau]

Like this for the second approach.

[Reid Barton]

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]

Do I not understand what you are proposing?

[Kenny Lau]

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

[Kenny Lau]

maybe we can define a new type altogether

[Kenny Lau]

where a function includes the domain

[Reid Barton]

Oh I see.

[Reid Barton]

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

[Kenny Lau]

but F isn't finite

[Kenny Lau]

and we hate partial functions

[Reid Barton]

But the dom is finite

[Reid Barton]

This is stupid, please stop the partial function hate.

[Reid Barton]

Seriously they are fine.

[Kenny Lau]

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

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Kenny Lau]

I don't have more experience than you

[Johan Commelin]

You do have more experience than a beginner (-;

[Kenny Lau]

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

[Kenny Lau]

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]

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

[Kenny Lau]

so essentially a new data structure

[Johan Commelin]

Why the finsupp?

[Johan Commelin]

Why not just a function + a finset

[Kenny Lau]

you can only interpolate finitely many points

[Kenny Lau]

oh that's because finsupp has better API

[Johan Commelin]

finset.sum also take a function

[Johan Commelin]

not a finsupp

[Kenny Lau]

and you can decompose a finsupp into singles

[Kenny Lau]

it just feels nicer to me

[Johan Commelin]

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

[Kenny Lau]

but maybe I'll just use partial functions

[Sebastien Gouezel]

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]

oh no, lagrange interpolation is a sheaf now?

[Kenny Lau]

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

[Reid Barton]

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]

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

[Mario Carneiro]

the input is just a list of pairs here

[Reid Barton]

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

[Mario Carneiro]

why?

[Mario Carneiro]

given a map, produce a polynomial

[Mario Carneiro]

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

[Reid Barton]

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]

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]

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.