Skip to content

refactor(PiTensorProduct/{InjectiveNorm, ProjectiveNorm}): deprecate injectiveSeminorm#35569

Open
goliath-klein wants to merge 13 commits intoleanprover-community:masterfrom
goliath-klein:pitp-seminorms-deprecations
Open

refactor(PiTensorProduct/{InjectiveNorm, ProjectiveNorm}): deprecate injectiveSeminorm#35569
goliath-klein wants to merge 13 commits intoleanprover-community:masterfrom
goliath-klein:pitp-seminorms-deprecations

Conversation

@goliath-klein
Copy link
Copy Markdown
Contributor

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

This PR:

  • Deprecates PiTensorProduct.injectiveSeminorm and supporting lemmas.
  • Moves the theory of liftEquiv from InjectiveSeminorm.lean to ProjectiveSeminorm.lean.

No changes are introduced beyond adding deprecation notices, adapting docstrings, and moving material between files.

The PR leaves InjectiveSeminorm.lean almost empty. A new implementation of injectiveSeminorm, one which reflects the common mathematical definition, is to be done.

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

Deprecations:

  • injectiveSeminorm
  • dualSeminorms_bounded
  • injectiveSeminorm_apply
  • norm_eval_le_injectiveSeminorm
  • injectiveSeminorm_le_projectiveSeminorm
  • injectiveSeminorm_tprod_le

Preliminary work toward a reimplementation is at #33969.

I've added Davood and myself to the "Authors" field, as we have now significantly refactored this module.

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 2da3b35b9d

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

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.

Increase in tech debt: (relative, absolute) = (4.00, 0.24)
Current number Change Type
17 4 disabled deprecation lints

Current commit 48ff867ca5
Reference commit 2da3b35b9d

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-merge-conflicts mathlib-merge-conflicts bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 3, 2026
@mathlib-merge-conflicts
Copy link
Copy Markdown

mathlib-merge-conflicts bot commented Mar 3, 2026

This pull request has conflicts, please merge master and resolve them.

@goliath-klein goliath-klein mentioned this pull request Mar 6, 2026
Closed
1 task
@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 27, 2026
@mathlib-dependent-issues
Copy link
Copy Markdown

mathlib-dependent-issues bot commented Mar 27, 2026

This PR/issue depends on:

@github-actions 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 Mar 27, 2026
@mathlib-merge-conflicts mathlib-merge-conflicts bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 29, 2026
@mathlib-merge-conflicts
Copy link
Copy Markdown

mathlib-merge-conflicts bot commented Mar 29, 2026

This pull request has conflicts, please merge master and resolve them.

@github-actions 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 Mar 29, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@goliath-klein