feat(Algebra/BigOperators/Fin): Add `finSigmaFinEquiv` by quangvdao · Pull Request #19013 · leanprover-community/mathlib4

quangvdao · 2024-11-14T02:19:09Z

This PR adds finSigmaFinEquiv which is the equivalence (i : Fin m) × Fin (n i) ≃ Fin (∑ i, n i). This is the dependent version of finProdFinEquiv.

CI should be passing, but there are two things I'd like feedback on:

When defining the mappings, I have to consider m = 0 separately. Is there a more uniform definition?
I'm proving this as a step toward defining Fin.join, which is the analogue of List.join. I can now technically define Fin.join as:

variable {a : Fin n → ℕ} {α : (i : Fin n) → (j : Fin (a i)) → Sort*}

def join (v : (i : Fin n) → (j : Fin (a i)) → α i j) (k : Fin (∑ i, a i)) :
    α (finSigmaFinEquiv.invFun k).1 (finSigmaFinEquiv.invFun k).2 :=
  v (finSigmaFinEquiv.invFun k).1 (finSigmaFinEquiv.invFun k).2

but this looks horrible. This highly motivates refactoring invFun as two new definitions:

def func1 {n : ℕ} (a : Fin n → ℕ) (k : Fin (∑ i, a i)) : Fin n := sorry

def func2 {n : ℕ} (a : Fin n → ℕ) (k : Fin (∑ i, a i)) : Fin (a (func1 a k)) := sorry

I'm not sure what to call these functions. The analogues in the non-dependent case are divNat and modNat.

github-actions · 2024-11-14T02:19:59Z

PR summary 9a02067e37

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ divSum
+ divSum?
+ divSum?_is_some_iff_lt_sum
+ finSigmaFinEquiv
+ finSigmaFinEquiv_apply
+ finSigmaFinEquiv_pair
+ modSum
+ sum_le_of_divSum?_eq_some

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

Changes to technical debt

Current number	Change	Type
5120	-2	porting notes

Current commit 9a02067e37
Reference commit 8d28d21b27

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

YaelDillies

I agree with you that m = 0 has to be treated separately

Mathlib/Algebra/BigOperators/Fin.lean

quangvdao · 2024-11-14T16:38:48Z

@YaelDillies addressed your comments.

I still think there is a uniform definition (this is what divNat and modNat does), but for now it would be great if the current version makes it into Mathlib.

eric-wieser · 2024-11-14T18:14:44Z

I agree with you that m = 0 has to be treated separately

I disagree, see the commit I pushed. There is no need to deal with a case separately that is impossible.

Mathlib/Algebra/BigOperators/Fin.lean

quangvdao · 2024-11-15T19:53:18Z

I have refactored finSigmaFinEquiv.invFun into two separate functions:

def Fin.divSum {m : ℕ} {n : Fin m → ℕ} (k : Fin (∑ j, n j)) : Fin m := sorry

def Fin.modSum {m : ℕ} {n : Fin m → ℕ} (k : Fin (∑ j, n j)) : Fin (n (divSum k)) := sorry

The naming takes inspiration from Fin.divNat and Fin.modNat used in finProdFinEquiv.

eric-wieser · 2024-11-15T22:28:40Z

Mathlib/Algebra/BigOperators/Fin.lean

+This is defined en-route to `Fin.divSum`, which is the dependent version of `Fin.divNat`.
+-/
+def divSum? {m : ℕ} (n : Fin m → ℕ) (k : ℕ) : Option (Fin m) :=
+  find (fun i => k < ∑ j, n (castLE i.isLt j))


This looks wrong to me; isLt is a proof of <, but castLE is about ≤. Can you make the type j explicit here to make it clearer what is going on?

Since i.isLt : i.val < n is definitionally equal to i.val.succ <= n, the sum is over j : Fin i.val.succ.

eric-wieser · 2024-11-16T01:34:39Z

Mathlib/Algebra/BigOperators/Fin.lean

+This is defined en-route to `Fin.divSum`, which is the dependent version of `Fin.divNat`.
+-/
+def divSum? {m : ℕ} (n : Fin m → ℕ) (k : ℕ) : Option (Fin m) :=
+  find (fun i => k < ∑ j : Fin i.val.succ, n (castLE i.isLt j))


Possibly better as

Suggested change

find (fun i => k < ∑ j : Fin i.val.succ, n (castLE i.isLt j))

find (fun i => k < ∑ j ≤ i, n j)

which avoids the .succ and casting

Yeah, this is certainly possible and looks nicer. I'd probably want to propagate this change to finPiFinEquiv as well (which a quick search tells me isn't used anywhere else). It also means that I'll need to add more lemmas about sum over Finset.Iic.

If all of this sounds good to you, then I'll make the changes.

Let's check @YaelDillies agrees too

Yes, makes sense to me

initial commit

235fb4d

github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Nov 14, 2024

quangvdao added the help-wanted The author needs attention to resolve issues label Nov 14, 2024

quangvdao requested review from YaelDillies and eric-wieser November 14, 2024 02:20

YaelDillies reviewed Nov 14, 2024

View reviewed changes

Mathlib/Algebra/BigOperators/Fin.lean Outdated Show resolved Hide resolved

Mathlib/Algebra/BigOperators/Fin.lean Outdated Show resolved Hide resolved

Mathlib/Algebra/BigOperators/Fin.lean Outdated Show resolved Hide resolved

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 14, 2024

simplified proof

dcb641b

quangvdao removed help-wanted The author needs attention to resolve issues awaiting-author A reviewer has asked the author a question or requested changes. labels Nov 14, 2024

remove the special case for n=0

1d92b77

eric-wieser reviewed Nov 14, 2024

View reviewed changes

Mathlib/Algebra/BigOperators/Fin.lean Outdated Show resolved Hide resolved

quangvdao added 3 commits November 15, 2024 13:16

made index type of summation explicit

95540e7

removed porting note in finPiFinEquiv

22b4114

refactored into new functions divSum and modSum

927c8a5

golf

80f6045

eric-wieser reviewed Nov 15, 2024

View reviewed changes

added explicit sum indexing for divSum?

9a02067

eric-wieser reviewed Nov 16, 2024

View reviewed changes

quangvdao added the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 18, 2024

This was referenced Dec 2, 2024

feat(BigOperators/Fin): Sum/product over Fin intervals #19697

Open

[Merged by Bors] - feat(Logic/Equiv/Basic): sumSigmaDistrib, finSigmaFinEquiv #19618

Closed

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 19, 2025

	find (fun i => k < ∑ j : Fin i.val.succ, n (castLE i.isLt j))
	find (fun i => k < ∑ j ≤ i, n j)

Conversation

quangvdao commented Nov 14, 2024

Uh oh!

github-actions bot commented Nov 14, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 9a02067e37

Import changes for modified files

Declarations diff

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

quangvdao commented Nov 14, 2024

Uh oh!

eric-wieser commented Nov 14, 2024

Uh oh!

Uh oh!

quangvdao commented Nov 15, 2024

Uh oh!

eric-wieser Nov 15, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

quangvdao Nov 15, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

eric-wieser Nov 16, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

quangvdao Nov 16, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

eric-wieser Nov 16, 2024

Choose a reason for hiding this comment

Uh oh!

YaelDillies Nov 16, 2024

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

github-actions bot commented Nov 14, 2024 •

edited

Loading

eric-wieser Nov 15, 2024 •

edited

Loading

quangvdao Nov 15, 2024 •

edited

Loading

eric-wieser Nov 16, 2024 •

edited

Loading

quangvdao Nov 16, 2024 •

edited

Loading