[Merged by Bors] - feat(Analysis/Fourier): discrete Fourier transform on `ZMod N` by loefflerd · Pull Request #13353 · leanprover-community/mathlib4

loefflerd · 2024-05-29T19:50:01Z

We write down basic definitions for the discrete Fourier transform, and compute the Fourier transforms of primitive Dirichlet characters (a minor reformulation of a result from an earlier PR).

depends on: [Merged by Bors] - feat(AddChar): Various improvements #13579
depends on: [Merged by Bors] - feat (MeasureTheory/Function): trivial cases of integrability / summability #13872
depends on: [Merged by Bors] - chore(NumberTheory/MulChar): deprecate IsNontrivial, fix isPrimitive #13878
depends on: [Merged by Bors] - chore: Split large file MeasureTheory.MeasurableSpace.Basic #13937

* Add a bunch of missing `simp` and `norm_cast` lemmas. * Get rid of `IsNontrivial ψ` since it's just `ψ ≠ 1`. This simplifies proofs. * Remove explicit arguments to `toMonoidHomEquiv`/`toAddMonoidHomEquiv`. We basically never need to provide them explicitly since unification usually does the job.

Mathlib/Analysis/Fourier/ZMod.lean

loefflerd · 2024-06-14T11:27:44Z

Thanks for the reviews guys! I'm going to review #13579 and then merge it here since it's clearly relevant.

…DL_zmod_fourier

github-actions · 2024-06-14T13:10:10Z

PR summary 16f43ac386

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.MeasureTheory.MeasurableSpace.Instances	517	590	+73 (+14.12%)

Import changes for all files

Files	Import difference
8 files `Mathlib.Analysis.Fourier.AddCircle` `Mathlib.Geometry.Euclidean.Sphere.Ptolemy` `Mathlib.Geometry.Euclidean.Angle.Sphere` `Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle` `Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation` `Mathlib.NumberTheory.ZetaValues` `Mathlib.Geometry.Euclidean.Triangle` `Mathlib.Geometry.Euclidean.Angle.Oriented.Affine`	1
`Mathlib.Analysis.SpecialFunctions.Complex.Circle`	2
`Mathlib.MeasureTheory.MeasurableSpace.Instances`	73
`Mathlib.Topology.Instances.ZMod`	623
`Mathlib.Analysis.Fourier.ZMod`	1954

Declarations diff

+ ZMod.instMeasurableSingletonClass
+ ZMod.instMeasurableSpace
+ dft
+ dft_apply
+ dft_def
+ fourierTransform_eq_gaussSum_mulShift
+ fourierTransform_eq_inv_mul_gaussSum
+ instance : DiscreteTopology (ZMod N) := ⟨rfl⟩
+ instance : TopologicalSpace (ZMod N) := ⊥
+ stdAddChar
+ stdAddChar_apply
+ stdAddChar_coe
+ toAddCircle
+ toAddCircle_apply
+ toAddCircle_eq_zero
+ toAddCircle_inj
+ toAddCircle_injective
+ toAddCircle_intCast
+ toAddCircle_natCast
+ toCircle
+ toCircle_apply
+ toCircle_intCast
+ toCircle_natCast

You can run this locally as follows

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

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

…bility

loefflerd · 2024-06-30T10:14:46Z

Thanks for the (re-)review! Good point about natCast as well as intCast, that actually simplifies several other arguments since it meshes better with ZMod.val being Nat-valued. I added the corresponding lemma for Circle as well as AddCircle.

YaelDillies

Rest looks good, except for the fact that your new definition has no API (but apparently that's a conscious design decision on your part)

Mathlib/Analysis/Fourier/ZMod.lean

Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

loefflerd · 2024-07-06T10:55:16Z

Thanks Yael for the comments – I have incorporated them. I promise there will be more API in follow-up PRs; but this PR is a bit of a pain to work on at present (because it involves edits to widely-separated files in the import hierarchy), so I'd rather get it in as it stands.

YaelDillies · 2024-07-06T16:16:42Z

Okay then

maintainer merge

Ruben-VandeVelde · 2024-07-06T17:49:16Z

Odd.

maintainer merge

github-actions · 2024-07-06T17:49:29Z

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

riccardobrasca · 2024-07-07T12:04:42Z

Thanks!

bors merge

We write down basic definitions for the discrete Fourier transform, and compute the Fourier transforms of primitive Dirichlet characters (a minor reformulation of a result from an earlier PR). Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

mathlib-bors · 2024-07-07T12:27:13Z

Pull request successfully merged into master.

Build succeeded:

loefflerd added 2 commits May 29, 2024 21:49

feat(Analysis/Fourier): discrete Fourier transform on ZMod N

d2b717e

rehome lemmas

9863a04

loefflerd added awaiting-review t-analysis Analysis (normed *, calculus) t-measure-probability Measure theory / Probability theory labels May 30, 2024

clarify docstring

0d4872b

loefflerd requested a review from sgouezel May 30, 2024 10:13

jcommelin reviewed Jun 14, 2024

View reviewed changes

Mathlib/Analysis/Fourier/ZMod.lean Outdated Show resolved Hide resolved

YaelDillies reviewed Jun 14, 2024

View reviewed changes

Mathlib/Analysis/Fourier/ZMod.lean Outdated Show resolved Hide resolved

Mathlib/Analysis/Fourier/ZMod.lean Outdated Show resolved Hide resolved

Mathlib/Analysis/Fourier/ZMod.lean Outdated Show resolved Hide resolved

loefflerd added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Jun 14, 2024

YaelDillies and others added 3 commits June 14, 2024 12:08

style

342d5d1

Merge remote-tracking branch 'origin/add_char_qol_improvements' into …

33b3592

…DL_zmod_fourier

Merge remote-tracking branch 'origin/add_char_qol_improvements' into …

c1d8541

…DL_zmod_fourier

ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jun 14, 2024

loefflerd added 2 commits June 14, 2024 15:37

merge fallout

1af25df

review changes

e13c2fe

ghost added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Jun 14, 2024

Merge remote-tracking branch 'origin/master' into DL_zmod_fourier

8f7fac6

ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 14, 2024

loefflerd added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jun 14, 2024

feat (MeasureTheory/Function): trivial cases of integrability / summa…

3d922f1

…bility

loefflerd mentioned this pull request Jun 16, 2024

[Merged by Bors] - feat (MeasureTheory/Function): trivial cases of integrability / summability #13872

Closed

loefflerd added 2 commits June 16, 2024 11:51

Update L1Space.lean

4e76c3e

Yael's comment

a41177d

loefflerd added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jun 30, 2024

better way

244a681

ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 30, 2024

loefflerd added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Jun 30, 2024

YaelDillies reviewed Jul 6, 2024

View reviewed changes

Mathlib/Analysis/Fourier/ZMod.lean Outdated Show resolved Hide resolved

Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean Outdated Show resolved Hide resolved

Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean Show resolved Hide resolved

loefflerd and others added 3 commits July 6, 2024 11:34

Apply suggestions from code review

3909174

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Merge remote-tracking branch 'origin/master' into DL_zmod_fourier

679ceea

review changes

82531cf

loefflerd added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Jul 6, 2024

fix

16f43ac

loefflerd added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jul 6, 2024

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jul 6, 2024

github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jul 7, 2024

mathlib-bors bot changed the title ~~feat(Analysis/Fourier): discrete Fourier transform on ZMod N~~ [Merged by Bors] - feat(Analysis/Fourier): discrete Fourier transform on ZMod N Jul 7, 2024

mathlib-bors bot closed this Jul 7, 2024

mathlib-bors bot deleted the DL_zmod_fourier branch July 7, 2024 12:27

adomani mentioned this pull request Aug 1, 2024

feat: MiM PR report #15355

Open

Conversation

loefflerd commented May 29, 2024 • edited by YaelDillies Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

loefflerd commented Jun 14, 2024

Uh oh!

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

Uh oh!

PR summary 16f43ac386

Import changes for modified files

Declarations diff

Uh oh!

loefflerd commented Jun 30, 2024

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

loefflerd commented Jul 6, 2024

Uh oh!

YaelDillies commented Jul 6, 2024

Uh oh!

Ruben-VandeVelde commented Jul 6, 2024

Uh oh!

github-actions bot commented Jul 6, 2024

Uh oh!

riccardobrasca commented Jul 7, 2024

Uh oh!

mathlib-bors bot commented Jul 7, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

loefflerd commented May 29, 2024 •

edited by YaelDillies

Loading

github-actions bot commented Jun 14, 2024 •

edited

Loading