Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat(analysis/fourier): span of monomials is dense in L^p #8328

Closed
wants to merge 55 commits into from
Closed

[Merged by Bors] - feat(analysis/fourier): span of monomials is dense in L^p #8328

wants to merge 55 commits into from

Conversation

hrmacbeth
Copy link
Member

@hrmacbeth
progress
807a526
@hrmacbeth
first pass
cebdb2b
@hrmacbeth
Merge remote-tracking branch 'origin/master' into refactor-l1-approx
fa86461
@hrmacbeth
bochner working
459a813
@hrmacbeth
integrable.induction
665d998
@hrmacbeth
kill some instances, does it break?
5e0ea9f
@hrmacbeth
golf
804a966
@hrmacbeth
lint
44d3c9a
@hrmacbeth
delete various restatements of add_subgroup lemmas
e550708
@hrmacbeth
revert a couple of changes
fac9d5d
@hrmacbeth
golf
b8231ca
@hrmacbeth
delete one more lemma and change notation
7cc82a2
@hrmacbeth
edit documentation
0166de0
@hrmacbeth
cleaner hypotheses
a77b7a7
@hrmacbeth
tweaks
1fd7626
@hrmacbeth
delete local notation to_L1
5949417
@hrmacbeth
open some namespaces
08f0cf7
@hrmacbeth
rename disjoint lemmas
c675f76
@hrmacbeth
tweaks
ec76d47
@hrmacbeth
mistaken name change
69b9fa3
@hrmacbeth
Merge remote-tracking branch 'origin/refactor-l1-approx' into continu…
36732ed 
…ous_dense_lp
@hrmacbeth
new Lp induction lemmas
750e7e3
@hrmacbeth
most of the proof
780e240
@hrmacbeth
typo
955c21c
@hrmacbeth
Merge remote-tracking branch 'origin/staging' into continuous_dense_lp
9fb6b90
@hrmacbeth
some algebra
9152552
@hrmacbeth
re-home lemmas
7aff919
@hrmacbeth
initial commit
41301d6
@hrmacbeth
alter name scheme
506bef8
@hrmacbeth
whitespace
940708d
@github-actions github-actions bot added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Jul 15, 2021
@github-actions github-actions bot added merge-conflict Please `git merge origin/master` then a bot will remove this label. and removed blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. labels Jul 16, 2021
@github-actions
Copy link

🎉 Great news! Looks like all the dependencies have been resolved:

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Jul 16, 2021
@semorrison semorrison added the awaiting-review The author would like community review of the PR label Jul 17, 2021
sgouezel
sgouezel reviewed Jul 19, 2021
View reviewed changes
src/analysis/fourier.lean Outdated Show resolved Hide resolved
@sgouezel
Copy link
Collaborator

bors r+
Thanks!

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Jul 19, 2021
bors bot pushed a commit that referenced this pull request Jul 19, 2021
@hrmacbeth
feat(analysis/fourier): span of monomials is dense in L^p (#8328)
02ecb62
@bors
Copy link

bors bot commented Jul 19, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(analysis/fourier): span of monomials is dense in L^p [Merged by Bors] - feat(analysis/fourier): span of monomials is dense in L^p Jul 19, 2021
@bors bors bot closed this Jul 19, 2021
@bors bors bot deleted the fourier-dense-l2 branch July 19, 2021 14:09
b-mehta pushed a commit that referenced this pull request Jul 20, 2021
@hrmacbeth @b-mehta
feat(analysis/fourier): span of monomials is dense in L^p (#8328)
02a9cd5
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@sgouezel sgouezel sgouezel left review comments

Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@hrmacbeth @sgouezel @semorrison