Skip to content

[Merged by Bors] - refactor(PiTensorProduct/{InjectiveNorm, ProjectiveNorm}): Golfs#35567

Closed
goliath-klein wants to merge 5 commits intoleanprover-community:masterfrom
goliath-klein:pit-tp-seminorms-golfs
Closed

[Merged by Bors] - refactor(PiTensorProduct/{InjectiveNorm, ProjectiveNorm}): Golfs#35567
goliath-klein wants to merge 5 commits intoleanprover-community:masterfrom
goliath-klein:pit-tp-seminorms-golfs

Conversation

@goliath-klein
Copy link
Copy Markdown
Contributor

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

This PR cleans up the proofs in

Analysis/Normed/Module/PiTensorProduct/{InjectiveSeminorm.lean, ProjectiveSeminorm.lean}

In addition, it performs the following minor structural changes:

  • Weaken assumptions from NontriviallyNormedField 𝕜 to NormedField 𝕜 where possible
  • The proofs showing that projectiveSeminorm actually defines a Seminorm are split off into separate lemmas. This mimics the idiom used e.g. in Analysis.Normed.Modula.Operator.Basic to define the operator norm.
  • Register a Nonempty x.lifts instance in PiTensorProduct.lean, to avoid creating a half-dozen local instances.

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

Co-authored-by: Davood H. T. 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.

@github-actions
Copy link
Copy Markdown

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

PR summary d6f48e471c

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ instance (x : ⨂[R] i, s i) : Nonempty ↑x.lifts := nonempty_subtype.mpr (nonempty_lifts x)
+ projectiveSeminormFun
+ projectiveSeminorm_add_le
+ projectiveSeminorm_smul_le
+ projectiveSeminorm_zero

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

This was referenced Feb 20, 2026
Closed
Open
@goliath-klein goliath-klein mentioned this pull request Feb 20, 2026
Closed
@tb65536
Copy link
Copy Markdown
Contributor

tb65536 commented Feb 20, 2026

!radar

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Feb 20, 2026 •
edited
Loading

Benchmark results for f4bf901 against d6f48e4 are in! @goliath-klein @tb65536

  • ✅ build//instructions: -28.1G (-0.02%)

Small changes (1✅)

  • ✅ build/module/Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm//instructions: -16.5G (-48.77%) (reduced significance based on *//lines)

@tb65536
Copy link
Copy Markdown
Contributor

tb65536 commented Feb 20, 2026

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Feb 20, 2026

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

@mathlib-triage mathlib-triage bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Feb 20, 2026
@jsm28 jsm28 removed their assignment Feb 25, 2026
riccardobrasca
riccardobrasca reviewed Mar 6, 2026
View reviewed changes
Copy link
Copy Markdown
Member

@riccardobrasca riccardobrasca 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

@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 6, 2026
mathlib-bors bot pushed a commit that referenced this pull request Mar 6, 2026
@goliath-klein
refactor(PiTensorProduct/{InjectiveNorm, ProjectiveNorm}): Golfs (#35567
ab0ddc2 
)

This PR cleans up the proofs in

Analysis/Normed/Module/PiTensorProduct/{InjectiveSeminorm.lean, ProjectiveSeminorm.lean}

In addition, it performs the following minor structural changes:
* Weaken assumptions from `NontriviallyNormedField 𝕜` to `NormedField 𝕜` where possible
* The proofs showing that `projectiveSeminorm` actually defines a `Seminorm` are split off into separate lemmas. This mimics the idiom used e.g. in `Analysis.Normed.Modula.Operator.Basic` to define the operator norm. 
* Register a `Nonempty x.lifts` instance in PiTensorProduct.lean, to avoid creating a half-dozen local instances.

This is the first 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).
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 6, 2026

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title refactor(PiTensorProduct/{InjectiveNorm, ProjectiveNorm}): Golfs [Merged by Bors] - refactor(PiTensorProduct/{InjectiveNorm, ProjectiveNorm}): Golfs Mar 6, 2026
@mathlib-bors mathlib-bors bot closed this Mar 6, 2026
xroblot pushed a commit to xroblot/mathlib4 that referenced this pull request Mar 9, 2026
@goliath-klein @xroblot
refactor(PiTensorProduct/{InjectiveNorm, ProjectiveNorm}): Golfs (lea…
ac0656e 
…nprover-community#35567)

This PR cleans up the proofs in

Analysis/Normed/Module/PiTensorProduct/{InjectiveSeminorm.lean, ProjectiveSeminorm.lean}

In addition, it performs the following minor structural changes:
* Weaken assumptions from `NontriviallyNormedField 𝕜` to `NormedField 𝕜` where possible
* The proofs showing that `projectiveSeminorm` actually defines a `Seminorm` are split off into separate lemmas. This mimics the idiom used e.g. in `Analysis.Normed.Modula.Operator.Basic` to define the operator norm. 
* Register a `Nonempty x.lifts` instance in PiTensorProduct.lean, to avoid creating a half-dozen local instances.

This is the first 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).
seewoo5 pushed a commit to seewoo5/mathlib4 that referenced this pull request Mar 9, 2026
@goliath-klein @seewoo5
refactor(PiTensorProduct/{InjectiveNorm, ProjectiveNorm}): Golfs (lea…
1d916bc 
…nprover-community#35567)

This PR cleans up the proofs in

Analysis/Normed/Module/PiTensorProduct/{InjectiveSeminorm.lean, ProjectiveSeminorm.lean}

In addition, it performs the following minor structural changes:
* Weaken assumptions from `NontriviallyNormedField 𝕜` to `NormedField 𝕜` where possible
* The proofs showing that `projectiveSeminorm` actually defines a `Seminorm` are split off into separate lemmas. This mimics the idiom used e.g. in `Analysis.Normed.Modula.Operator.Basic` to define the operator norm. 
* Register a `Nonempty x.lifts` instance in PiTensorProduct.lean, to avoid creating a half-dozen local instances.

This is the first 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).
xroblot pushed a commit to xroblot/mathlib4 that referenced this pull request Mar 10, 2026
@goliath-klein @xroblot
refactor(PiTensorProduct/{InjectiveNorm, ProjectiveNorm}): Golfs (lea…
59f40eb 
…nprover-community#35567)

This PR cleans up the proofs in

Analysis/Normed/Module/PiTensorProduct/{InjectiveSeminorm.lean, ProjectiveSeminorm.lean}

In addition, it performs the following minor structural changes:
* Weaken assumptions from `NontriviallyNormedField 𝕜` to `NormedField 𝕜` where possible
* The proofs showing that `projectiveSeminorm` actually defines a `Seminorm` are split off into separate lemmas. This mimics the idiom used e.g. in `Analysis.Normed.Modula.Operator.Basic` to define the operator norm. 
* Register a `Nonempty x.lifts` instance in PiTensorProduct.lean, to avoid creating a half-dozen local instances.

This is the first 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).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@riccardobrasca riccardobrasca riccardobrasca left review comments

@tb65536 tb65536 tb65536 approved these changes

Assignees

@sgouezel sgouezel

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.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

6 participants

@goliath-klein @tb65536 @leanprover-radar @riccardobrasca @jsm28 @sgouezel