[Merged by Bors] - feat(linear_algebra/lagrange): Refactor lagrange interpolation and add extended proofs. #15036

linesthatinterlace · 2022-06-28T18:39:19Z

The current formulation of Lagrange interpolants phrases things in terms of a finset of nodes, and functions interpolated at those nodes. This changes things in order to allow for indexed nodes and weights. It also extends various functionalities of the lagrange interpolation.

It is more standard - and in many ways more natural - to think in terms of nodes and weights (that is, evaluations) at those nodes. This corresponds to a reformulation in terms of injective functions from fintypes. This commit implements the necessary changes to do this, and attempts to introduce API to fill the gaps left behind.

I am looking for feedback on this in terms of overall approach as well as details - I should point out that this isn't for the sake of it: in the real context of the theory of binary Goppa codes, I was encountering issues with the previous formulation as it is very natural to want to index your weights by the same thing that one indexes your nodes: and, again, it's natural for these to be tuples.

This new approach seems to give tighter and neater proofs, which seems a good sign.

vihdzp

There's tons of untapped simp potential.

src/linear_algebra/lagrange.lean

src/linear_algebra/vandermonde.lean

I stripped out all the simps from the original file when refactoring - this adds a chunk of them back in (though they have not been linted). Co-authored-by: Violeta Hernández <vi.hdz.p@gmail.com>

src/linear_algebra/lagrange.lean

linesthatinterlace · 2022-07-01T12:49:37Z

I have pushed a number of extensive reworks to this, including adding new, genuinely mathematical interesting (I think!) lemmas. https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Lagrange.20interpolants

linesthatinterlace · 2022-07-01T14:57:49Z

I have an ongoing question about a) whether the nodal stuff I define is worth keeping, b) whether it is worth defining certain special cases of the definition, and whether or not they should be accompanied by theorems.

BoltonBailey

This seems good. Scanning the proof no golfs jump out at me. I'll make some other reviews with style comments.

src/linear_algebra/lagrange.lean

Vierkantor · 2022-07-29T09:42:03Z

@Vierkantor Do you have any thoughts on whether it is worth including any of the special-case spellings a la here: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Lagrange.20interpolants/near/288179709

I'd like to hold off on special spellings for now, until I see them in action a bit more. Unfortunately adding new defs generally causes a lot more work...

Vierkantor

I went through again especially focussed on the names this time, I think one more round of reviews and we're there.

src/data/finset/basic.lean

src/ring_theory/polynomial/basic.lean

src/linear_algebra/lagrange.lean

vihdzp

A few general remarks.

src/data/finset/basic.lean

src/linear_algebra/vandermonde.lean

src/ring_theory/polynomial/basic.lean

linesthatinterlace · 2022-08-02T13:08:16Z

@Vierkantor what do you reckon now?

Vierkantor

Everything looks good with just some minor remarks, thanks!

bors d+

src/linear_algebra/lagrange.lean

bors · 2022-08-03T10:26:37Z

✌️ linesthatinterlace can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

linesthatinterlace · 2022-08-03T10:36:11Z

bors r+

…d extended proofs. (#15036) The current formulation of Lagrange interpolants phrases things in terms of a finset of nodes, and functions interpolated at those nodes. This changes things in order to allow for indexed nodes and weights. It also extends various functionalities of the lagrange interpolation. Co-authored-by: Wrenna Robson <34025592+linesthatinterlace@users.noreply.github.com>

bors · 2022-08-03T11:31:34Z

Build failed (retrying...):

Build mathlib

…d extended proofs. (#15036) The current formulation of Lagrange interpolants phrases things in terms of a finset of nodes, and functions interpolated at those nodes. This changes things in order to allow for indexed nodes and weights. It also extends various functionalities of the lagrange interpolation. Co-authored-by: Wrenna Robson <34025592+linesthatinterlace@users.noreply.github.com>

bors · 2022-08-03T11:35:23Z

This PR was included in a batch that was canceled, it will be automatically retried

…d extended proofs. (#15036) The current formulation of Lagrange interpolants phrases things in terms of a finset of nodes, and functions interpolated at those nodes. This changes things in order to allow for indexed nodes and weights. It also extends various functionalities of the lagrange interpolation. Co-authored-by: Wrenna Robson <34025592+linesthatinterlace@users.noreply.github.com>

bors · 2022-08-03T16:27:29Z

Pull request successfully merged into master.

Build succeeded:

linesthatinterlace added 2 commits June 28, 2022 19:28

Add useful lemmas linking the Vandermonde to polynomials

3be6bc1

Refactor the lagrange interpolation in terms of fintypes

233e826

linesthatinterlace added WIP Work in progress awaiting-review The author would like community review of the PR labels Jun 28, 2022

vihdzp reviewed Jun 28, 2022

View reviewed changes

linesthatinterlace and others added 2 commits June 28, 2022 20:30

Add missing simp lemmas

bb31d8d

I stripped out all the simps from the original file when refactoring - this adds a chunk of them back in (though they have not been linted). Co-authored-by: Violeta Hernández <vi.hdz.p@gmail.com>

Updated documentation, naming and whitespace

3ec2e97

eric-wieser reviewed Jun 28, 2022

View reviewed changes

src/linear_algebra/lagrange.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Jun 28, 2022

View reviewed changes

src/linear_algebra/lagrange.lean Outdated Show resolved Hide resolved

linesthatinterlace added 12 commits June 29, 2022 16:21

Add bernoulli lemmas

a4a231f

Fix line lengths

0107b45

Change definition of basis to use erase

2ff77c2

Add characteristic property of the interpolation

efa8112

Remove unused argument

25a965c

Reposition module documentation

07c823a

Add nodal/barycentric construction of Lagrange interpolant

27c749d

Remove erase lemmas until we can figure out what to do with them

d5009f7

Fix line lengths

2293704

Fix line lengths

722c0a5

Refactor of previous commits to allow for finset indexing

2b98564

Extend erase and sum of basis lemmas

3d2e907

linesthatinterlace added 2 commits July 4, 2022 15:05

Add barycentric form of interpolant

045fd4d

Remove Bernoulli lemmas as no longer used in this PR

1556255

linesthatinterlace changed the title ~~refactor(linear_algebra/lagrange): Refactor the lagrange interpolant in terms of fintypes.~~ refactor(linear_algebra/lagrange): Refactor lagrange interpolation. Jul 4, 2022

linesthatinterlace changed the title ~~refactor(linear_algebra/lagrange): Refactor lagrange interpolation.~~ feat(linear_algebra/lagrange): Refactor lagrange interpolation and add extended proofs. Jul 4, 2022

BoltonBailey reviewed Jul 7, 2022

View reviewed changes

src/linear_algebra/lagrange.lean Outdated Show resolved Hide resolved

BoltonBailey reviewed Jul 7, 2022

View reviewed changes

src/linear_algebra/lagrange.lean Outdated Show resolved Hide resolved

linesthatinterlace added awaiting-review The author would like community review of the PR awaiting-CI The author would like to see what CI has to say before doing more work. and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jul 22, 2022

github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Jul 22, 2022

Vierkantor reviewed Jul 29, 2022

View reviewed changes

Vierkantor added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Jul 29, 2022

vihdzp reviewed Jul 29, 2022

View reviewed changes

src/data/finset/basic.lean Outdated Show resolved Hide resolved

src/linear_algebra/vandermonde.lean Outdated Show resolved Hide resolved

src/ring_theory/polynomial/basic.lean Outdated Show resolved Hide resolved

linesthatinterlace added 3 commits August 1, 2022 15:46

Changes after review

86d3dc9

Fix line length

26ac61a

Fix lint and style

f9f91d6

linesthatinterlace added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Aug 2, 2022

Vierkantor approved these changes Aug 3, 2022

View reviewed changes

src/linear_algebra/lagrange.lean Outdated Show resolved Hide resolved

src/linear_algebra/lagrange.lean Outdated Show resolved Hide resolved

leanprover-community-bot-assistant added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Aug 3, 2022

Apply suggestions from code review

983b045

Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

bors bot changed the title ~~feat(linear_algebra/lagrange): Refactor lagrange interpolation and add extended proofs.~~ [Merged by Bors] - feat(linear_algebra/lagrange): Refactor lagrange interpolation and add extended proofs. Aug 3, 2022

bors bot closed this Aug 3, 2022

bors bot deleted the lagrange-fintype branch August 3, 2022 16:27

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(linear_algebra/lagrange): Refactor lagrange interpolation and add extended proofs. #15036

[Merged by Bors] - feat(linear_algebra/lagrange): Refactor lagrange interpolation and add extended proofs. #15036

linesthatinterlace commented Jun 28, 2022 •

edited

vihdzp left a comment

linesthatinterlace commented Jul 1, 2022

linesthatinterlace commented Jul 1, 2022

BoltonBailey left a comment

Vierkantor commented Jul 29, 2022

Vierkantor left a comment

vihdzp left a comment

linesthatinterlace commented Aug 2, 2022

Vierkantor left a comment

bors bot commented Aug 3, 2022

linesthatinterlace commented Aug 3, 2022

bors bot commented Aug 3, 2022

bors bot commented Aug 3, 2022

bors bot commented Aug 3, 2022

[Merged by Bors] - feat(linear_algebra/lagrange): Refactor lagrange interpolation and add extended proofs. #15036

[Merged by Bors] - feat(linear_algebra/lagrange): Refactor lagrange interpolation and add extended proofs. #15036

Conversation

linesthatinterlace commented Jun 28, 2022 • edited

vihdzp left a comment

Choose a reason for hiding this comment

linesthatinterlace commented Jul 1, 2022

linesthatinterlace commented Jul 1, 2022

BoltonBailey left a comment

Choose a reason for hiding this comment

Vierkantor commented Jul 29, 2022

Vierkantor left a comment

Choose a reason for hiding this comment

vihdzp left a comment

Choose a reason for hiding this comment

linesthatinterlace commented Aug 2, 2022

Vierkantor left a comment

Choose a reason for hiding this comment

bors bot commented Aug 3, 2022

linesthatinterlace commented Aug 3, 2022

bors bot commented Aug 3, 2022

bors bot commented Aug 3, 2022

bors bot commented Aug 3, 2022

linesthatinterlace commented Jun 28, 2022 •

edited