[Merged by Bors] - feat(MeasureTheory/Integral/RieszMarkovKakutani) prove that the Riesz content is regular and define the Riesz measure by yoh-tanimoto · Pull Request #20040 · leanprover-community/mathlib4

yoh-tanimoto · 2024-12-18T15:51:06Z

Prove regularity of RieszContent, define the Riesz measure μ Λ and prove basic properties.

Motivation: these definitions and lemmas will be used to prove the Riesz-Markov-Kakutani theorem, characterizing μ Λ.

In this PR, it is assumed to be NNReal-linear. In this way, the proof of the RMK theorem will be twice as long as a proof for Real-linear Λ because one cannot define -f. #12290 proves the RMK theorem for real linear Λ, using the Riesz measure defined in this PR through toNNRealLinear.

depends on: [Merged by Bors] - feat(Topology/ContinuousMap/CompactlySupported): add partialOrder #21206 for partialOrder

Most probably the naming Λ_mono is not good, but I don't know which is the right one.

github-actions · 2024-12-18T15:51:57Z

messageFile.md

…20126) Add instance `IsOrderBornology ℝ≥0`. motivation: I will need in #20040 (or a later PR) that the range of a compactly supported `NNReal`-valued function is bounded below and above. see also https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/IsOrderBornology.20.E2.84.9D.E2.89.A50 Co-authored-by: Yoh Tanimoto <57562556+yoh-tanimoto@users.noreply.github.com>

YaelDillies · 2024-12-25T18:24:28Z

Great to see this moving forward! Could you please address the comments I made on #12290 ? Thanks!

yoh-tanimoto · 2024-12-26T11:00:02Z

Thanks for your reviews! sure, I will do it.

Mathlib/MeasureTheory/Integral/RieszMarkovKakutani.lean

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

This reverts commit e35a2d8.

mathlib4-dependent-issues-bot · 2025-02-03T08:04:10Z

This PR/issue depends on:

~~[Merged by Bors] - feat(Topology/ContinuousMap/CompactlySupported): add partialOrder #21206~~
By Dependent Issues (🤖). Happy coding!

…gularity

github-actions · 2025-02-03T09:08:13Z

PR summary ec260d60bc

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ CompactlySupportedContinuousMap.monotone_of_nnreal
+ contentRegular_rieszContent
+ exists_add_of_le
+ le_rieszMeasure_of_isCompact_tsupport_subset
+ le_rieszMeasure_of_tsupport_subset
+ rieszContent_ne_top
+ rieszMeasure

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).

YaelDillies · 2025-02-03T10:18:32Z

Mathlib/MeasureTheory/Integral/RieszMarkovKakutani.lean

+/-- `rieszContent` gives a `Content` from `Λ : C_c(X, ℝ≥0) →ₗ[ℝ≥0] ℝ≥0`. Here `rieszContent Λ` is
+promoted to a measure. It will be later shown that
+`∫ (x : X), f x ∂(rieszMeasure Λ hΛ) = Λ f` for all `f : C_c(X, ℝ≥0)`. -/


What about

Suggested change

/-- `rieszContent` gives a `Content` from `Λ : C_c(X, ℝ≥0) →ₗ[ℝ≥0] ℝ≥0`. Here `rieszContent Λ` is

promoted to a measure. It will be later shown that

`∫ (x : X), f x ∂(rieszMeasure Λ hΛ) = Λ f` for all `f : C_c(X, ℝ≥0)`. -/

/-- Given a `ℝ≥0`-linear functional `Λ` on `C_c(X, ℝ≥0)`. the Riesz measure is a measure which

respects `∫ x, f x ∂(rieszMeasure Λ) = Λ f` for all `f : C_c(X, ℝ≥0)`. -/

Well, I'm not sure... this will be proved in the later theorem, and this is not the definition of rieszMeasure.

Yeah but the definition is just below. This doesn't necessarily need to be repeated in the docstring.

If you do want to repeat it, you can do

Suggested change

/-- `rieszContent` gives a `Content` from `Λ : C_c(X, ℝ≥0) →ₗ[ℝ≥0] ℝ≥0`. Here `rieszContent Λ` is

promoted to a measure. It will be later shown that

`∫ (x : X), f x ∂(rieszMeasure Λ hΛ) = Λ f` for all `f : C_c(X, ℝ≥0)`. -/

/-- Given a `ℝ≥0`-linear functional `Λ` on `C_c(X, ℝ≥0)`. the Riesz measure is a measure which

respects `∫ x, f x ∂(rieszMeasure Λ) = Λ f` for all `f : C_c(X, ℝ≥0)`.

This is defined as the measure corresponding to the Riesz content of `Λ`. -/

My point is that docstrings will mostly be read after the fact. People will see them either when hovering over the definition in a later file or in the docs

Mathlib/MeasureTheory/Integral/RieszMarkovKakutani.lean

Mathlib/Topology/ContinuousMap/CompactlySupported.lean

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

YaelDillies

Thanks!

maintainer delegate

github-actions · 2025-02-03T11:27:01Z

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

…gularity

sgouezel · 2025-02-05T09:26:38Z

bors r+

… content is regular and define the Riesz measure (#20040) Prove regularity of `RieszContent`, define the Riesz measure `μ Λ` and prove basic properties. Motivation: these definitions and lemmas will be used to prove the Riesz-Markov-Kakutani theorem, characterizing `μ Λ`. In this PR, it is assumed to be NNReal-linear. In this way, the proof of the RMK theorem will be twice as long as a proof for `Real`-linear `Λ` because one cannot define `-f`. #12290 proves the RMK theorem for real linear `Λ`, using the Riesz measure defined in this PR through `toNNRealLinear`. Co-authored-by: Yoh Tanimoto <57562556+yoh-tanimoto@users.noreply.github.com>

mathlib-bors · 2025-02-05T09:52:41Z

Pull request successfully merged into master.

Build succeeded:

* 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) ...

… content is regular and define the Riesz measure (#20040) Prove regularity of `RieszContent`, define the Riesz measure `μ Λ` and prove basic properties. Motivation: these definitions and lemmas will be used to prove the Riesz-Markov-Kakutani theorem, characterizing `μ Λ`. In this PR, it is assumed to be NNReal-linear. In this way, the proof of the RMK theorem will be twice as long as a proof for `Real`-linear `Λ` because one cannot define `-f`. #12290 proves the RMK theorem for real linear `Λ`, using the Riesz measure defined in this PR through `toNNRealLinear`. Co-authored-by: Yoh Tanimoto <57562556+yoh-tanimoto@users.noreply.github.com>

yoh-tanimoto added 2 commits December 18, 2024 16:21

rieszContentRegular

1ed3152

Update RieszMarkovKakutani.lean

fadf892

github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Dec 18, 2024

Update RieszMarkovKakutani.lean

f120a2e

github-actions bot removed the large-import Automatically added label for PRs with a significant increase in transitive imports label Dec 18, 2024

yoh-tanimoto added t-measure-probability Measure theory / Probability theory large-import Automatically added label for PRs with a significant increase in transitive imports labels Dec 18, 2024

Update RieszMarkovKakutani.lean

9f531f9

github-actions bot removed the large-import Automatically added label for PRs with a significant increase in transitive imports label Dec 18, 2024

yoh-tanimoto added the RFC Request for comment label Dec 18, 2024

Update NNReal.lean

04b5ba1

yoh-tanimoto mentioned this pull request Dec 20, 2024

[Merged by Bors] - feat(Mathlib/Topology/Instances/NNReal): add IsOrderBornology ℝ≥0 #20126

Closed

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 25, 2024

Merge branch 'master' into yoh-tanimoto-RMK-regularity

2a9a5f1

leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 25, 2024

yoh-tanimoto mentioned this pull request Dec 25, 2024

[Merged by Bors] - feat(MeasureTheory/Integral): the Riesz-Markov-Kakutani theorem for Real-linear functionals #12290

Closed

5 tasks

implementing comments in #12290

26e2ed3

YaelDillies reviewed Dec 28, 2024

View reviewed changes

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 28, 2024

yoh-tanimoto and others added 7 commits December 28, 2024 19:40

Update Mathlib/MeasureTheory/Integral/RieszMarkovKakutani.lean

c8e50de

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Update Mathlib/MeasureTheory/Integral/RieszMarkovKakutani.lean

e35a2d8

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Update Mathlib/MeasureTheory/Integral/RieszMarkovKakutani.lean

6c30ce8

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Update Mathlib/MeasureTheory/Integral/RieszMarkovKakutani.lean

d2a1717

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Update Mathlib/MeasureTheory/Integral/RieszMarkovKakutani.lean

e1c3fda

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Update Mathlib/MeasureTheory/Integral/RieszMarkovKakutani.lean

87f0ead

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Revert "Update Mathlib/MeasureTheory/Integral/RieszMarkovKakutani.lean"

9743eb7

This reverts commit e35a2d8.

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 3, 2025

Merge remote-tracking branch 'origin/master' into yoh-tanimoto-RMK-re…

03c5aca

…gularity

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 3, 2025

YaelDillies reviewed Feb 3, 2025

View reviewed changes

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 3, 2025

yoh-tanimoto and others added 4 commits February 3, 2025 12:06

Update Mathlib/MeasureTheory/Integral/RieszMarkovKakutani.lean

9ef1518

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Update Mathlib/MeasureTheory/Integral/RieszMarkovKakutani.lean

9bae393

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Update Mathlib/Topology/ContinuousMap/CompactlySupported.lean

9e18a68

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

adapt

84563f8

yoh-tanimoto added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Feb 3, 2025

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Feb 3, 2025

YaelDillies approved these changes Feb 3, 2025

View reviewed changes

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Feb 3, 2025

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 3, 2025

Merge remote-tracking branch 'origin/master' into yoh-tanimoto-RMK-re…

ec260d6

…gularity

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 3, 2025

ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Feb 5, 2025

mathlib-bors bot closed this Feb 5, 2025

mathlib-bors bot deleted the yoh-tanimoto-RMK-regularity branch February 5, 2025 09:52

Conversation

yoh-tanimoto commented Dec 18, 2024 • edited by YaelDillies Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Dec 18, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

YaelDillies commented Dec 25, 2024

Uh oh!

yoh-tanimoto commented Dec 26, 2024

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mathlib4-dependent-issues-bot commented Feb 3, 2025

Uh oh!

github-actions bot commented Feb 3, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary ec260d60bc

Import changes for modified files

Declarations diff

Uh oh!

YaelDillies Feb 3, 2025

Choose a reason for hiding this comment

Uh oh!

yoh-tanimoto Feb 3, 2025

Choose a reason for hiding this comment

Uh oh!

YaelDillies Feb 3, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

YaelDillies Feb 3, 2025

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Feb 3, 2025

Uh oh!

sgouezel commented Feb 5, 2025

Uh oh!

mathlib-bors bot commented Feb 5, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

yoh-tanimoto commented Dec 18, 2024 •

edited by YaelDillies

Loading

github-actions bot commented Dec 18, 2024 •

edited

Loading

github-actions bot commented Feb 3, 2025 •

edited

Loading

YaelDillies Feb 3, 2025 •

edited

Loading