Skip to content

feat: locallyIntegrableOn_smul_iff#39217

Open
grunweg wants to merge 5 commits into
leanprover-community:masterfrom
grunweg:temp
Open

feat: locallyIntegrableOn_smul_iff#39217
grunweg wants to merge 5 commits into
leanprover-community:masterfrom
grunweg:temp

Conversation

@grunweg
Copy link
Copy Markdown
Contributor

@grunweg grunweg commented May 11, 2026 •
edited
Loading

From Sobolev spaces. Written by (some unspecified subset of) Floris, Filippo and me.

Open in Gitpod

@github-actions github-actions Bot added the t-measure-probability Measure theory / Probability theory label May 11, 2026
@github-actions
Copy link
Copy Markdown

github-actions Bot commented May 11, 2026 •
edited
Loading

PR summary 578f407c34

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ LocallyIntegrableOn.smul
+ integrableAtFilter_neg_iff
+ integrableAtFilter_smul_iff
+ integrableAtFilter_smul_iff'
+ integrableAtFilter_zero
+ locallyIntegrableOn_neg_iff
+ locallyIntegrableOn_smul_iff

You can run this locally as follows 
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

No changes to strong technical debt.
No changes to weak technical debt.

@grunweg grunweg changed the title chore: extracted from #32305 feat: locallyIntegrableOn_smul_iff May 11, 2026
@grunweg grunweg mentioned this pull request May 11, 2026
Open
3 tasks
grunweg
grunweg commented May 11, 2026
View reviewed changes
Comment thread Mathlib/MeasureTheory/Function/LocallyIntegrable.lean Outdated
Comment thread Mathlib/MeasureTheory/Function/LocallyIntegrable.lean Outdated
Comment thread Mathlib/MeasureTheory/Function/LocallyIntegrable.lean Outdated
Comment thread Mathlib/MeasureTheory/Function/LocallyIntegrable.lean Outdated
@grunweg
Fix nits
1ee629e 
Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
grunweg
grunweg commented May 11, 2026
View reviewed changes
Comment thread Mathlib/MeasureTheory/Function/LocallyIntegrable.lean Outdated
grunweg added 2 commits May 11, 2026 20:24
@grunweg
Apply suggestions from code review
775b927 
Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
@grunweg
Add more general lemmas for integrableAtFilter
4e2e06e
@ADedecker ADedecker self-assigned this May 11, 2026
@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented May 11, 2026

Updated the proofs with the new strategy (thanks for the suggestion). This is ready for another look!

ADedecker
ADedecker reviewed May 11, 2026
View reviewed changes
Comment thread Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
Comment on lines +217 to +220
@[simp] theorem locallyIntegrableOn_neg_iff {f : X → E} :
LocallyIntegrableOn (-f) s μ ↔ LocallyIntegrableOn f s μ := by
unfold LocallyIntegrableOn
simp_rw [MeasureTheory.integrableAtFilter_neg_iff]
Copy link
Copy Markdown
Member

@ADedecker ADedecker May 11, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could we have this for LocallyIntegrable as well?

Comment thread Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
Comment on lines +227 to +232
-- TODO: generalise this to ENormed spaces, once there are suitable typeclasses
@[simp] theorem locallyIntegrableOn_smul_iff {𝕜 : Type*} [NormedField 𝕜] [NormedSpace 𝕜 E]
{f : X → E} (c : 𝕜) :
LocallyIntegrableOn (c • f) s μ ↔ c = 0 ∨ LocallyIntegrableOn f s μ := by
unfold LocallyIntegrableOn
grind [integrableAtFilter_smul_iff]
Copy link
Copy Markdown
Member

@ADedecker ADedecker May 11, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same

Comment thread Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
-- TODO: generalise this to ENormed spaces, once there are suitable typeclasses
protected theorem LocallyIntegrableOn.smul {𝕜 : Type*} [NormedField 𝕜] [NormedSpace 𝕜 E]
{f : X → E} (hf : LocallyIntegrableOn f s μ) (c : 𝕜) :
LocallyIntegrableOn (c • f) s μ := fun x hx ↦ (hf x hx).smul c
Copy link
Copy Markdown
Member

@ADedecker ADedecker May 11, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
LocallyIntegrableOn (c • f) s μ := fun x hx ↦ (hf x hx).smul c
LocallyIntegrableOn (c • f) s μ := fun x hx ↦ (hf x hx).smul c

@grunweg grunweg added the awaiting-author A reviewer has asked the author a question or requested changes. label May 11, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@ADedecker ADedecker ADedecker left review comments

Assignees

@ADedecker ADedecker

Labels

awaiting-author A reviewer has asked the author a question or requested changes. t-measure-probability Measure theory / Probability theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@grunweg @ADedecker