Skip to content

feat: define multivariate restricted power series#32692

Open
WilliamCoram wants to merge 22 commits intoleanprover-community:masterfrom
WilliamCoram:MVRestrictedPowerSeries
Open

feat: define multivariate restricted power series#32692
WilliamCoram wants to merge 22 commits intoleanprover-community:masterfrom
WilliamCoram:MVRestrictedPowerSeries

Conversation

@WilliamCoram
Copy link
Copy Markdown
Collaborator

@WilliamCoram WilliamCoram commented Dec 10, 2025

We define multivariate restricted power series over a normed ring R, and show the properties that they form a ring when R has the ultrametric property.

This work generalises my previous work in #26089 which will need to be refactored.

Open in Gitpod

@github-actions github-actions bot added new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-ring-theory Ring theory labels Dec 10, 2025
@WilliamCoram
Copy link
Copy Markdown
Collaborator Author

WilliamCoram commented Dec 10, 2025

re refactoring: I can do this after people think this new set up is acceptable.

@github-actions
Copy link
Copy Markdown

github-actions bot commented Dec 10, 2025 •
edited
Loading

PR summary e7f2949fc6

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.RingTheory.MvPowerSeries.test (new file) 1
Mathlib.RingTheory.MvPowerSeries.Restricted (new file) 1628

Declarations diff

+ IsRestricted
+ Restricted
+ instance [IsUltrametricDist R] (c : σ → ℝ) : Ring (Restricted R c)
+ isAddSubgroup
+ isRestricted.add
+ isRestricted.mul
+ isRestricted.neg
+ isRestricted_C
+ isRestricted_abs_iff
+ isRestricted_monomial
+ isRestricted_one
+ isRestricted_zero
+ isSubring
+ nonempty_antidiagonal
+ tendsto_antidiagonal
+ tendsto_sup'_antidiagonal_cofinite

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.

No changes to technical debt.

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

@WilliamCoram WilliamCoram added the t-number-theory Number theory (also use t-algebra or t-analysis to specialize) label Dec 10, 2025
erdOne
erdOne reviewed Dec 13, 2025
View reviewed changes
Copy link
Copy Markdown
Member

@erdOne erdOne left a comment

Choose a reason for hiding this comment

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

Some golfs

@erdOne erdOne added the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 13, 2025
@WilliamCoram WilliamCoram removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 14, 2026
@WilliamCoram
Copy link
Copy Markdown
Collaborator Author

WilliamCoram commented Jan 14, 2026

Some golfs

Thanks for the cleaning up, most of the proofs look a lot nicer now.

jcommelin
jcommelin reviewed Jan 22, 2026
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks for your PR. I've left some comments. Some of them also apply to similar code below them. Please extrapolate.

@jcommelin jcommelin added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 22, 2026
@WilliamCoram
Copy link
Copy Markdown
Collaborator Author

WilliamCoram commented Jan 23, 2026

Thanks for your PR. I've left some comments. Some of them also apply to similar code below them. Please extrapolate.

Thanks for the review. I think I have found all the suggested changes.

@WilliamCoram WilliamCoram removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 23, 2026
jcommelin
jcommelin reviewed Jan 23, 2026
View reviewed changes
@jcommelin jcommelin added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 23, 2026
@github-actions github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Jan 26, 2026
@github-actions github-actions bot removed the large-import Automatically added label for PRs with a significant increase in transitive imports label Feb 13, 2026
@WilliamCoram WilliamCoram removed awaiting-author A reviewer has asked the author a question or requested changes. labels Mar 9, 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 11, 2026
@mathlib-merge-conflicts
Copy link
Copy Markdown

mathlib-merge-conflicts bot commented Mar 11, 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 11, 2026
erdOne
erdOne reviewed Mar 16, 2026
View reviewed changes
erdOne
erdOne reviewed Mar 16, 2026
View reviewed changes
erdOne
erdOne reviewed Mar 16, 2026
View reviewed changes
Mathlib/RingTheory/MvPowerSeries/Restricted.lean Outdated
Comment on lines +69 to +75
lemma isRestricted.smul (c : σ → ℝ) {f : MvPowerSeries σ R} (hf : IsRestricted c f) (r : R) :
IsRestricted c (r • f) := by
rw [← isRestricted_abs_iff, IsRestricted] at *
refine tendsto_const_nhds.squeeze ((hf.const_mul ‖r‖).trans_eq (by simp)) (fun n ↦ ?_) fun n ↦ ?_
· dsimp [Finsupp.prod]; positivity
simp only [map_smul, smul_eq_mul, Pi.abs_apply, ← mul_assoc]
exact mul_le_mul_of_nonneg_right (norm_mul_le _ _) (by dsimp [Finsupp.prod]; positivity)
Copy link
Copy Markdown
Member

@erdOne erdOne Mar 16, 2026

Choose a reason for hiding this comment

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

Can you generalize this to take (r : S) with Algebra S R and some typeclass about the norm and smul so that nsmul and zsmul are unnecessary?

Copy link
Copy Markdown
Collaborator Author

@WilliamCoram WilliamCoram Mar 18, 2026

Choose a reason for hiding this comment

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

For now I have removed this from the PR, I will have a think about how I could do this.

However, this was initially towards proving they formed a ring - instead I added instances showing they are ring via showing a subring then pushing to its own type. Let me know if this is the idiomatic way to do this, and in the future I can add a more general smul lemma in - if/when I need it.

erdOne
erdOne reviewed Mar 16, 2026
View reviewed changes
Copy link
Copy Markdown
Member

@erdOne erdOne left a comment

Choose a reason for hiding this comment

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

Also can you resolve the comments that you have dealt with already? Thanks.

erdOne
erdOne reviewed Mar 18, 2026
View reviewed changes
Mathlib/Analysis/Normed/Order/Antidiag.lean Outdated
Comment on lines +30 to +46
lemma Finset.nonempty_antidiagonal {M : Type*} [AddMonoid M] [Finset.HasAntidiagonal M] (a : M) :
(Finset.antidiagonal a).Nonempty :=
⟨(0, a), by simp⟩

open Filter Pointwise in
lemma tendsto_sup'_antidiagonal_cofinite
{M R : Type*} [AddMonoid M] [Finset.HasAntidiagonal M] {f : M × M → R}
[LinearOrder R] {F : Filter R} (hf : Tendsto f cofinite F) :
Tendsto (fun a ↦ (Finset.antidiagonal a).sup' (Finset.nonempty_antidiagonal _) f)
cofinite F := by
intro U hU
refine ((((hf hU).image Prod.fst)).add ((hf hU).image Prod.snd)).subset ?_
simp only [Set.subset_def, Set.mem_compl_iff, Set.mem_preimage]
intro x hx
obtain ⟨i, hi, e⟩ := Finset.exists_mem_eq_sup' (Finset.nonempty_antidiagonal x) f
obtain rfl : i.1 + i.2 = x := by simpa using hi
exact Set.add_mem_add (by simpa using ⟨i.2, e ▸ hx⟩) (by simpa using ⟨i.1, e ▸ hx⟩)
Copy link
Copy Markdown
Member

@erdOne erdOne Mar 18, 2026

Choose a reason for hiding this comment

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

I think these two lemmas now belong somewhere else.

Copy link
Copy Markdown
Collaborator Author

@WilliamCoram WilliamCoram Mar 20, 2026

Choose a reason for hiding this comment

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

I have moved these, I think the first is okay to be moved to the file ‎Mathlib/Algebra/Order/Antidiag/Prod.lean‎. However, I do not believe where I placed the second one is correct - I will have a think about it more, but if you have any ideas let me know.

erdOne
erdOne reviewed Mar 18, 2026
View reviewed changes
@github-actions github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Mar 20, 2026
@github-actions github-actions bot removed the large-import Automatically added label for PRs with a significant increase in transitive imports label Mar 31, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin left review comments

@erdOne erdOne erdOne left review comments

Assignees

@alreadydone alreadydone

Labels

new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-number-theory Number theory (also use t-algebra or t-analysis to specialize) t-ring-theory Ring theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@WilliamCoram @jcommelin @erdOne @alreadydone