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] - refactor(measure_theory/simple_func_dense): generalize approximation results from L^1 to L^p #8114
Conversation
Thanks for this work! |
Sure, that sounds like a good rule to have! I'll make the change. |
🎉 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! |
Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
@RemyDegenne I switched to |
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.
Looks good to me!
I would change a few lemma names, though.
Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
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.
LGTM, thanks!
bors r+ |
…results from L^1 to L^p (#8114) Simple functions are dense in L^p. The argument for `1 ≤ p < ∞` is exactly the same as for `p = 1`, which was already in mathlib: construct a suitable sequence of pointwise approximations and apply the Dominated Convergence Theorem. This PR refactors to provide the general-`p` result. The argument for `p = ∞` requires finite-dimensionality of `E` and a different approximating sequence, so is left for another PR.
Pull request successfully merged into master. Build succeeded: |
…construction of embedding of L1 simple funcs (#8185) At the moment, there is a low-level construction in `measure_theory/simple_func_dense` for the approximation of an element of L1 by simple functions, and this is generalized to a more abstract version (with a normed space `L1.simple_func` and a dense linear embedding of this into `L1`) in `measure_theory/bochner_integration`. #8114 generalized the low-level construction, and I am thinking of rewriting the more abstract version to apply to `Lp`, too. But since this will all be more generally useful than in the construction of the Bochner integral, and since the Bochner integral file is very long, I propose moving all this material into `measure_theory/simple_func_dense`. This PR shows what it would look like. There are no mathematical changes.
…results from L^1 to L^p (#8114) Simple functions are dense in L^p. The argument for `1 ≤ p < ∞` is exactly the same as for `p = 1`, which was already in mathlib: construct a suitable sequence of pointwise approximations and apply the Dominated Convergence Theorem. This PR refactors to provide the general-`p` result. The argument for `p = ∞` requires finite-dimensionality of `E` and a different approximating sequence, so is left for another PR.
…construction of embedding of L1 simple funcs (#8185) At the moment, there is a low-level construction in `measure_theory/simple_func_dense` for the approximation of an element of L1 by simple functions, and this is generalized to a more abstract version (with a normed space `L1.simple_func` and a dense linear embedding of this into `L1`) in `measure_theory/bochner_integration`. #8114 generalized the low-level construction, and I am thinking of rewriting the more abstract version to apply to `Lp`, too. But since this will all be more generally useful than in the construction of the Bochner integral, and since the Bochner integral file is very long, I propose moving all this material into `measure_theory/simple_func_dense`. This PR shows what it would look like. There are no mathematical changes.
Simple functions are dense in L^p. The argument for
1 ≤ p < ∞
is exactly the same as forp = 1
, which was already in mathlib: construct a suitable sequence of pointwise approximations and apply the Dominated Convergence Theorem. This PR refactors to provide the general-p
result.The argument for
p = ∞
requires finite-dimensionality ofE
and a different approximating sequence, so is left for another PR.