feat(Analysis/Analytic): add AnalyticAt properties for iterated dslope

[e-271828]

This PR adds three fundamental lemmas in the AnalyticAt namespace to establish the analyticity of the (iterated) dslope function:

• AnalyticAt.dslope_of_ne
• AnalyticAt.iterate_dslope_of_ne
• AnalyticAt.iterate_dslope (at the singularity, using has_fpower_series_iterate_dslope_fslope)

These properties are crucial for factoring out removable singularities iteratively while preserving analyticity.
This PR was assisted by LLMs (Aristotle and Gemini).

---

[github-actions]

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

[github-actions]

PR summary df818bb9eb

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ AnalyticAt.dslope
+ AnalyticAt.dslope_of_ne
+ AnalyticAt.iterate_dslope

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

[wwylele]

You can combine AnalyticAt.iterate_dslope_of_ne and AnalyticAt.iterate_dslope into one theorem without condition on s

theorem AnalyticAt.iterate_dslope' {f : 𝕜 → E} {z₀ s : 𝕜} (hf : AnalyticAt 𝕜 f s) (n : ℕ) :
    AnalyticAt 𝕜 ((Function.swap dslope z₀)^[n] f) s := by
  by_cases hs : s = z₀
  · simp_rw [← hs]
    exact hf.iterate_dslope n
  exact hf.iterate_dslope_of_ne hs n

This is just to demonstrate that this is true, and you can rename this to the new AnalyticAt.iterate_dslope. You can either inline the existing code, or keep them as-is and mark them private. Similarly, there should also be a publuc AnalyticAt.dslope without (hs : s ≠ z₀), and you can make AnalyticAt.dslope_of_ne private

[e-271828]

You can combine AnalyticAt.iterate_dslope_of_ne and AnalyticAt.iterate_dslope into one theorem without condition on s

theorem AnalyticAt.iterate_dslope' {f : 𝕜 → E} {z₀ s : 𝕜} (hf : AnalyticAt 𝕜 f s) (n : ℕ) :
    AnalyticAt 𝕜 ((Function.swap dslope z₀)^[n] f) s := by
  by_cases hs : s = z₀
  · simp_rw [← hs]
    exact hf.iterate_dslope n
  exact hf.iterate_dslope_of_ne hs n

This is just to demonstrate that this is true, and you can rename this to the new AnalyticAt.iterate_dslope. You can either inline the existing code, or keep them as-is and mark them private. Similarly, there should also be a publuc AnalyticAt.dslope without (hs : s ≠ z₀), and you can make AnalyticAt.dslope_of_ne private

@wwylele
Thank you so much for the review and the excellent suggestion!

I completely agree that combining them without the condition on s makes the API much cleaner and easier to use.
I have followed your advice, updated the theorems (including the visibility changes you suggested), and already pushed the new commits.

I really appreciate your guidance!