Skip to content

[Merged by Bors] - feat(Topology/ContinuousMap/CompactlySupported): turn a positive Real-linear functional into a NNReal-linear functional#20257

Closed
yoh-tanimoto wants to merge 26 commits intomasterfrom
yoh-tanimoto-tonnreallinear
Closed

[Merged by Bors] - feat(Topology/ContinuousMap/CompactlySupported): turn a positive Real-linear functional into a NNReal-linear functional#20257
yoh-tanimoto wants to merge 26 commits intomasterfrom
yoh-tanimoto-tonnreallinear

Conversation

@yoh-tanimoto
Copy link
Copy Markdown
Collaborator

@yoh-tanimoto yoh-tanimoto commented Dec 26, 2024 •
edited by YaelDillies
Loading

Define toNNRealLinear that maps positive Real-linear functionals to NNReal-linear functionals and prove that it is injective.

Motivation: I use this to define rieszMeasure for Real-linear functional in #12290.

@github-actions
Copy link
Copy Markdown

github-actions bot commented Dec 26, 2024 •
edited
Loading

PR summary 66d84172b9

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ coeNNRealReal_zero
+ coe_toRealLinearMap
+ nnrealPart_sub_nnrealPart_neg
+ toNNRealLinear
+ toNNRealLinear_apply
+ toNNRealLinear_inj
+ toReal
+ toRealLinearMap
+ toRealLinearMap_apply
+ toRealLinearMap_apply_apply
+ toReal_add
+ toReal_apply
+ toReal_nonneg
+ toReal_smul

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

@github-actions github-actions bot added the t-topology Topological spaces, uniform spaces, metric spaces, filters label Dec 26, 2024
@yoh-tanimoto yoh-tanimoto added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Dec 26, 2024
@yoh-tanimoto yoh-tanimoto mentioned this pull request Dec 26, 2024
Closed
5 tasks
@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 Dec 26, 2024
YaelDillies
YaelDillies reviewed Dec 27, 2024
View reviewed changes
@YaelDillies YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 27, 2024
@yoh-tanimoto 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 Dec 28, 2024
@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 Dec 28, 2024
@YaelDillies YaelDillies changed the title feat(Topology/ContinuousMap/CompactlySupported): add map from positive Real linear functionas to NNReal linear functionals feat(Topology/ContinuousMap/CompactlySupported): turn a positive Real-linear functional into a NNReal-linear functional Dec 28, 2024
YaelDillies
YaelDillies reviewed Dec 28, 2024
View reviewed changes
@YaelDillies YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 28, 2024
@yoh-tanimoto 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 Jan 12, 2025
@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 Jan 12, 2025
@YaelDillies YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 12, 2025
@yoh-tanimoto 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 Jan 12, 2025
@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 Jan 12, 2025
yoh-tanimoto and others added 2 commits February 3, 2025 10:58
@yoh-tanimoto @YaelDillies
Update Mathlib/Topology/ContinuousMap/CompactlySupported.lean
0b577ce 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@yoh-tanimoto @YaelDillies
Update Mathlib/Topology/ContinuousMap/CompactlySupported.lean
2f304f8 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
YaelDillies
YaelDillies reviewed Feb 3, 2025
View reviewed changes
yoh-tanimoto and others added 4 commits February 3, 2025 11:45
@yoh-tanimoto @YaelDillies
Update Mathlib/Topology/ContinuousMap/CompactlySupported.lean
bca96ef 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@yoh-tanimoto @YaelDillies
Update Mathlib/Topology/ContinuousMap/CompactlySupported.lean
45b8733 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@yoh-tanimoto @YaelDillies
Update Mathlib/Topology/ContinuousMap/CompactlySupported.lean
af837a2 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@yoh-tanimoto @YaelDillies
Update Mathlib/Topology/ContinuousMap/CompactlySupported.lean
54b26da 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
YaelDillies
YaelDillies reviewed Feb 3, 2025
View reviewed changes
@yoh-tanimoto 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 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
YaelDillies approved these changes Feb 3, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

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

I pushed a hopefully final golf. If you're happy with it, let's merge!

maintainer delegate

@github-actions
Copy link
Copy Markdown

github-actions bot commented Feb 3, 2025

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

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Feb 3, 2025
@yoh-tanimoto
Copy link
Copy Markdown
Collaborator Author

yoh-tanimoto commented Feb 3, 2025

thank you very much for your reviews and suggestions!

jcommelin
jcommelin reviewed Feb 3, 2025
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@ghost 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 3, 2025
mathlib-bors bot pushed a commit that referenced this pull request Feb 3, 2025
@yoh-tanimoto @YaelDillies
feat(Topology/ContinuousMap/CompactlySupported): turn a positive `Rea…
989a8db 
…l`-linear functional into a `NNReal`-linear functional (#20257)

Define `toNNRealLinear` that maps positive `Real`-linear functionals to `NNReal`-linear functionals and prove that it is injective.



Co-authored-by: Yoh Tanimoto <57562556+yoh-tanimoto@users.noreply.github.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Feb 3, 2025

Build failed (retrying...):

mathlib-bors bot pushed a commit that referenced this pull request Feb 3, 2025
@yoh-tanimoto @YaelDillies
feat(Topology/ContinuousMap/CompactlySupported): turn a positive `Rea…
2549057 
…l`-linear functional into a `NNReal`-linear functional (#20257)

Define `toNNRealLinear` that maps positive `Real`-linear functionals to `NNReal`-linear functionals and prove that it is injective.



Co-authored-by: Yoh Tanimoto <57562556+yoh-tanimoto@users.noreply.github.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Feb 3, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Topology/ContinuousMap/CompactlySupported): turn a positive Real-linear functional into a NNReal-linear functional [Merged by Bors] - feat(Topology/ContinuousMap/CompactlySupported): turn a positive Real-linear functional into a NNReal-linear functional Feb 3, 2025
@mathlib-bors mathlib-bors bot closed this Feb 3, 2025
@mathlib-bors mathlib-bors bot deleted the yoh-tanimoto-tonnreallinear branch February 3, 2025 17:32
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin left review comments

@YaelDillies YaelDillies YaelDillies approved these changes

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-topology Topological spaces, uniform spaces, metric spaces, filters

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@yoh-tanimoto @mathlib4-dependent-issues-bot @jcommelin @YaelDillies @leanprover-community-bot-assistant