[Merged by Bors] - chore: match the definition of AnalyticWithinAt with ContDiffWithinAt

[sgouezel]

The current definition of AnalyticWithinAt in a set s at a point x requires good behavior inside s, and continuity within s at x (because good behavior at x is important). In ContDiffWithinAt, where the issues are similar, one requires instead good behavior inside insert x s. Those two points of view are equivalent, but the latter is often more convenient (just one field to check, more uniform proofs).

In this PR, we switch the definition of AnalyticWithinAt to the latter approach. We also expand a little bit the API around AnalyticWithinAt, by tweaking theorems that required AnalyticAt to require AnalyticWithinAt, and deduce AnalyticAt versions from AnalyticWithinAt versions. For this, a few statements have to be moved from the file Analytic.Within.lean to Analytic.Basic.lean.

There is no real new statement or new proof in this PR, but it opens the way to further improvements.

---

[github-actions]

PR summary 5b34af5477

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ AnalyticWithinAt.continuousWithinAt_insert
+ HasFPowerSeriesAt.hasFPowerSeriesWithinAt
+ HasFPowerSeriesOnBall.hasFPowerSeriesWithinOnBall
+ HasFPowerSeriesWithinAt.analyticWithinAt
+ HasFPowerSeriesWithinAt.coeff_zero
+ HasFPowerSeriesWithinAt.congr
+ HasFPowerSeriesWithinAt.continuousWithinAt_insert
+ HasFPowerSeriesWithinAt.eventually
+ HasFPowerSeriesWithinAt.isBigO_image_sub_norm_mul_norm_sub
+ HasFPowerSeriesWithinAt.isBigO_sub_partialSum_pow
+ HasFPowerSeriesWithinOnBall.analyticWithinAt
+ HasFPowerSeriesWithinOnBall.coeff_zero
+ HasFPowerSeriesWithinOnBall.congr
+ HasFPowerSeriesWithinOnBall.continuousOn
+ HasFPowerSeriesWithinOnBall.continuousWithinAt
+ HasFPowerSeriesWithinOnBall.continuousWithinAt_insert
+ HasFPowerSeriesWithinOnBall.hasFPowerSeriesWithinAt
+ HasFPowerSeriesWithinOnBall.hasSum_sub
+ HasFPowerSeriesWithinOnBall.image_sub_sub_deriv_le
+ HasFPowerSeriesWithinOnBall.isBigO_image_sub_image_sub_deriv_principal
+ HasFPowerSeriesWithinOnBall.of_le
+ HasFPowerSeriesWithinOnBall.radius_pos
+ HasFPowerSeriesWithinOnBall.tendstoLocallyUniformlyOn
+ HasFPowerSeriesWithinOnBall.tendstoLocallyUniformlyOn'
+ HasFPowerSeriesWithinOnBall.tendstoUniformlyOn
+ HasFPowerSeriesWithinOnBall.tendstoUniformlyOn'
+ HasFPowerSeriesWithinOnBall.uniform_geometric_approx
+ HasFPowerSeriesWithinOnBall.uniform_geometric_approx'
+ MapsTo.insert
+ _
+ analyticWithinAt_iff_exists_analyticAt'

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]

Thanks 🎉

bors merge
Thanks 🎉

bors merge

[mathlib-bors]

Already running a review

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style