Skip to content

[Merged by Bors] - refactor(PiTensorProduct/{InjectiveNorm, ProjectiveNorm}): switch NormedSpace instance to projectiveSeminorm#35568

Closed
goliath-klein wants to merge 10 commits intoleanprover-community:masterfrom
goliath-klein:pitp-seminorms-switch-instance
Closed

[Merged by Bors] - refactor(PiTensorProduct/{InjectiveNorm, ProjectiveNorm}): switch NormedSpace instance to projectiveSeminorm#35568
goliath-klein wants to merge 10 commits intoleanprover-community:masterfrom
goliath-klein:pitp-seminorms-switch-instance

Conversation

@goliath-klein
Copy link
Copy Markdown
Contributor

@goliath-klein goliath-klein commented Feb 20, 2026 •
edited by tb65536
Loading

The PR switches the NormedSpace instance on PiTensorProducts from injectiveSeminorm to projectiveSeminorm and updates all follow-up results.

The signature of norm_eval_le_projectiveSeminorm is changed to match the one of norm_eval_le_injectiveSeminorm.

This is the second in a series of three PRs with the goal to deprecate PiTensorProuduct.injectiveSeminorm.

This series is the result of splitting up #34137. More discussion there.

Co-authored-by: Davood H. H. Tehrani

Open in Gitpod

@github-actions github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Feb 20, 2026
@github-actions
Copy link
Copy Markdown

github-actions bot commented Feb 20, 2026

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

@goliath-klein goliath-klein mentioned this pull request Feb 20, 2026
Open
2 tasks
@github-actions
Copy link
Copy Markdown

github-actions bot commented Feb 20, 2026 •
edited
Loading

PR summary b029f5e21d

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ instance : Norm (⨂[𝕜] i, E i)
+ instance : NormedSpace 𝕜 (⨂[𝕜] i, E i) := ⟨projectiveSeminorm_smul_le⟩
+ norm_def
- instance : NormedSpace 𝕜 (⨂[𝕜] i, E i)

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

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

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

No changes to technical debt.

You can run this locally as

./scripts/reporting/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).

@goliath-klein goliath-klein mentioned this pull request Feb 20, 2026
Closed
@mathlib-dependent-issues mathlib-dependent-issues bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Feb 20, 2026
@mathlib-dependent-issues mathlib-dependent-issues bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 6, 2026
@mathlib-dependent-issues
Copy link
Copy Markdown

mathlib-dependent-issues bot commented Mar 6, 2026

This PR/issue depends on:

@robin-carlier robin-carlier added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 13, 2026
@goliath-klein
Copy link
Copy Markdown
Contributor Author

goliath-klein commented Mar 13, 2026

Thanks.

-awaiting-author

@github-actions github-actions bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 13, 2026
@robin-carlier robin-carlier added the t-analysis Analysis (normed *, calculus) label Mar 27, 2026
robin-carlier
robin-carlier reviewed Mar 27, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@robin-carlier robin-carlier left a comment

Choose a reason for hiding this comment

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

Thanks!

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 27, 2026

🚀 Pull request has been placed on the maintainer queue by robin-carlier.

pull_request_review, wf_run

@mathlib-triage mathlib-triage bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Mar 27, 2026
@riccardobrasca
Copy link
Copy Markdown
Member

riccardobrasca commented Mar 27, 2026

Thanks!

bors merge

@mathlib-triage mathlib-triage bot 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 Mar 27, 2026
mathlib-bors bot pushed a commit that referenced this pull request Mar 27, 2026
@goliath-klein @pre-commit-ci-lite
refactor(PiTensorProduct/{InjectiveNorm, ProjectiveNorm}): switch Nor…
c28b5a8 
…medSpace instance to `projectiveSeminorm` (#35568)

The PR switches the `NormedSpace` instance on `PiTensorProduct`s from `injectiveSeminorm` to `projectiveSeminorm` and updates all follow-up results.

The signature of `norm_eval_le_projectiveSeminorm` is changed to match the one of `norm_eval_le_injectiveSeminorm`.

This is the second in a series of three PRs with the goal to [deprecate `PiTensorProuduct.injectiveSeminorm`](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/injectiveSeminorm/with/568798633).

Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 27, 2026

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title refactor(PiTensorProduct/{InjectiveNorm, ProjectiveNorm}): switch NormedSpace instance to projectiveSeminorm [Merged by Bors] - refactor(PiTensorProduct/{InjectiveNorm, ProjectiveNorm}): switch NormedSpace instance to projectiveSeminorm Mar 27, 2026
@mathlib-bors mathlib-bors bot closed this Mar 27, 2026
justus-springer pushed a commit to justus-springer/mathlib4 that referenced this pull request Mar 28, 2026
@goliath-klein @pre-commit-ci-lite @justus-springer
refactor(PiTensorProduct/{InjectiveNorm, ProjectiveNorm}): switch Nor…
4577f01 
…medSpace instance to `projectiveSeminorm` (leanprover-community#35568)

The PR switches the `NormedSpace` instance on `PiTensorProduct`s from `injectiveSeminorm` to `projectiveSeminorm` and updates all follow-up results.

The signature of `norm_eval_le_projectiveSeminorm` is changed to match the one of `norm_eval_le_injectiveSeminorm`.

This is the second in a series of three PRs with the goal to [deprecate `PiTensorProuduct.injectiveSeminorm`](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/injectiveSeminorm/with/568798633).

Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@robin-carlier robin-carlier robin-carlier left review comments

Assignees

@robin-carlier robin-carlier

Labels

new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! 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.

3 participants

@goliath-klein @riccardobrasca @robin-carlier