Skip to content

[Merged by Bors] - feat(Analysis/Analytic): lemmas about smul for power series#19816

Closed
vasnesterov wants to merge 12 commits intomasterfrom
vasnesterov/HasFPowerSeriesOnBall_lemmas
Closed

[Merged by Bors] - feat(Analysis/Analytic): lemmas about smul for power series#19816
vasnesterov wants to merge 12 commits intomasterfrom
vasnesterov/HasFPowerSeriesOnBall_lemmas

Conversation

@vasnesterov
Copy link
Copy Markdown
Collaborator

@vasnesterov vasnesterov commented Dec 8, 2024 •
edited
Loading

  • Prove radius_le_smul and radius_smul_eq stating that c • p converges on the same ball as p.
  • Prove HasFPowerSeriesOnBall.const_smul (and variations) stating that scalar multiplication preserves series' convergence on the same ball.
  • Add smul_apply simp-lemma for FormalMultilinearSeries.

Open in Gitpod

@github-actions
Copy link
Copy Markdown

github-actions bot commented Dec 8, 2024 •
edited
Loading

PR summary 5dcef2033f

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ AnalyticAt.const_smul
+ AnalyticWithinAt.const_smul
+ HasFPowerSeriesAt.const_smul
+ HasFPowerSeriesOnBall.const_smul
+ HasFPowerSeriesWithinAt.const_smul
+ HasFPowerSeriesWithinOnBall.const_smul
+ radius_le_smul
+ radius_smul_eq
+ smul_apply

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.

No changes to technical debt.

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 Dec 8, 2024
@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 Dec 10, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 10, 2024
@vasnesterov vasnesterov mentioned this pull request Dec 16, 2024
Closed
2 tasks
sgouezel
sgouezel reviewed Dec 18, 2024
View reviewed changes
@sgouezel sgouezel added the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 18, 2024
sgouezel
sgouezel reviewed Dec 18, 2024
View reviewed changes
@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 Dec 18, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 18, 2024
@vasnesterov vasnesterov removed the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 18, 2024
j-loreaux
j-loreaux reviewed Jan 6, 2025
View reviewed changes
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.

Thanks! Just some minor changes to the proof of radius_le_smul. Please wait for CI to finish before merging.

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jan 6, 2025

✌️ vasnesterov can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@ghost ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jan 6, 2025
@vasnesterov @j-loreaux
Update Mathlib/Analysis/Analytic/Basic.lean
5dcef20 
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
@vasnesterov
Copy link
Copy Markdown
Collaborator Author

vasnesterov commented Jan 6, 2025

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Jan 7, 2025
@vasnesterov
feat(Analysis/Analytic): lemmas about smul for power series (#19816)
9e41cdd 
* Prove `radius_le_smul` and `radius_smul_eq` stating that `c • p` converges on the same ball as `p`.
* Prove `HasFPowerSeriesOnBall.const_smul` (and variations) stating that scalar multiplication preserves series' convergence on the same ball.
* Add `smul_apply` simp-lemma for `FormalMultilinearSeries`.


Co-authored-by: Vasily Nesterov <118051017+vasnesterov@users.noreply.github.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jan 7, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Analysis/Analytic): lemmas about smul for power series [Merged by Bors] - feat(Analysis/Analytic): lemmas about smul for power series Jan 7, 2025
@mathlib-bors mathlib-bors bot closed this Jan 7, 2025
@mathlib-bors mathlib-bors bot deleted the vasnesterov/HasFPowerSeriesOnBall_lemmas branch January 7, 2025 00:55
Julian added a commit that referenced this pull request Jan 8, 2025
@Julian
Merge remote-tracking branch 'origin/master' into emultiplicity-of-nat
53d4c08 
* origin/master: (642 commits)
  feat: the Boolean subalgebra generated by the lattice generated by a set (#20440)
  feat: misc. lemmas about moments, tilted measures (#20150)
  chore(Algebra/Lie): make IsNilpotent and IsSolvable independent of scalars (#20556)
  feat(Combinatorics/SimpleGraph/Path): add `IsPath.getVert_injOn` (#19373)
  feat(Combinatorics/SimpleGraph): add lemmas about `spanningCoe` (#19377)
  chore: scope 'on' notation to Function (#20562)
  chore: disable docPrime linter (#20559)
  chore: deprecate MulRingNorm._ in favour of AbsoluteValue._ (#20557)
  fix(scripts/bench_summary): input jobID as a Nat, rather than a String (#20539)
  chore: move results about `DivisionMonoid` + `HasDistribNeg` (#20551)
  feat(NumberTheory/NumberField/Embeddings): definition of totally real field (#20542)
  chore(Noetherian/Artinian): generalize to Semiring (#20534)
  chore: protect `Filter.nhds_{iInf,inf}` (#20530)
  chore(AlgebraicTopology): move SplitSimplicialObject.lean (#20511)
  chore: extract 3 new files out of MeasureSpace (#20509)
  feat(RingTheory): Jacobian criterion for smoothness of local algebras (#20326)
  doc(RingTheory/Flat): add reference to Lambek's paper (#20266)
  feat(NumberTheory/AbelSummation): add more results (#19942)
  chore(Multilinear/Basic): generalize the `SMul` instance (#20536)
  feat(FDeriv/Equiv): generalize `HasFDerivAt.of_local_left_inverse` (#20516)
  feat(ContDiff): add `iteratedFDeriv_comp` (#20472)
  feat(LowerUpperTopology): add lemmas (#20465)
  feat(ContDiff): weaken some assumptions (#20368)
  fix(scripts/technical-debt-metric): avoid division by 0 (#20537)
  chore(Algebra/Ring): Clean up in SumsOfSquares and Semireal/Defs (#20528)
  feat(FTaylorSeries): add lemmas about `dist` between 0th and 1st derivs (#20089)
  feat: results on inner regularity of finite measures (#19780)
  chore: to_additive various results on groups, group actions (#20547)
  feat(Probability/Kernel): `Kernel.sectL` and `sectR` (#15466)
  chore(CategoryTheory/Limits/Fubini): relax universes constraints and weaken hypotheses (#20553)
  perf: remove `@[simp]` on `Fintype.card_of{IsEmpty,Subsingleton}` (#20524)
  fix(HashCommandLinter): remove unnecessary, broken workaround for tests (#20529)
  chore(Ideal/Basic): dependent generalization of `Ideal.pi` (#20535)
  feat(RingTheory): being unramified is a local property (#20323)
  chore(BooleanSubalgebra): use `IsSublattice` in `closure_sdiff_sup_induction` (#20439)
  feat(Order/SuccPred/CompleteLinearOrder): `⨆ a < x, succ a = x` (#19970)
  chore(*): replace `no_index (ofNat n)` with `ofNat(n)` everywhere (#20521)
  feat(CategoryTheory/Triangulated/Adjunction): the right adjoint of a triangulated functor is triangulated (#20255)
  chore(Order/SuccPred/LinearLocallyFinite): change data-creating instances to defs (#20235)
  chore: don't import algebra in `Data.Finset.Basic` (#19779)
  feat: initial segment commutes with `Iio` (#20503)
  chore(Measure/Pi): move parts to `MeasurableSpace/` (#20215)
  chore: smile more often (#20436)
  chore(Algebra/Category/MonCat/ForgetCorepresentable, Algebra/Group/Equiv/Basic): move definitions and add symmetric version (#20416)
  feat(GroupTheory/QuotientGroup): group correspondence theorem (#20007)
  doc: change "module homomorphism" to "linear map" (#20481)
  perf: improves the performance of the `Repr (Equiv.Perm α)` instance (1/4) (#20519)
  fix: do not keep only the first line of hints (#19756)
  feat(Analysis/Analytic): lemmas about `smul` for power series (#19816)
  chore: don't import algebra in `Data.Multiset.Basic` (#19775)
  ...
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@j-loreaux j-loreaux j-loreaux left review comments

@sgouezel sgouezel sgouezel left review comments

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-analysis Analysis (normed *, calculus)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@vasnesterov @j-loreaux @sgouezel @leanprover-community-bot-assistant