Skip to content

[Merged by Bors] - doc: document design choice of (AE)StronglyMeasurable.enorm and edist#21423

Closed
grunweg wants to merge 4 commits intomasterfrom
MR-generalise-enorm-3
Closed

[Merged by Bors] - doc: document design choice of (AE)StronglyMeasurable.enorm and edist#21423
grunweg wants to merge 4 commits intomasterfrom
MR-generalise-enorm-3

Conversation

@grunweg
Copy link
Copy Markdown
Contributor

@grunweg grunweg commented Feb 4, 2025 •
edited
Loading

It intentionally only proves (a.e.) measurability, not (a.e.) strong measurability.

Discovered while generalising lemmas to enormed spaces, for the Carleson project.

Open in Gitpod

@grunweg grunweg added WIP Work in progress blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Feb 4, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Feb 4, 2025 •
edited
Loading

PR summary eb7346ba7f

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Feb 4, 2025
@grunweg grunweg force-pushed the MR-generalise-enorm-3 branch from 6956415 to af27d61 Compare February 4, 2025 14:49
@grunweg grunweg added easy < 20s of review time. See the lifecycle page for guidelines. awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed WIP Work in progress labels Feb 4, 2025
@grunweg grunweg changed the title WIP: generalise to enorm, part 3 fix: statement of AEStronglyMeasurable.enorm Feb 4, 2025
@fpvandoorn
Copy link
Copy Markdown
Member

fpvandoorn commented Feb 4, 2025

I also noticed this, and I wasn't sure whether this was a feature or a bug, but it did surprise me (in the case I needed it I did need AEMeasurable)

@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented Feb 4, 2025 •
edited
Loading

I think this is a bug - the lemma name and statement don't match, so one should be fixed.
I'm inclined to go for "stronger lemma conclusion", as I don't have reasons otherwise.

Edit: Thinking over it again: I would expect a lemma MyClass.enorm to prove that MyClass enorm holds, i.e. expect the conclusion to be about StronglyAEMeasurable (in particular, since that is a true statement). But most of all, I would expect the analogous lemmas for norm, nnnorm and enorm to be consistent. The simplest heuristic (match the existing lemmas) leads to this PR.

@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented Feb 4, 2025

It builds now, so I'm hopefully CI will pass soon.

@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Feb 4, 2025
@grunweg grunweg mentioned this pull request Feb 4, 2025
Open
2 tasks
@fpvandoorn
Copy link
Copy Markdown
Member

fpvandoorn commented Feb 4, 2025

The same design decision is used in AEStronglyMeasurable.edist, which goes back to leanprover-community/mathlib3#12985
I think this is done intentionally, since often it is what you want, although it is somewhat surprising.
@sgouezel was this done intentionally?

I'm personally fine with the change or to keep it as-is but add a docstring with an explanation (or to keep both versions).

@fpvandoorn fpvandoorn requested a review from sgouezel February 4, 2025 21:18
@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented Feb 4, 2025 •
edited
Loading

Thanks for checking and the context! I've checked git blame: this lemma exists in the current form since the port (so was introduced in mathlib3).

I personally find the lemma both surprising (it does not say what I would expect it to) and inconsistent (its norm and nnnorm cousins are different). Having audited every single use, I agree that the previous form was shorter. If there is a preference to leave the statement, a comment documenting this decision would also be fine with me.

eric-wieser
eric-wieser reviewed Feb 5, 2025
View reviewed changes
Copy link
Copy Markdown
Member

@eric-wieser eric-wieser left a comment •
edited
Loading

Choose a reason for hiding this comment

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

Can the same be done to edist?

@sgouezel
Copy link
Copy Markdown
Contributor

sgouezel commented Feb 5, 2025

Yes, it is intentional: AEStronglyMeasurable is used most of the time in a context of Bochner integrals (so, for functions taking values in a vector space), while for functions taking values in ENNReal the useful version is almost always AEMeasurable. You can see that from the applications: with the modified version, in all the examples you use .enorm, and then you compose it with .aemeasurable, so all examples become longer.

So, I think we should keep the current statement, which is the useful one, but we also improve the docstring to explain this design decision.

@grunweg grunweg force-pushed the MR-generalise-enorm-3 branch from 3981eab to 4bf407c Compare February 5, 2025 09:40
@grunweg grunweg changed the title fix: statement of AEStronglyMeasurable.enorm doc: document design choice of StronglyMeasurable.enorm Feb 5, 2025
@grunweg grunweg removed the easy < 20s of review time. See the lifecycle page for guidelines. label Feb 5, 2025
@grunweg
doc: document design choice of (AE)StronglyMeasurable.enorm
c897362 
It intentionally only proves (a.e.) measurability, not (a.e.) strong measurability.
@grunweg grunweg force-pushed the MR-generalise-enorm-3 branch from 4bf407c to c897362 Compare February 5, 2025 09:43
@grunweg grunweg changed the title doc: document design choice of StronglyMeasurable.enorm doc: document design choice of (AE)StronglyMeasurable.enorm Feb 5, 2025
@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented Feb 5, 2025

I have reverted the statement change, and added a comment. Please let me know if you prefer me to rephrase it.

fpvandoorn
fpvandoorn reviewed Feb 5, 2025
View reviewed changes
Copy link
Copy Markdown
Member

@fpvandoorn fpvandoorn left a comment

Choose a reason for hiding this comment

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

Please add the same comments to edist lemmas
Please turn them into docstrings
I would remove "(At the time of writing, no application of this lemma used strong measurability.)"

Otherwise LGTM

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Feb 5, 2025

✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@ghost ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Feb 5, 2025
@grunweg grunweg changed the title doc: document design choice of (AE)StronglyMeasurable.enorm doc: document design choice of (AE)StronglyMeasurable.enorm and edist Feb 5, 2025
@grunweg grunweg added the auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. label Feb 5, 2025
@ghost
Copy link
Copy Markdown

ghost commented Feb 5, 2025

As this PR is labelled auto-merge-after-CI, we are now sending it to bors:

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Feb 5, 2025
mathlib-bors bot pushed a commit that referenced this pull request Feb 5, 2025
@grunweg
doc: document design choice of (AE)StronglyMeasurable.enorm and `edis…
6cfdcb3 
…t` (#21423)

It intentionally only proves (a.e.) measurability, not (a.e.) strong measurability.

Discovered while generalising lemmas to enormed spaces, for the Carleson project.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Feb 5, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title doc: document design choice of (AE)StronglyMeasurable.enorm and edist [Merged by Bors] - doc: document design choice of (AE)StronglyMeasurable.enorm and edist Feb 5, 2025
@mathlib-bors mathlib-bors bot closed this Feb 5, 2025
@mathlib-bors mathlib-bors bot deleted the MR-generalise-enorm-3 branch February 5, 2025 14:36
Julian added a commit that referenced this pull request Feb 5, 2025
@Julian
Merge remote-tracking branch 'origin/master' into bhargava-factorial
ae1775b 
* origin/master: (103 commits)
  chore(PresheafedSpace): remove `mk_coe` and some comments from porting  (#21382)
  refactor(CategoryTheory): `ConcreteCategory` instance for `FintypeCat` (#21466)
  refactor(Algebra/Category): clean up remaining uses of `HasForget` (#21460)
  chore(Algebra/Field/Basic): make some arguments implicit (#21453)
  chore(LinearAlgebra/TensorProduct): upgrade `TensorProduct.prodRight` (#21432)
  docs(Logic/Function/Defs): missing backticks (#21459)
  style(Logic/Embedding/Set): unindent (#21457)
  doc: document design choice of (AE)StronglyMeasurable.enorm and `edist` (#21423)
  perf(RingTheory/Artinian): reorder arguments in `IsArtinianRing.isMaximal_of_isPrime` (#21449)
  feat(Probability): first two derivatives of `cgf` (#21223)
  feat(RingTheory): `Ring.KrullDimLE` type class (#21452)
  chore(Probability/ProbabilityMassFunction/Binomial): typo "bernoulli" (#21455)
  chore: remove unused argument (#21393)
  feat(MeasureTheory/Integral/RieszMarkovKakutani) prove that the Riesz content is regular and define the Riesz measure (#20040)
  chore(Topology/Algebra/ContinuousMonoidHom): do not depend on `ContinuousLinearMap` (#21443)
  doc(CategoryTheory/Monoidal/Category): fix expression in docs (#21445)
  refactor(Order/CompleteBooleanAlgebra): a complete lattice which is a Heyting algebra is automatically a frame (#21391)
  chore: cleanup porting notes in TuringMachine (#20821)
  chore: remove @[simp] when the discr_key is a lambda (#21395)
  feat/doc: split files, add documentation (#21421)
  feat(Data/Set/Lattice): iUnion + insertion  (#21322)
  feat(Factorial): k! divides the product of any k successive integers (#21332)
  feat(CI): bench-after-CI (#21414)
  feat: primitive group actions (#12052)
  feat(Algebra/GroupWithZero/Int): add lemmas about Zm0 (#21370)
  feat(CategoryTheory): small classes of morphisms (#21411)
  feat(CategoryTheory): (co)limits of constant functors (#21412)
  chore: rename isUnit_ofPowEqOne (#21407)
  chore: split mapDomain out of MonoidAlgebra.Defs (#21398)
  chore: generalise lemmas to `ENorm` spaces, part 1 (#21380)
  chore: add `simp` to `Setoid.refl` (#21107)
  chore: tidy various files (#21406)
  chore(Geometry/Manifold/IsManifold): split out material on extended charts (#21219)
  refactor: introduce `Ideal.IsTwoSided` class for quotients of noncommutative rings (#17930)
  chore(Algebra/Category/ModuleCat): delete `ModuleCat.hasForgetModuleCat` (#21425)
  feat(RingTheory): unramified iff `κ(q)/κ(p)` is separable and `pS_q = qS_q` (#20690)
  doc(Order/Heyting/Basic): Coheyting difference is not right adjoint but left adjoint (#21418)
  chore: move ProofWidgets to v0.0.51 (#21416)
  chore: rename mem_nonZeroDivisor_of_injective and comap_nonZeroDivisor_le_of_injective (#21408)
  feat: drop ordering assumption in `RootPairing.coxeterWeight_mem_set_of_isCrystallographic` (#21122)
  feat(AlgebraicGeometry): the diagonal of an unramified morphism is an open immersion (#21386)
  feat(Data/LinearIndependent): iff versions of smul action on independent sets (#21383)
  chore(Combinatorics/SimpleGraph): Fix `hadj` naming (#21389)
  chore: rename AnalyticAt.order_neq_top_iff (#21388)
  fix: bug in daily.yml (#21401)
  chore: remove `@[simp]` from `CategoryTheory.Discrete.functor_map` (#21392)
  chore(Algebra/PUnitInstances): generalise universes (#21381)
  feat(RingTheory/PowerSeries): describe when power series map is zero (#21379)
  feat(Tactic/Linter): options to in/exclude definitions and private decls (#21374)
  feat: the prime spectrum is quasi-separated (#21362)
  ...
pfaffelh pushed a commit that referenced this pull request Feb 7, 2025
@grunweg
doc: document design choice of (AE)StronglyMeasurable.enorm and `edis…
9c0b0a5 
…t` (#21423)

It intentionally only proves (a.e.) measurability, not (a.e.) strong measurability.

Discovered while generalising lemmas to enormed spaces, for the Carleson project.
@grunweg grunweg added the carleson part of the ongoing formalization of Carleson's theorem label Jul 25, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

@fpvandoorn fpvandoorn fpvandoorn left review comments

@sgouezel sgouezel Awaiting requested review from sgouezel

Assignees

No one assigned

Labels

auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. carleson part of the ongoing formalization of Carleson's theorem delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@grunweg @fpvandoorn @sgouezel @eric-wieser @mathlib4-dependent-issues-bot