-
Notifications
You must be signed in to change notification settings - Fork 299
[Merged by Bors] - feat(integration): integral commutes with continuous linear maps #4167
Conversation
from the sphere eversion project.
src/measure_theory/set_integral.lean
Outdated
by simp [l1.clm_apply] | ||
|
||
/-- Composing `φ : α →₁[μ] E` with `L : E →L[ℝ] F`, seen as a `ℝ`-linear map on `α →₁[μ] E`. -/ | ||
def l1.clm_applyₗ (L : E →L[ℝ] F) : (α →₁[μ] E) →ₗ[ℝ] (α →₁[μ] F) := |
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.
It feels strange to have this one in the namespace measure_theory.l1
. I'd rather have it in continuous_linear_map
, just like continuous_linear_map.l1_apply
(maybe with more similar names)
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.
I changed all names and namespaces. I'm sorry I opened this PR without doing the name cleanup. I wanted Yury to have it and I was too fast.
src/measure_theory/set_integral.lean
Outdated
@@ -464,6 +464,135 @@ lemma continuous_at.integral_sub_linear_is_o_ae | |||
is_o (λ s, ∫ x in s, f x ∂μ - (μ s).to_real • f a) (λ s, (μ s).to_real) ((𝓝 a).lift' powerset) := | |||
(ha.mono_left inf_le_left).integral_sub_linear_is_o_ae hfm (μ.finite_at_nhds a) | |||
|
|||
section continuous_linear_map |
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.
section docstring, explaining what you are going to do in this paragraph, and why?
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.
I'm also fine with this one being merged first. It seems easy enough to fix the changes.
bors d+ |
✌️ PatrickMassot can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
bors merge |
👎 Rejected by label |
bors r+ |
from the sphere eversion project. Main result: ```lean continuous_linear_map.integral_apply_comm {α : Type*} [measurable_space α] {μ : measure α} {E : Type*} [normed_group E] [second_countable_topology E] [normed_space ℝ E] [complete_space E] [measurable_space E] [borel_space E] {F : Type*} [normed_group F] [second_countable_topology F] [normed_space ℝ F] [complete_space F] [measurable_space F] [borel_space F] {φ : α → E} (L : E →L[ℝ] F) (φ_meas : measurable φ) (φ_int : integrable φ μ) : ∫ a, L (φ a) ∂μ = L (∫ a, φ a ∂μ) ```
Pull request successfully merged into master. Build succeeded: |
from the sphere eversion project. Main result:
This PR doesn't build on #4170 but it will conflict, so should be merged later.