Skip to content

feat: split continuous linear maps#23186

Closed
grunweg wants to merge 15 commits intomasterfrom
MR-continuouslinearmap-split
Closed

feat: split continuous linear maps#23186
grunweg wants to merge 15 commits intomasterfrom
MR-continuouslinearmap-split

Conversation

@grunweg
Copy link
Copy Markdown
Contributor

@grunweg grunweg commented Mar 21, 2025 •
edited
Loading

We define split linear maps and prove their basic properties.

There are two sorries left. One is ClosedComplemented.prod; the other relates to the composition of split maps. Help with both is welcome.

This zulip discussion contains a proof of the non-trivial sorry.

Open in Gitpod

@grunweg grunweg added the help-wanted The author needs attention to resolve issues label Mar 21, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 21, 2025 •
edited
Loading

PR summary c785c9ed17

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Analysis.NormedSpace.HahnBanach.Splits (new file) 1845

Declarations diff

+ ContinuousLinearMap.Splits
+ Submodule.sum_assoc
+ _root_.ContinuousLinearEquiv.splits
+ _root_.Submodule.map_add
+ antilipschitzConstant
+ antilipschitzWith
+ antilipschitz_aux
+ closedComplemented
+ comp
+ compCLE_left
+ compCLE_right
+ complement
+ complement_isClosed
+ complement_isCompl
+ disjoint_aux
+ injective
+ isClosedMap
+ isClosed_range
+ of_injective_of_finiteDimensional
+ of_injective_of_finiteDimensional_of_completeSpace
+ prodMap
+ range_prodMap

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.

Increase in tech debt: (relative, absolute) = (1.00, 0.00)
Current number Change Type
967 1 erw

Current commit c785c9ed17
Reference commit d3fb08bfb2

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

@github-actions github-actions bot added the t-analysis Analysis (normed *, calculus) label Mar 21, 2025
@grunweg grunweg added WIP Work in progress and removed help-wanted The author needs attention to resolve issues labels Mar 21, 2025
@grunweg grunweg mentioned this pull request Mar 22, 2025
Open
7 tasks
@grunweg grunweg added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 22, 2025
@mathlib4-dependent-issues-bot mathlib4-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 22, 2025
@grunweg grunweg added the help-wanted The author needs attention to resolve issues label Apr 10, 2025
grunweg added a commit that referenced this pull request Apr 10, 2025
@grunweg
chore: manually copy changes made in #23186
aaebea0
@grunweg grunweg mentioned this pull request Jun 19, 2025
Closed
@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented Jun 19, 2025

Closing in favour of #26174.

@grunweg grunweg closed this Jun 19, 2025
@YaelDillies YaelDillies deleted the MR-continuouslinearmap-split branch August 15, 2025 16:45
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

help-wanted The author needs attention to resolve issues t-analysis Analysis (normed *, calculus) WIP Work in progress

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@grunweg @mathlib4-dependent-issues-bot