Skip to content

[Merged by Bors] - feature(Analysis/Seminorm): Add closedBall equivalents of open ball results#22264

Closed
mans0954 wants to merge 2 commits intomasterfrom
mans0954/seminorm-closedBall
Closed

[Merged by Bors] - feature(Analysis/Seminorm): Add closedBall equivalents of open ball results#22264
mans0954 wants to merge 2 commits intomasterfrom
mans0954/seminorm-closedBall

Conversation

@mans0954
Copy link
Copy Markdown
Collaborator

@mans0954 mans0954 commented Feb 25, 2025 •
edited
Loading

Adds closedBall equivalents of existing (open) ball results. Specifically:

  • sub_mem_closedBall
  • neg_mem_closedBall_zero
  • neg_closedBall
  • smul_closedBall_preimage
  • closedBall_normSeminorm
  • blanced_closedBall_zero

balanced_closedBall_zero is used in #21002

Open in Gitpod

@mans0954 mans0954 mentioned this pull request Feb 25, 2025
Closed
2 tasks
@github-actions github-actions bot added the t-analysis Analysis (normed *, calculus) label Feb 25, 2025
@github-actions
Copy link
Copy Markdown

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

PR summary 64a3485dc6

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ balanced_closedBall_zero
+ closedBall_normSeminorm
+ neg_closedBall
+ neg_mem_closedBall_zero
+ smul_closedBall_preimage
+ sub_mem_closedBall

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

j-loreaux
j-loreaux reviewed Feb 26, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor

@j-loreaux j-loreaux left a comment

Choose a reason for hiding this comment

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

Thanks! It's always nice to have these conveniences.

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Feb 26, 2025
mathlib-bors bot pushed a commit that referenced this pull request Feb 26, 2025
@mans0954
feature(Analysis/Seminorm): Add closedBall equivalents of open ball r…
068c55c 
…esults (#22264)

Adds `closedBall` equivalents of existing (open) `ball` results. Specifically:

- `sub_mem_closedBall`
- `neg_mem_closedBall_zero`
- `neg_closedBall`
- `smul_closedBall_preimage`
- `closedBall_normSeminorm`
- `blanced_closedBall_zero`

`balanced_closedBall_zero` is used in #21002
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Feb 26, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feature(Analysis/Seminorm): Add closedBall equivalents of open ball results [Merged by Bors] - feature(Analysis/Seminorm): Add closedBall equivalents of open ball results Feb 26, 2025
@mathlib-bors mathlib-bors bot closed this Feb 26, 2025
@mathlib-bors mathlib-bors bot deleted the mans0954/seminorm-closedBall branch February 26, 2025 21:29
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@j-loreaux j-loreaux j-loreaux left review comments

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-analysis Analysis (normed *, calculus)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@mans0954 @j-loreaux