-
Notifications
You must be signed in to change notification settings - Fork 298
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.
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
[Merged by Bors] - feat(measure_theory/{lp_space,set_integral}): extend linear map lemmas from R to is_R_or_C #8210
Closed
Closed
Changes from 40 commits
Commits
Show all changes
41 commits
Select commit
Hold shift + click to select a range
be00f14
extend integral comp lemmas
RemyDegenne 5495f8e
add space
RemyDegenne c354445
undo accidental deletion of integral_apply
RemyDegenne 81dd754
fix
RemyDegenne fd532ea
Update docstring
RemyDegenne 603a922
use nondiscrete_normed_field
RemyDegenne 9aca324
Merge branch 'integral_comp' of github.com:leanprover-community/mathl…
RemyDegenne 30dddea
use semi_normed_space
RemyDegenne e8f80d2
use semi_normed_space
RemyDegenne 897f5b7
Revert "use semi_normed_space"
RemyDegenne 67e010f
add one semi_
RemyDegenne c6f7218
use more semi_normed_space
RemyDegenne 3abe826
use semi_normed_group
RemyDegenne 5cefb13
distinguish normed and semi_normed in lp_space
RemyDegenne af62add
prove completeness of Lp with only semi_
RemyDegenne 4756a3a
prove completeness of Lp with only semi_
RemyDegenne 5bce86a
add many semi_ and pseudo_ in bounded.lean
RemyDegenne da9fc10
add semi_ to lp_space lemmas about bounded
RemyDegenne 4d16fed
add some semi_ in compact.lean
RemyDegenne e6a45f5
more semi_ in lp_space
RemyDegenne b66ca78
fix
RemyDegenne 5300fa3
fix lint
RemyDegenne 0ef8151
Merge branch 'integral_comp' of https://github.com/leanprover-communi…
RemyDegenne 9acee35
undo indicator_function
RemyDegenne 1920f24
undo bochner_integration
RemyDegenne 619507e
undo borel_space
RemyDegenne 7dd7bf6
undo l1_space
RemyDegenne 073c244
undo set_integral
RemyDegenne 46f2a02
undo simple_func_dense
RemyDegenne 9e40657
undo bounded and compact
RemyDegenne 6722134
undo gromov_hausdorff
RemyDegenne 762c3cd
fake commit
RemyDegenne a01130f
fake commit
RemyDegenne f31481c
Merge remote-tracking branch 'origin/master' into integral_comp
RemyDegenne d76e2c3
remove semi_ in lp_space
RemyDegenne 533290e
remove primes in lp_space
RemyDegenne 2185b53
more undo in lp_space
RemyDegenne 5103d1b
undo
RemyDegenne bb533c9
undo bounded
RemyDegenne 56372a4
add references in docstring
RemyDegenne d418652
Update src/measure_theory/lp_space.lean
RemyDegenne File filter
Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Constructions like this are often hard to find in mathlib, because you don't think about them until you need them. While you're working here, would you mind adding a cross-reference to the similar constructions
continuous_linear_map.comp_left_continuous
,continuous_linear_map.comp_left_continuous_bounded
, just to increase visibility?There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Done!
Doing so, I realized that I did not know what
comp_LpL
was. It was in the same section as a lemma I wanted to generalize, so it got the same treatment, but I did not even read it.