feat(Analysis/Analytic): add AnalyticAt properties for iterated dslope#37926
feat(Analysis/Analytic): add AnalyticAt properties for iterated dslope#37926e-271828 wants to merge 3 commits intoleanprover-community:masterfrom
Conversation
github-actions
Bot
added
the
new-contributor
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 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. |
PR summary df818bb9ebImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
|
You can combine This is just to demonstrate that this is true, and you can rename this to the new |
… Function.Iterate.rec Apply an elegant simplification suggested by @wwylele. Co-authored-by: Weiyi Wang <wwylele@gmail.com>
@wwylele I completely agree that combining them without the condition on I really appreciate your guidance! |
| private lemma AnalyticAt.dslope_of_ne {f : 𝕜 → E} {z₀ s : 𝕜} (hf : AnalyticAt 𝕜 f s) | ||
| (hs : s ≠ z₀) : AnalyticAt 𝕜 (_root_.dslope f z₀) s := by | ||
| have h_inv : AnalyticAt 𝕜 (fun z => (z - z₀)⁻¹) s := | ||
| (analyticAt_id.sub analyticAt_const).inv (sub_ne_zero.mpr hs) | ||
| have h_quot : AnalyticAt 𝕜 (fun z => (z - z₀)⁻¹ • (f z - f z₀)) s := | ||
| h_inv.smul (hf.sub analyticAt_const) | ||
| have h_eq : (fun z => (z - z₀)⁻¹ • (f z - f z₀)) =ᶠ[𝓝 s] _root_.dslope f z₀ := by | ||
| filter_upwards [isOpen_ne.mem_nhds hs] with z hz | ||
| exact (_root_.dslope_of_ne f hz).symm | ||
| exact h_quot.congr h_eq | ||
|
|
||
| /-- If `f` is analytic at `s`, then `dslope f z₀` is analytic at `s`. -/ | ||
| lemma AnalyticAt.dslope {f : 𝕜 → E} {z₀ s : 𝕜} (hf : AnalyticAt 𝕜 f s) : | ||
| AnalyticAt 𝕜 (_root_.dslope f z₀) s := by | ||
| by_cases hs : s = z₀ | ||
| · subst hs | ||
| obtain ⟨p, hp⟩ := hf | ||
| exact ⟨_, hp.has_fpower_series_dslope_fslope⟩ | ||
| · exact hf.dslope_of_ne hs |
There was a problem hiding this comment.
The first lemma is trivial if you use fun_prop, and there's no reason to have the private lemma which is immediately superseded. So you just inline the proof into the second lemma, like so:
| private lemma AnalyticAt.dslope_of_ne {f : 𝕜 → E} {z₀ s : 𝕜} (hf : AnalyticAt 𝕜 f s) | |
| (hs : s ≠ z₀) : AnalyticAt 𝕜 (_root_.dslope f z₀) s := by | |
| have h_inv : AnalyticAt 𝕜 (fun z => (z - z₀)⁻¹) s := | |
| (analyticAt_id.sub analyticAt_const).inv (sub_ne_zero.mpr hs) | |
| have h_quot : AnalyticAt 𝕜 (fun z => (z - z₀)⁻¹ • (f z - f z₀)) s := | |
| h_inv.smul (hf.sub analyticAt_const) | |
| have h_eq : (fun z => (z - z₀)⁻¹ • (f z - f z₀)) =ᶠ[𝓝 s] _root_.dslope f z₀ := by | |
| filter_upwards [isOpen_ne.mem_nhds hs] with z hz | |
| exact (_root_.dslope_of_ne f hz).symm | |
| exact h_quot.congr h_eq | |
| /-- If `f` is analytic at `s`, then `dslope f z₀` is analytic at `s`. -/ | |
| lemma AnalyticAt.dslope {f : 𝕜 → E} {z₀ s : 𝕜} (hf : AnalyticAt 𝕜 f s) : | |
| AnalyticAt 𝕜 (_root_.dslope f z₀) s := by | |
| by_cases hs : s = z₀ | |
| · subst hs | |
| obtain ⟨p, hp⟩ := hf | |
| exact ⟨_, hp.has_fpower_series_dslope_fslope⟩ | |
| · exact hf.dslope_of_ne hs | |
| /-- If `f` is analytic at `s`, then `dslope f z₀` is analytic at `s`. -/ | |
| protected lemma AnalyticAt.dslope {f : 𝕜 → E} {z₀ s : 𝕜} (hf : AnalyticAt 𝕜 f s) : | |
| AnalyticAt 𝕜 (dslope f z₀) s := by | |
| obtain (rfl | hs) := eq_or_ne s z₀ | |
| · obtain ⟨p, hp⟩ := hf | |
| exact ⟨_, hp.has_fpower_series_dslope_fslope⟩ | |
| · apply AnalyticAt.congr (f := fun z => (z - z₀)⁻¹ • (f z - f z₀)) (by fun_prop (disch := grind)) | |
| filter_upwards [isOpen_ne.mem_nhds hs] with z hz using (dslope_of_ne f hz).symm |
Also note that we protect the lemma to avoid naming clashes with dslope.
| /-- If `f` is analytic at `s`, then the `n`-th iterated `dslope` of `f` at `z₀` | ||
| is analytic at `s`. -/ | ||
| lemma AnalyticAt.iterate_dslope {f : 𝕜 → E} {z₀ s : 𝕜} (hf : AnalyticAt 𝕜 f s) (n : ℕ) : | ||
| AnalyticAt 𝕜 ((Function.swap _root_.dslope z₀)^[n] f) s := |
There was a problem hiding this comment.
| AnalyticAt 𝕜 ((Function.swap _root_.dslope z₀)^[n] f) s := | |
| AnalyticAt 𝕜 ((Function.swap dslope z₀)^[n] f) s := |
j-loreaux
added
the
awaiting-author
3 participants
This PR adds three fundamental lemmas in the
AnalyticAtnamespace to establish the analyticity of the (iterated)dslopefunction:AnalyticAt.dslope_of_neAnalyticAt.iterate_dslope_of_neAnalyticAt.iterate_dslope(at the singularity, usinghas_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).