Skip to content

feat(Analysis): radius of convergence for FormalMultilinearSeries.compContinuousLinearMap#22531

Closed
vasnesterov wants to merge 9 commits intomasterfrom
vasnesterov/compContinuousLinearMap
Closed

feat(Analysis): radius of convergence for FormalMultilinearSeries.compContinuousLinearMap#22531
vasnesterov wants to merge 9 commits intomasterfrom
vasnesterov/compContinuousLinearMap

Conversation

@vasnesterov
Copy link
Copy Markdown
Collaborator

  • Add basic lemmas compContinuousLinearMap_id and compContinuousLinearMap_comp.
  • Prove lower and upper bounds for the convergence radius of f.compContinuousLinearMap.
  • Prove radius_compNeg: the convergence radii of f(x) and f(-x) are equal.

Open in Gitpod

@github-actions github-actions bot added the t-analysis Analysis (normed *, calculus) label Mar 4, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 4, 2025

PR summary 50da38824a

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/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
1556 1 porting notes

Current commit 50da38824a
Reference commit 42e558f91a

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

@grunweg grunweg changed the title feat(Analysis): Radius of convergence for FormalMultilinearSeries.compContinuousLinearMap feat(Analysis): fadius of convergence for FormalMultilinearSeries.compContinuousLinearMap Mar 4, 2025
@grunweg grunweg changed the title feat(Analysis): fadius of convergence for FormalMultilinearSeries.compContinuousLinearMap feat(Analysis): radius of convergence for FormalMultilinearSeries.compContinuousLinearMap Mar 4, 2025
@leanprover-community-bot-assistant leanprover-community-bot-assistant 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 10, 2025
@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 11, 2025
@leanprover-community-bot-assistant leanprover-community-bot-assistant 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 13, 2025
@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 13, 2025
Copy link
Copy Markdown
Contributor

@j-loreaux j-loreaux left a comment

Choose a reason for hiding this comment

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

sorry, out of time for review now, but here are some things to get you started.

@j-loreaux j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes. label May 8, 2025
@vasnesterov vasnesterov removed the awaiting-author A reviewer has asked the author a question or requested changes. label May 10, 2025
Copy link
Copy Markdown
Contributor

@j-loreaux j-loreaux left a comment

Choose a reason for hiding this comment

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

@vasnesterov I'm sorry it took me so long to come back to this. I needed a decent chunk of time to sit and think about how to simplify things a bit. Sorry that this is less guided learning for you and is instead just a bunch of code, but hopefully you can still glean something from it.

@vasnesterov
Copy link
Copy Markdown
Collaborator Author

This PR has been migrated to a fork-based workflow: #26255

@YaelDillies YaelDillies deleted the vasnesterov/compContinuousLinearMap branch August 18, 2025 07:25
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

awaiting-author A reviewer has asked the author a question or requested changes. migrated-to-fork t-analysis Analysis (normed *, calculus)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants