Skip to content

refactor(LocallyConvex,Topology): split WeakDual/WeakSpace and rename WeakBilin#37027

Open
mike1729 wants to merge 7 commits intoleanprover-community:masterfrom
mike1729:weakbilin-rename
Open

refactor(LocallyConvex,Topology): split WeakDual/WeakSpace and rename WeakBilin#37027
mike1729 wants to merge 7 commits intoleanprover-community:masterfrom
mike1729:weakbilin-rename

Conversation

@mike1729
Copy link
Copy Markdown
Contributor

@mike1729 mike1729 commented Mar 23, 2026 •
edited by j-loreaux
Loading

Reorganize the weak topology files for cleaner dependencies:

  1. Rename Analysis.LocallyConvex.WeakDual → Analysis.LocallyConvex.WeakBilin:
    This file contains only general WeakBilin infrastructure (LinearMap.toSeminormFamily,
    weakBilin_withSeminorms, WeakBilin.locallyConvexSpace, etc.) with no reference to
    WeakDual. The name now reflects the content.

  2. Split Topology.Algebra.Module.WeakDual into WeakDual and WeakSpace:
    The WeakSpace type, its instances, and toWeakSpace/toWeakSpaceCLM move to a new
    Topology.Algebra.Module.WeakSpace. This allows downstream files about weak spaces
    to avoid depending on WeakDual.

  3. Add WeakSpace.seminormFamily and WeakSpace.withSeminorms to
    Analysis.LocallyConvex.WeakSpace: The weak topology on WeakSpace 𝕜 E is generated
    by the seminorm family fun f x ↦ ‖f x‖ indexed by StrongDual 𝕜 E, via the general
    LinearMap.weakBilin_withSeminorms applied to the flipped topDualPairing.

Moves:

  • Mathlib.Analysis.LocallyConvex.WeakDual -> Mathlib.Analysis.LocallyConvex.WeakBilin
  • WeakSpace -> Mathlib.Topology.Algebra.Module.WeakSpace
  • toWeakSpace -> Mathlib.Topology.Algebra.Module.WeakSpace
  • toWeakSpaceCLM -> Mathlib.Topology.Algebra.Module.WeakSpace

CC @j-loreaux

@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 Mar 23, 2026
@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 23, 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. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

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. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

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 Mar 23, 2026 •
edited
Loading

PR summary 6cad1b0fcc

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Analysis.LocallyConvex.WeakDual -1805
Mathlib.Analysis.LocallyConvex.WeakSpace Mathlib.Analysis.Normed.Module.DoubleDual 1
Mathlib.Topology.Algebra.Module.WeakSpace (new file) 1210
Mathlib.Analysis.LocallyConvex.WeakBilin 1805

Declarations diff

+ seminormFamily
+ seminormFamily_apply
+ withSeminorms

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) = (3.00, 0.00)
Current number Change Type
7426 3 backward.isDefEq

Current commit 9c598f700d
Reference commit 6cad1b0fcc

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

note: file Mathlib/Analysis/LocallyConvex/WeakDual.lean` was renamed to `Mathlib/Analysis/LocallyConvex/WeakBilin.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

@github-actions github-actions bot added the file-removed A Lean module was (re)moved without a `deprecated_module` annotation label Mar 23, 2026
@mike1729 mike1729 mentioned this pull request Mar 23, 2026
Closed
3 tasks
@mike1729 mike1729 mentioned this pull request Mar 23, 2026
Closed
@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 25, 2026
@mathlib-merge-conflicts
Copy link
Copy Markdown

mathlib-merge-conflicts bot commented Mar 25, 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 25, 2026
@mike1729 mike1729 mentioned this pull request Mar 25, 2026
Draft
1 task
@mike1729
Merge remote-tracking branch 'upstream/master' into weakbilin-rename
9c598f7 
# Conflicts:
#	Mathlib/Analysis/LocallyConvex/WeakSpace.lean
@j-loreaux
Copy link
Copy Markdown
Contributor

j-loreaux commented Mar 31, 2026

I'm going to make this wait for #37314 as they will conflict.

@j-loreaux j-loreaux added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 31, 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 Apr 3, 2026
@mathlib-dependent-issues
Copy link
Copy Markdown

mathlib-dependent-issues bot commented Apr 3, 2026

This PR/issue depends on:

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

file-removed A Lean module was (re)moved without a `deprecated_module` annotation 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.

2 participants

@mike1729 @j-loreaux