Skip to content

[Merged by Bors] - chore: rename AnalyticOn to AnalyticOnNhd, and AnalyticWithinOn to AnalyticOn#17146

Closed
sgouezel wants to merge 17 commits intomasterfrom
SG_analyticOn
Closed

[Merged by Bors] - chore: rename AnalyticOn to AnalyticOnNhd, and AnalyticWithinOn to AnalyticOn#17146
sgouezel wants to merge 17 commits intomasterfrom
SG_analyticOn

Conversation

@sgouezel
Copy link
Copy Markdown
Contributor

@sgouezel sgouezel commented Sep 26, 2024 •
edited
Loading

For coherence with ContinuousOn, DifferentiableOn and so on. See Zulip https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/Integrate.20analytic.20functions.20in.20the.20smooth.20hierarchy/near/471899268

This is 90% renaming all AnalyticOn to AnalyticOnNhd and then AnalyticWithinOn to AnalyticOn, and then adding deprecations. The 10% remaining is, when adding a deprecation alias AnalyticOn.foo := AnalyticOnNhd.foo, I noticed that AnalyticOn.foo would definitely make sense (with the new meaning of AnalyticOn), so I added the lemma with the new meaning instead of deprecating the old one.

Open in Gitpod

@sgouezel sgouezel added the WIP Work in progress label Sep 26, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Sep 26, 2024 •
edited
Loading

PR summary 94aa5324e7

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ AnalyticAt.exists_ball_analyticOnNhd
+ AnalyticAt.exists_mem_nhds_analyticOnNhd
+ AnalyticOnNhd
+ AnalyticOnNhd.add
+ AnalyticOnNhd.aeval_mvPolynomial
+ AnalyticOnNhd.aeval_polynomial
+ AnalyticOnNhd.along_fst
+ AnalyticOnNhd.along_snd
+ AnalyticOnNhd.analyticOn
+ AnalyticOnNhd.cexp
+ AnalyticOnNhd.clog
+ AnalyticOnNhd.comp
+ AnalyticOnNhd.comp'
+ AnalyticOnNhd.comp_analyticOn
+ AnalyticOnNhd.comp₂
+ AnalyticOnNhd.congr
+ AnalyticOnNhd.congr'
+ AnalyticOnNhd.contDiffOn
+ AnalyticOnNhd.continuous
+ AnalyticOnNhd.continuousOn
+ AnalyticOnNhd.cpow
+ AnalyticOnNhd.curry_left
+ AnalyticOnNhd.curry_right
+ AnalyticOnNhd.deriv
+ AnalyticOnNhd.differentiableOn
+ AnalyticOnNhd.div
+ AnalyticOnNhd.eval_continuousLinearMap
+ AnalyticOnNhd.eval_continuousLinearMap'
+ AnalyticOnNhd.eval_linearMap
+ AnalyticOnNhd.eval_linearMap'
+ AnalyticOnNhd.eval_mvPolynomial
+ AnalyticOnNhd.eval_polynomial
+ AnalyticOnNhd.fderiv
+ AnalyticOnNhd.inv
+ AnalyticOnNhd.is_constant_or_isOpen
+ AnalyticOnNhd.iteratedFDeriv
+ AnalyticOnNhd.iterated_deriv
+ AnalyticOnNhd.meromorphicOn
+ AnalyticOnNhd.mono
+ AnalyticOnNhd.mul
+ AnalyticOnNhd.neg
+ AnalyticOnNhd.pi
+ AnalyticOnNhd.pow
+ AnalyticOnNhd.prod
+ AnalyticOnNhd.smul
+ AnalyticOnNhd.sub
+ AnalyticWithinAt.aeval_polynomial
+ AnalyticWithinAt.cexp
+ AnalyticWithinAt.clog
+ AnalyticWithinAt.congr_of_eventuallyEq_insert
+ AnalyticWithinAt.cpow
+ CPolynomialAt.analyticWithinAt
+ CPolynomialOn.analyticOnNhd
+ ContinuousLinearMap.comp_analyticOnNhd
+ Finset.analyticOnNhd_prod
+ Finset.analyticOnNhd_sum
+ HasFPowerSeriesOnBall.analyticOnNhd
+ IsOpen.analyticOn_iff_analyticOnNhd
+ LSeries_analyticOnNhd
+ _root_.AnalyticOn.eq_of_frequently_eq
+ _root_.DifferentiableOn.analyticOnNhd
+ analyticOnNhd_bilinear
+ analyticOnNhd_cexp
+ analyticOnNhd_congr
+ analyticOnNhd_congr'
+ analyticOnNhd_const
+ analyticOnNhd_fst
+ analyticOnNhd_id
+ analyticOnNhd_iff_differentiableOn
+ analyticOnNhd_inv
+ analyticOnNhd_pi_iff
+ analyticOnNhd_snd
+ analyticOnNhd_uncurry_of_multilinear
+ analyticOnNhd_univ_iff_differentiable
+ analyticOn_of_locally_analyticOn
+ analyticOn_univ
+ analyticWithinAt_bilinear
++++ analyticOnNhd
++++---- analyticWithinOn
+--+++-- analyticOn

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.

@jcommelin
Copy link
Copy Markdown
Member

jcommelin commented Sep 26, 2024

The individual commits look great! Thanks

bors merge

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Sep 26, 2024

👎 Rejected by label

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Sep 26, 2024
@sgouezel sgouezel removed the WIP Work in progress label Sep 26, 2024
@sgouezel
Copy link
Copy Markdown
Contributor Author

sgouezel commented Sep 26, 2024

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Sep 26, 2024
@sgouezel
chore: rename AnalyticOn to AnalyticOnNhd, and AnalyticWithinOn…
5d4532a 
… to `AnalyticOn` (#17146)

For coherence with `ContinuousOn`, `DifferentiableOn` and so on. See Zulip https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/Integrate.20analytic.20functions.20in.20the.20smooth.20hierarchy/near/471899268

This is 90% renaming all `AnalyticOn` to `AnalyticOnNhd` and then `AnalyticWithinOn` to `AnalyticOn`, and then adding deprecations. The 10% remaining is, when adding a deprecation `alias AnalyticOn.foo := AnalyticOnNhd.foo`, I noticed that `AnalyticOn.foo` would definitely make sense (with the new meaning of `AnalyticOn`), so I added the lemma with the new meaning instead of deprecating the old one.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Sep 26, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: rename AnalyticOn to AnalyticOnNhd, and AnalyticWithinOn to AnalyticOn [Merged by Bors] - chore: rename AnalyticOn to AnalyticOnNhd, and AnalyticWithinOn to AnalyticOn Sep 26, 2024
@mathlib-bors mathlib-bors bot closed this Sep 26, 2024
@mathlib-bors mathlib-bors bot deleted the SG_analyticOn branch September 26, 2024 10:28
fbarroero pushed a commit that referenced this pull request Oct 2, 2024
@sgouezel @fbarroero
chore: rename AnalyticOn to AnalyticOnNhd, and AnalyticWithinOn…
7587a22 
… to `AnalyticOn` (#17146)

For coherence with `ContinuousOn`, `DifferentiableOn` and so on. See Zulip https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/Integrate.20analytic.20functions.20in.20the.20smooth.20hierarchy/near/471899268

This is 90% renaming all `AnalyticOn` to `AnalyticOnNhd` and then `AnalyticWithinOn` to `AnalyticOn`, and then adding deprecations. The 10% remaining is, when adding a deprecation `alias AnalyticOn.foo := AnalyticOnNhd.foo`, I noticed that `AnalyticOn.foo` would definitely make sense (with the new meaning of `AnalyticOn`), so I added the lemma with the new meaning instead of deprecating the old one.
@sgouezel sgouezel mentioned this pull request Nov 27, 2024
Closed
22 tasks
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

ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@sgouezel @jcommelin