Lagrange interpolants

Stream: maths

[Wrenna Robson]

I'm picking back up some work I was doing with https://leanprover-community.github.io/mathlib_docs/linear_algebra/lagrange.html.

One issue I have here is that, quite commonly, one wants to talk of a (finite) set of interpolation points, and the values they take at those points.

Naively, I would think to represent this as an (injective) map from a fintype to my field, and then a separate map from my fintype to the field, representing the point and their values.

The difficulty with this is that it's difficult to then take "the product over the fintype for all j \= to some (fixed) i", which is relevant in the interpolation. And indeed, in the above, we define the interpolation for a finset in particular. The difficulty then is that my finset, as well as being a set of points in my field, also ends up indexing, say, the values a polynomial takes on them.

This also has the effect of impose a decidable_eq constraint on the field which I'm not sure is warranted: I think this comes from the use of "finset.erase", but really what is necessary is that you have decidable equality on your indexing finset/fintype.

Do you see my issue? What do you think the best way to solve this would be? Is it worth re-factoring https://leanprover-community.github.io/mathlib_docs/linear_algebra/lagrange.html in order to remove this decidable_eq constraint on the field (which as I say I am not sure is necessary)?

[Junyan Xu]

You can get rid of decidable_eq by going back to the underlying list of the finset, and if you define docs#lagrange.basis using docs#list.prod and docs#lagrange.interpolate using docs#list.sum you don't need decidable_eq, as you can remove the nth element from a list without decidable_eq. If you then show the resulting Lagrange polnomial is independent of the list (a chosen ordering) then it descends to a function on finset F.
I'm not sure you should worry too much about dicidable_eq though. docs#polynomial.X and docs#polynomial.C are already noncomputable (boils down to docs#finsupp.single being noncomputable), but I'd expect the above definition should unfold/reduce/eval(?) more nicely than the current one; if you have a computable finset I think it can be definitionally reduce to an expression involving X and C without decidable_eq.

[Wrenna Robson]

I've been playing around with something which I'm more or less ready to share. How do I create PRs which depend on one another?

[Wrenna Robson]

(tl;dr doing everything on fintypes seems very viable, matches with mv_polynomial in some nice ways, and gives shorter proofs most of the time)

[Wrenna Robson]

Actually, you know what, if I factor this in the right way, it won't matter.

[Wrenna Robson]

https://github.com/leanprover-community/mathlib/pull/15036

[Wrenna Robson]

Here - I decided it would just be easier to do the refactor and then people could comment on it.

The issue, by the way, isn't the decidable equality of the finset in the way I think you are describing, @Junyan Xu. The previous formulation needed decidable equality of the whole field: that's extremely strong compared to, say, decidable equality of fin n.

[Wrenna Robson]

If you index things injectively by a decidably equal fintype, then you don't care about equality on the field.

[Junyan Xu]

Well an injective function from fin n is equivalent to an ordering on the finset, namely a list. However it's indeed weird that docs#lagrange.interpolate takes a function from F to F, and your PR would allow a function from the finset/fintype to F, which seems better. And I agree that using an indexing type might be more convenient in some cases.

[Wrenna Robson]

Indeed, but I have injective functions from arbitrary fintypes (fin n is just the obvious special case).

[Stuart Presnell]

Wrenna Robson said:

How do I create PRs which depend on one another?

One way to do this (perhaps not simplest or most efficient, idk) is to create the first PR (e.g. in branch my_branch_one) then open a new branch for the dependent PR and do git merge my_branch_one. Then when you create a PR from the second branch, add a line in the comments indicating the dependency, e.g. - [ ] depends on: #54321 [Using stuff from my first branch].

[Wrenna Robson]

Thanks for the review @Violeta Hernández

[Wrenna Robson]

as you noticed I had throughly de-simped it, so thanks for the skutwork.

[Wrenna Robson]

interpolate_eq_interpolate_erase_add has proved challenging to translate into this refactor. I am inclined to ditch it - there are I think other things one might want to prove about the Lagrange interpolants (for instance, other ways of constructing them) but my suspicion is that there will be better routes to this.

[Wrenna Robson]

I'm not sure how we handle operating over a subtype of a fintype acting as an index, in general.

[Yaël Dillies]

I would strongly advise you to not use an indexing fintype, but instead a finset inside an indexing type.

[Yaël Dillies]

This makes adding/removing elements less awkward and lets you take finsets in the field by considering the field itself as the indexing type.

[Eric Wieser]

@Wrenna Robson; these Zulip discussions are great, but can you make sure to link the PR from the Zulip thread (#15036?) and vice versa in future? It makes it easier to track what's going on!

[Wrenna Robson]

Ah, so the link here is fine, but I need to link it back the other way?

[Wrenna Robson]

@Yaël Dillies that's a nice idea, I see the logic of it. How do you pair up nodes and values using that approach?

[Yaël Dillies]

It would be more readable if you were writing #15036 instead of https://github.com/leanprover-community/mathlib/pull/15036

[Wrenna Robson]

Right - and what about the link back?

[Yaël Dillies]

Wrenna Robson said:

Yaël Dillies that's a nice idea, I see the logic of it. How do you pair up nodes and values using that approach?

Have them both be indexed families indexed by the same finset?

[Yaël Dillies]

Write something like Zulip

[Wrenna Robson]

Hmm - the thing is that sometimes it is really natural to consider these things as fin n -> tuples, rather than, say, going from finset.range (which I think is what you would do with that approach).

[Yaël Dillies]

You can always index them by univ : finset (fin n).

[Wrenna Robson]

The question I suppose is how this stuff is to be used - it isn't currently and I can only testify from my use-case.

[Wrenna Robson]

(in which there's little need for adding/removing points)

[Yaël Dillies]

Please please please give it a try. I've add extensive experience with similar things and finset-indexed families are by far the least painful.

[Wrenna Robson]

I'll certainly have a go - do you have a link to something that uses a similar approach so I have something to model off?

[Wrenna Robson]

I've seen plenty of fintype-indexed stuff but much less finset-indexed stuff.

[Eric Wieser]

docs#finpartition comes to mind oh, that's not indexed

[Eric Wieser]

Apologies, I totally missed that you had already linked to the PR above!

[Wrenna Robson]

No worries - it would be a bit odd of me if I hadn't for sure.

[Yaël Dillies]

Typically, docs#finset.sum

[Eric Wieser]

Also docs#finset.sup

[Eric Wieser]

This case is a bit unusual though because the map has to be injective, so the only motivation for this refactor seems to be one of computability?

[Wrenna Robson]

No

[Wrenna Robson]

It's also because the current version interpolates over a whole function F -> F. But this is an unusual place to start.

[Eric Wieser]

Doesn't it let you specify an arbitrary finset of F?

[Wrenna Robson]

As the nodal points.

[Wrenna Robson]

What's more usual is the following: you have some nodal points, which I'll index in the obvious way but we understand that it could be more general: x_1, x_2, ..., x_n. You have some values, r_1, ..., r_n. You construct a polynomial p of minimal degree such that p(x_i) = r_i.

[Eric Wieser]

Ah. I missed that you needed to match up elements of two finsets

[Wrenna Robson]

The current formulation is the following: given some finset s, and some function f : F -> F, construct a polynomial p of minimal degree such that p(x) = f(x) for all x in s

[Wrenna Robson]

Yes - it's the matching up which is the tricky part, and why I've reformulated in the way that I did, after thinking about it and trying a few things. It ran through very smooth this way.

[Eric Wieser]

I think what Yaël is proposing is roughly (s : finset ι) (x : ι ↪ F) (r : ι → F)?

[Wrenna Robson]

And actually btw - the second lot isn't a finset necessarily: they don't have to be distinct.

[Yaël Dillies]

or (s : finset F) (r : F → F)

[Eric Wieser]

That's what we have today

[Wrenna Robson]

Yes: I don't want r: F -> F. That's just what we already have, and it isn't useful in my actual context to do the actual maths you want to do with this

[Wrenna Robson]

What you describe there is nearly what I have, Eric - though I'm not sure how the finset gets folded in.

[Eric Wieser]

It's the union of what you have and what we had before

[Wrenna Robson]

Yes. I mean I'm perfectly happy to find something that works for everyone - but I have found my formulation very straightforward to work with and it works for my context. I do agree that erasing or adding nodes is hard though - it could be nice to fix that.

[Eric Wieser]

One other thing to consider; (s : finset F) (r : F → F) in this case can be represented neatly as r' : F →₀ F

[Wrenna Robson]

Yes, I had actually wondered about the use of finsupps somehow.

[Eric Wieser]

And then my spelling above amounts to having r' = r.map_domain f (docs#finsupp.map_domain)

[Wrenna Robson]

A key test I would like to try is if my definition of the interpolant is compatible with, say, the construction of the interpolant using the derivative (I already have some work doing this, using current-mathlib).

[Wrenna Robson]

This sort of thing does often leave you wanting to erase stuff from sums.

[Junyan Xu]

How does finsupp work? If you use finsupp you can't specify any element to be mapped to 0.

[Wrenna Robson]

Yeah I mean that is the issue - you want to lead values outside the nodal values unspecified.

[Wrenna Robson]

That's why I am suspicious of anything that starts with F -> F: clearly that's a thing you want to be able to work with, that's why I define interpolate_at.

[Wrenna Robson]

But I'm not sure it should be the core definition.

[Eric Wieser]

Whoops. Clutching at straws, F →₀ with_zero F ought to be a faithful representation, but I doubt it's useful

[Wrenna Robson]

Yes that sounds highly suspect. Again, in the context I am working in - I'm not going to fully explain it but, it's Goppa codes, it's always Goppa codes, I hate it, free me from this ahem - you really do have like, a fixed number of points that you care about, and those points are fixed.

[Wrenna Robson]

That's why - look you can say "ho ho ho I'm very good at Lean and this works better" all you like but I did do it this way for a reason - just picking some fintype or finset or whatever, fixing that, and using that to index is very natural.

[Wrenna Robson]

Ultimately if you pick a finset I think you're going to want to be thinking about functions from it anyway and then you're just promoting it to a type.

[Eric Wieser]

I don't disagree, I just wonder if we're missing some primitive collection type

[Wrenna Robson]

Cotton?

[Wrenna Robson]

Oh I see. I mean I suppose, technically, all I need is some labels for my nodes and they don't have to be homogeneous? So maybe there's some absolutely demented ways of labelling them with heterogeneous types.

[Wrenna Robson]

But uh - I don't want to. <_<

[Wrenna Robson]

I will say that I did first of all try indexing the values with the node finset. It just ended up a lot messier and I kept fighting against myself.

[Eric Wieser]

What I'm curious about is whether something like

structure indexed_dict :=
(s : finset ι)
(keys : ι ↪ α)
(values : ι → β)

def indexed_dict.get (a : α) : option β :=
-- computable by enumeration

is a useful abstraction for this kind of problem

[Wrenna Robson]

I'm not sure I understand the role that s has here.

[Wrenna Robson]

(Incidentally, this is a side point, I think one reason it is nice to get more computability here even though at the current time it doesn't matter, is that in some future Lean 4 world where we're actually doing computation, somebody is going to want to write a numerical methods library and at that time they'll thank us if the interpolant works nicely.)

[Eric Wieser]

(they'll be very annoyed that polynomial is noncomputable first though)

[Wrenna Robson]

yes in this perfect world I'm imagining we've fixed that perverse state of affairs

[Wrenna Robson]

I mean it's like that for very good reasons but it's also a funny joke

[Wrenna Robson]

I imagine in practice we might have "computable polynomials" and "theorem polynomials" and some translation between them, a la how we have array I think because it's fast even though we don't really do, say, linear algebra proofs with it.

[Wrenna Robson]

Incidentally my framework also fits well into the lemmas at the top (reworked versions of existing ones) which link to the vandermonde. If you look at how the matrix.vandermonde lemmas work, it's all about doing this kind of thing with indexes.

[Wrenna Robson]

In the case of the vandermonde you have to do stuff with fin n but you can fix that (noncomputably, but that's fine enough for government work).

[Wrenna Robson]

I'm really very, very happy with how easy those proofs were (with only a little bit of massaging). The vandermonde is the key link between Lagrange interpolation and linear algebra (and thus the particular link between polynomials and linear algebra which is key for This Sort Of Thing).

[Wrenna Robson]

It's basically the best gadget.

[Junyan Xu]

I imagine in practice we might have "computable polynomials" and "theorem polynomials" and some translation between them, a la how we have array I think because it's fast even though we don't really do, say, linear algebra proofs with it.

Some discussions in this twitter thread last November:
https://twitter.com/XenaProject/status/1462788134584954881
https://twitter.com/XenaProject/status/1462475753556221953
https://twitter.com/XenaProject/status/1462800104541376524

@EscardoMartin @jjcarett2 Well this is an interesting idea. I remember when Lean switched from constructive to nonconstructive polynomials (and I remember why too -- we were having problems proving theorems about constructive polys). But wouldn't having both `poly` and `constructive_poly` be a minefield?

- Kevin Buzzard (@XenaProject)

@jjcarett2 @EscardoMartin In Lean we rejected constructive polynomials because they were simply too tedious to work with; constructivism caused pain, and the only gain was constructive polynomial addition. Instead we have a *tactic* for doing polynomial addition, and this will do for us.

- Kevin Buzzard (@XenaProject)

@jonmsterling @EscardoMartin @jjcarett2 You say "coefficients are 0 except for degrees in this explicit finset" where a finset is a constructive finite subset of the naturals, so now you can't add them because you can't tell whether the coefficient of x^3 is zero because you can't decide a+b=0 in the reals.

- Kevin Buzzard (@XenaProject)

[Wrenna Robson]

Interesting! I leave that stuff to cleverer minds than I.

[Wrenna Robson]

I am simply small brain cavewoman and want to know that x + x + x^2 + x = x^2 + 3*x.

[Wrenna Robson]

(Which I assume is ultimately how you do it in the simple case, use some sparkly ubertactic to put polynomials in some normal form.)

[Junyan Xu]

The noncomputability of docs#finsupp.single comes from the need to distinguish between zero and nonzero, hence the need of decidable_eq, supplied by the classical instance:

finsupp.single a b = {support := ite (b = 0) ∅ {a}, to_fun := λ (a' : α), ite (a = a') b 0, mem_support_to_fun := _}

A more computable implementation of finsupp would be the following:

import
  data.finset.basic
  data.setoid.basic

variables (α M : Type*)

structure finsupp_aux [has_zero M] :=
(support : multiset α)
(to_fun : α → M)
(mem_support_to_fun : ∀ a, to_fun a ≠ 0 → a ∈ support) -- notice this is no longer iff

def finsupp [has_zero M] := quotient (setoid.comap finsupp_aux.to_fun ⊥ : setoid (finsupp_aux α M))
-- `f g : finsupp_aux α M` are equivalent iff `f.to_fun = g.to_fun`.

def finsupp.single [decidable_eq α] [has_zero M] (a : α) (m : M) : finsupp α M :=
begin
  apply quotient.mk, exact
{ support := {a},
  to_fun := λ a', if a' = a then m else 0,
  mem_support_to_fun := λ a' h, by { left, by_contra hne, exact h (if_neg hne) } },
end

However, if you have a list of terms in α × M and want to computably construct a term in finsupp α M, you still need decidable_eq α to define to_fun field and to define polynomial multiplication, but that's satisfied when α is ℕ or ℤ (for polynomials) and many other cases. A maximally computable definition would be the following:

def finsupp' [add_comm_monoid M] := quotient (setoid.comap
  (λ s a, (multiset.map prod.snd $ by classical; exact s.filter (λ p, p.fst = a)).sum) ⊥ : setoid $ multiset (α × M))

def finsupp'.single [add_comm_monoid M] (a : α) (m : M) : finsupp' α M :=
by { apply quotient.mk, exact {(a,m)} }

This definition would allow you to define polynomial addition and multiplication computably without decidable_eq α. But it requires an add_comm_monoid, and evaluation won't be able to automatically combine like terms. So it feels the first definition would be most useful.
A third definition only requires has_zero, but doesn't support computable addition:

structure finsupp''_aux [has_zero M] :=
(monomials : multiset (α × M))
(nodup : (monomials.map prod.fst).nodup)

def finsupp'' [has_zero M] := quotient (setoid.comap
  (λ f [decidable_eq M], by exactI f.monomials.filter (λ p, p.snd ≠ 0)) ⊥ : setoid (finsupp''_aux α M))

def finsupp''.single [has_zero M] (a : α) (m : M) : finsupp'' α M :=
begin
  apply quotient.mk, exact
{ monomials := {(a,m)},
  nodup := multiset.nodup_singleton _ },
end

Have people explored these ideas before?

[Junyan Xu]

Wow, docs#dfinsupp.pre uses exactly my first strategy! I found it in this thread.

Maybe I am not thinking about the right question, as per what Reid Barton said:

"making finsupp computable" is not the right kind of goal, the correct goal should be "add data structure X which supports operations Y in time complexity Z, for use in algorithm W"

[Junyan Xu]

Since the lagrange stuff is being refactored, what do people think about allowing the values to live in some algebra R over F instead of F itself? If R is a domain you also get uniqueness.

[Kevin Buzzard]

I wouldn't take anything I say about constructivism on Twitter seriously, not least because I don't know anything about it

[Wrenna Robson]

I'm fine for it to not be over a field - just let me know the more general setting.

[Wrenna Robson]

@Eric Wieser I understand why you've made the suggestion re: not using∏ j, ite (i = j) 1 that you have - but I have certainly found that form a lot easier to work with in proofs.

[Wrenna Robson]

Like switching to the erase formulation makes all my proofs break and it isn't necessarily clear how to fix them without making them all longer.

[Eric Wieser]

I'm quite surprised by that; we have plenty of lemmas about the product of finset.erase

[Eric Wieser]

It's also worth noting that the existing proofs already used finset.erase

[Eric Wieser]

With @Yaël Dillies' suggested approach docs#lagrange.basis would just become

def basis (s : finset ι) (i : ι) (v : ι ↪ F) : F[X] :=
∏ j in s.erase i, C (v i - v j)⁻¹ * (X - C (v j))

or the equivalent

def basis (s : finset ι) (i : ι) (v : ι ↪ F) : F[X] :=
∏ y in (s.erase i).map v, C (v i - y)⁻¹ * (X - C y)

[Wrenna Robson]

Oh, I'm sure if I find the right lemmas it'll be fine; it's worth saying that the existing proofs got quite long and involved (my current proofs I think generally are shorter) but I'm sure there are short ways.

[Wrenna Robson]

I just don't much like that definition, though.

[Wrenna Robson]

(Also the basis_divisor v i j abstraction is very nice to work with so it would be good to keep that.)

[Wrenna Robson]

I don't see why you would define some indexed embedding but then only work with a finset of it, as opposed to simply working with a finite type. Indexing by types is what we do in the case of, say, !docs#matrix, it works well there.

[Wrenna Robson]

(I could see, btw (v : s ↪ F) working... but at that stage you're just using s as a fintype!)

[Wrenna Robson]

@Eric Wiesergood news - managed to fix my proofs. thank goodness the effect wasn't too large.

[Wrenna Robson]

ultimately I can see the value of the above approach when we're dealing with a flexible indexing set. it's just not clear to me that is what you want here.

[Wrenna Robson]

Also - what do you do in the case where you want to add a node to v : ι ↪ F that wasn't originally specified - that is, extend ι? That to me feels at least as likely as wanting to shrink it.

[Wrenna Robson]

It occurs that you could define def basis_divisor (x y : F) : F[X] := C (x - y)⁻¹ * (X - C (y)), closer to how it originally works (though I do think abstracting that out is useful, it has nice properties in and of itself).

[Wrenna Robson]

But then you get close to re-introducing this decidable_eq condition on the field, which is unnatural.

[Wrenna Robson]

https://leanprover-community.github.io/mathlib_docs/data/setoid/partition.html#indexed_partition

[Wrenna Robson]

This seems to be an example where, again, we index by type.

[Eric Wieser]

I'm not sure if it's what you're explicitly describing above, but I think I see the problem; (s : finset ι) (i : ι) (v : ι ↪ F) puts too strong a condition on v, as it only need to be injective on s.

[Sebastien Gouezel]

Can't you drop all the injectivity assumptions in the definition of basis, and prove results assuming inj_on v s?

[Wrenna Robson]

Yes; what isn't clear to me is what advantage that gets you.

[Wrenna Robson]

Like - at that stage, why not just define v : s ↪ F?

[Yaël Dillies]

because then how do you add an element? This sounds like pain.

[Wrenna Robson]

Right - what I'm saying is I'm not sure that you need to.

[Wrenna Robson]

Certainly I'm proving everything I want to be proving without doing this.

[Wrenna Robson]

It's like saying, for, say, matrix, "how do you add a column to the column indexing type"? You don't, really.

[Wrenna Robson]

Also: if I define v : ι -> F, then what happens when I want to add a node to s that isn't indexed by any i : ι? You end up with the same problem anyway.

[Wrenna Robson]

Just pushed a new set of commits to #15036.

[Wrenna Robson]

Importantly we now have eq_interpolate_iff, which we implicitly previously had but I think is good to have explicitly: this is the characteristic property of the interpolation to a set of node-value pairs.

[Wrenna Robson]

(This also perhaps makes a little clearer why I am happy with the current formulation: an interpolation is arguably defined /according to a particular choice of nodes/, and adding or removing a node simply gives a different interpolation, although there clearly is a relationship here.)

[Wrenna Robson]

We also need a better location for the non_lagrange lemmas than this file: happy to take suggestions.

[Wrenna Robson]

The only requirement is that wherever they go, this file will want to import it.

[Wrenna Robson]

The finset approach does have things to commend it, I think, if we wanted to have other forms of the interpolant especially.
So what is needed is:

• Have some type of indexes ι, which will probably have decidable equality.
• Have some s : finset ι, which represents "currently used indexes".
• For each i in s, we have some v_i in F, and these v_i are unique. They're the nodes.
• For each i in s, we have some r_i in F. They don't have to be unique.

That's almost the setup above, but, crucially, there's no need to define v_i and r_i across the entire ι.

[Wrenna Robson]

But as I've said, I'm not necessarily sure that's better if you're not adding/removing nodes.

[Eric Wieser]

Wrenna Robson said:

That's almost the setup above, but, crucially, there's no need to define v_i and r_i across the entire ι.

This doesn't really matter though, as you know these types are inhabited so you can always output zero.

[Wrenna Robson]

yes, but I am... not convinced by that perspective.

[Wrenna Robson]

Is there a way to (noncomputably) turn a s : finset F into an injective function v : fin (card s) -> F

[Wrenna Robson]

Having tried to implement the above, that's really the sticking point, because I want to be able to use det_vandermonde_ne_zero_iff.

[Wrenna Robson]

fintype.equiv_fin does this for fintypes.

[Eric Wieser]

I guess you could claim that we should have vandermonde : matrix ι (fin n) R, although that doesn't help when you get to taking the determinant

[Eric Wieser]

Wrenna Robson said:

fintype.equiv_fin does this for fintypes.

That should be all you need, ↥s is a fintype

[Wrenna Robson]

I don't really claim that - I just want to use the nice vandermonde polynomial lemmas.

[Wrenna Robson]

Eric Wieser said:

Wrenna Robson said:

fintype.equiv_fin does this for fintypes.

That should be all you need, ↥s is a fintype

Right, that's what I thought. I'll try it again. Where's the instance for that?

[Wrenna Robson]

I need ↥s ↪ F; what gives that?

[Eric Wieser]

docs#function.embedding.subtype

[Wrenna Robson]

ta

[Wrenna Robson]

well, that does it. it's not... pretty...

[Wrenna Robson]

theorem eq_zero_of_eval_eq_zero {F : Type*} [field F] (s : finset F) {f : F[X]}
  (degree_f_lt : f.degree < card s) (eval_f : ∀ x ∈ s, f.eval x = 0) : f = 0 :=
begin
  rw [← mem_degree_lt, ← fintype.card_coe] at degree_f_lt,
  refine vandermonde_invert (function.embedding.trans (fintype.equiv_fin s).symm.to_embedding (function.embedding.subtype _)) degree_f_lt _,
  simp_rw [function.embedding.trans_apply, function.embedding.coe_subtype],
  exact λ _, eval_f _ (coe_mem _),
end

[Wrenna Robson]

Compared with:

theorem eq_zero_of_eval_eq_zero {F : Type*} [field F] {ι : Type*} [fintype ι] (v : ι ↪ F) {f : F[X]}
  (degree_f_lt : f.degree < fintype.card ι) (eval_f : ∀ i, f.eval (v i) = 0) : f = 0 :=
begin
  rw ← mem_degree_lt at degree_f_lt,
  exact vandermonde_invert  (function.embedding.trans(fintype.equiv_fin ι).symm.to_embedding v)
                            degree_f_lt (λ _, eval_f _)
end

[Wrenna Robson]

For reference vandermonde_invert is essentially "that, but indexed with fin n".

[Wrenna Robson]

Eric Wieser said:

Wrenna Robson said:

That's almost the setup above, but, crucially, there's no need to define v_i and r_i across the entire ι.

This doesn't really matter though, as you know these types are inhabited so you can always output zero.

It's a shame there's no "finsupp but for junk values instead of zero".

[Wrenna Robson]

Because that's kinda what this approach would need.

[Wrenna Robson]

@Yaël Dillies @Eric Wieser Good news! After substantial effort, I've refactored my refactor so that it's indexed-by-finsets, per the suggestions above.

[Wrenna Robson]

We're now in the sort of halfway house between the two worlds.

[Wrenna Robson]

I've also left out all the interpolate_at stuff, which is about interpolating a particular function F -> F: it was ending up with a lot of definition replication where the proofs were just yards of def eq, for no clear benefit.

[Wrenna Robson]

interpolate_eq_interpolate_erase_add now has a nice proof (I changed the statement slightly but it says the same thing). I think this is probably generalisable, incidentally, to any subset of the finset.

Also, the proof of basis_divisor_add_symm is a little indulgent (you can do it quicker using "brute force rewrites, though it's horrible), but I think it nicely shows the utility of using the earlier lemmas.

[Wrenna Robson]

It might be nice to have the barycentric form of the interpolant, but that does run into issues with the fact you have to work over the fraction field.

[Wrenna Robson]

682c36ab-c98e-4b4b-b99b-e5387a300bb6.jpg

[Wrenna Robson]

For reference

[Wrenna Robson]

By the way, do we really not have zero_lt_two for with_bot?

[Violeta Hernández]

Oh if only someone had proposed a refactor to provide those lemmas in much more general circumstances

[Wrenna Robson]

Hahaha I did think of you

[Wrenna Robson]

I hate working with with_bot so much. Everything is so much harder than it needs to be.

[Wrenna Robson]

And then occasionally mathlib can't find the covariant class instances and complains.

[Wrenna Robson]

I was dreaming about finsets last night -_-

[Wrenna Robson]

My worry is that it might be annoying to use some of this stuff in practice, and also that maybe I should make a fintype definition as well, using the now finset-indexed version. But then it's like - do you replicate all the theorems? Is it better to just have the one most general version of interpolate and let people just use it in different ways in context, or is there value to providing specific versions?

[Wrenna Robson]

Interested in thoughts.

[Wrenna Robson]

Also someone mentioned it might be possible to generalise it somewhat more

[Wrenna Robson]

This is what I mean by other spellings (fragment):

section other_spellings
open finset
variables {ι : Type*} [decidable_eq ι]

def interpolate_on (s : finset ι) (v : ι → F) (f : F → F) := interpolate s v (λ i, f (v i))
def interpolate_fintype [fintype ι] (v : ι ↪ F) (r : ι → F) := interpolate univ v r
def interpolate_fintype_on [fintype ι] (v : ι ↪ F) (f : F → F) := interpolate univ v (λ i, f (v i))

lemma inj_on_finset_univ [fintype ι] {v : ι ↪ F} : set.inj_on v (univ : finset ι) :=
set.inj_on_of_injective v.inj' _

end other_spellings

[Wrenna Robson]

So, like, in theory you could replicate some of the theorems for some of these? But I'm not sure there's much use.

[Wrenna Robson]

The only thing would be avoiding having to type out that proof for inj_on_finset_univ every time.

[Wrenna Robson]

We now have the following extension of the existing interpolate_eq_interpolate_erase_add, which is now a special case:

theorem interpolate_eq_sum_interpolate_insert_sdiff (hvt : set.inj_on v t) (hs : s.nonempty) (hst : s ⊆ t) : interpolate t v r = ∑ i in s, (interpolate (insert i (t \ s)) v r) * basis s v i := sorry

[Wrenna Robson]

Ultimately the finset approach was the right one because this was, mostly, a dream.

[Wrenna Robson]

This is going to need some extensive review (even though I think it is near a "done" point). In particular, I think a lot of my proofs today can probably be golfed, but I didn't have it in me to tighten them all.

[Wrenna Robson]

But I do feel confident in the work - things, mostly, feel "neat".

[Wrenna Robson]

def interpolate_on (s : finset ι) (v : ι → F) (f : F → F) := interpolate s v (f ∘ v)
def interpolate_fintype [fintype ι] (v : ι ↪ F) (r : ι → F) := interpolate univ v r
def interpolate_fintype_on [fintype ι] (v : ι ↪ F) (f : F → F) := interpolate univ v (f ∘ v)
def interpolate_fintype_using [decidable_eq F] (s : finset F) (f : F → F) := interpolate s id f
def interpolate_finfield [fintype F] [decidable_eq F] (f : F → F) := interpolate univ id f

These are all the sensible variants I can think of. It could be useful to have other versions of my theorems for them - the alternative I think would be making more of the parameters in the theorems explicit.

[Wrenna Robson]

What I hadn't realised was true until I wrote that last one down, but which is obvious now that I think about it, is that all maps F -> F on a finite field F can be described as polynomials.

[Wrenna Robson]

Just a bump to ask what people think is still required here, and if I should put in any of the different spellings/special cases I made above?

[Wrenna Robson]

#15036 is the PR in question, as a reminder.

[Yaël Dillies]

You could post in #PR reviews

[Wrenna Robson]

Ah - thanks, I wasn't subbed to that/