-
Notifications
You must be signed in to change notification settings - Fork 234
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat(Analysis/Analytic): define meromorphic functions (#9590)
This patch defines `MeromorphicAt`, for functions on nontrivially normed fields, and prove it is preserved by sums and products (routine) and inverses (much less trivial). Along the way, we define "order of vanishing" for a function analytic at a point (as an `ENat`).
- Loading branch information
Showing
3 changed files
with
196 additions
and
2 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,125 @@ | ||
| /- | ||
| Copyright (c) 2024 David Loeffler. All rights reserved. | ||
| Released under Apache 2.0 license as described in the file LICENSE. | ||
| Authors: David Loeffler | ||
| -/ | ||
| import Mathlib.Analysis.Analytic.IsolatedZeros | ||
|
|
||
| /-! | ||
| # Meromorphic functions | ||
| -/ | ||
|
|
||
| open scoped Topology | ||
|
|
||
| variable {π : Type*} [NontriviallyNormedField π] | ||
| {E : Type*} [NormedAddCommGroup E] [NormedSpace π E] | ||
|
|
||
| /-- Meromorphy of `f` at `x` (more precisely, on a punctured neighbourhood of `x`; the value at | ||
| `x` itself is irrelevant). -/ | ||
| def MeromorphicAt (f : π β E) (x : π) := | ||
| β (n : β), AnalyticAt π (fun z β¦ (z - x) ^ n β’ f z) x | ||
|
|
||
| lemma AnalyticAt.meromorphicAt {f : π β E} {x : π} (hf : AnalyticAt π f x) : | ||
| MeromorphicAt f x := | ||
| β¨0, by simpa only [pow_zero, one_smul]β© | ||
|
|
||
| lemma meromorphicAt_id (x : π) : MeromorphicAt id x := (analyticAt_id π x).meromorphicAt | ||
|
|
||
| lemma meromorphicAt_const (e : E) (x : π) : MeromorphicAt (fun _ β¦ e) x := | ||
| analyticAt_const.meromorphicAt | ||
|
|
||
| namespace MeromorphicAt | ||
|
|
||
| lemma add {f g : π β E} {x : π} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) : | ||
| MeromorphicAt (f + g) x := by | ||
| rcases hf with β¨m, hfβ© | ||
| rcases hg with β¨n, hgβ© | ||
| refine β¨max m n, ?_β© | ||
| have : (fun z β¦ (z - x) ^ max m n β’ (f + g) z) = fun z β¦ (z - x) ^ (max m n - m) β’ | ||
| ((z - x) ^ m β’ f z) + (z - x) ^ (max m n - n) β’ ((z - x) ^ n β’ g z) | ||
| Β· simp_rw [β mul_smul, β pow_add, Nat.sub_add_cancel (Nat.le_max_left _ _), | ||
| Nat.sub_add_cancel (Nat.le_max_right _ _), Pi.add_apply, smul_add] | ||
| rw [this] | ||
| exact ((((analyticAt_id π x).sub analyticAt_const).pow _).smul hf).add | ||
| ((((analyticAt_id π x).sub analyticAt_const).pow _).smul hg) | ||
|
|
||
| lemma smul {f : π β π} {g : π β E} {x : π} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) : | ||
| MeromorphicAt (f β’ g) x := by | ||
| rcases hf with β¨m, hfβ© | ||
| rcases hg with β¨n, hgβ© | ||
| refine β¨m + n, ?_β© | ||
| convert hf.smul hg using 2 with z | ||
| rw [smul_eq_mul, β mul_smul, mul_assoc, mul_comm (f z), β mul_assoc, pow_add, | ||
| β smul_eq_mul (a' := f z), smul_assoc, Pi.smul_apply'] | ||
|
|
||
| lemma mul {f g : π β π} {x : π} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) : | ||
| MeromorphicAt (f * g) x := | ||
| hf.smul hg | ||
|
|
||
| lemma neg {f : π β E} {x : π} (hf : MeromorphicAt f x) : MeromorphicAt (-f) x := by | ||
| convert (meromorphicAt_const (-1 : π) x).smul hf using 1 | ||
| ext1 z | ||
| simp only [Pi.neg_apply, Pi.smul_apply', neg_smul, one_smul] | ||
|
|
||
| @[simp] | ||
| lemma neg_iff {f : π β E} {x : π} : | ||
| MeromorphicAt (-f) x β MeromorphicAt f x := | ||
| β¨fun h β¦ by simpa only [neg_neg] using h.neg, MeromorphicAt.negβ© | ||
|
|
||
| lemma sub {f g : π β E} {x : π} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) : | ||
| MeromorphicAt (f - g) x := by | ||
| convert hf.add hg.neg using 1 | ||
| ext1 z | ||
| simp_rw [Pi.sub_apply, Pi.add_apply, Pi.neg_apply, sub_eq_add_neg] | ||
|
|
||
| /-- With our definitions, `MeromorphicAt f x` depends only on the values of `f` on a punctured | ||
| neighbourhood of `x` (not on `f x`) -/ | ||
| lemma congr {f g : π β E} {x : π} (hf : MeromorphicAt f x) (hfg : f =αΆ [π[β ] x] g) : | ||
| MeromorphicAt g x := by | ||
| rcases hf with β¨m, hfβ© | ||
| refine β¨m + 1, ?_β© | ||
| have : AnalyticAt π (fun z β¦ z - x) x := (analyticAt_id π x).sub analyticAt_const | ||
| refine (this.smul hf).congr ?_ | ||
| rw [eventuallyEq_nhdsWithin_iff] at hfg | ||
| filter_upwards [hfg] with z hz | ||
| rcases eq_or_ne z x with rfl | hn | ||
| Β· simp | ||
| Β· rw [hz (Set.mem_compl_singleton_iff.mp hn), pow_succ, mul_smul] | ||
|
|
||
| lemma inv {f : π β π} {x : π} (hf : MeromorphicAt f x) : MeromorphicAt fβ»ΒΉ x := by | ||
| rcases hf with β¨m, hfβ© | ||
| by_cases h_eq : (fun z β¦ (z - x) ^ m β’ f z) =αΆ [π x] 0 | ||
| Β· -- silly case: f locally 0 near x | ||
| apply (meromorphicAt_const 0 x).congr | ||
| rw [eventuallyEq_nhdsWithin_iff] | ||
| filter_upwards [h_eq] with z hfz hz | ||
| rw [Pi.inv_apply, (smul_eq_zero_iff_right <| pow_ne_zero _ (sub_ne_zero.mpr hz)).mp hfz, | ||
| inv_zero] | ||
| Β· -- interesting case: use local formula for `f` | ||
| obtain β¨n, g, hg_an, hg_ne, hg_eqβ© := hf.exists_eventuallyEq_pow_smul_nonzero_iff.mpr h_eq | ||
| have : AnalyticAt π (fun z β¦ (z - x) ^ (m + 1)) x := | ||
| ((analyticAt_id π x).sub analyticAt_const).pow _ | ||
| -- use `m + 1` rather than `m` to damp out any silly issues with the value at `z = x` | ||
| refine β¨n + 1, (this.smul <| hg_an.inv hg_ne).congr ?_β© | ||
| filter_upwards [hg_eq, hg_an.continuousAt.eventually_ne hg_ne] with z hfg hg_ne' | ||
| rcases eq_or_ne z x with rfl | hz_ne | ||
| Β· simp only [sub_self, pow_succ, zero_mul, zero_smul] | ||
| Β· simp_rw [smul_eq_mul] at hfg β’ | ||
| have aux1 : f z β 0 | ||
| Β· have : (z - x) ^ n * g z β 0 := mul_ne_zero (pow_ne_zero _ (sub_ne_zero.mpr hz_ne)) hg_ne' | ||
| rw [β hfg, mul_ne_zero_iff] at this | ||
| exact this.2 | ||
| field_simp [sub_ne_zero.mpr hz_ne] | ||
| rw [pow_succ, mul_assoc, hfg] | ||
| ring | ||
|
|
||
| @[simp] | ||
| lemma inv_iff {f : π β π} {x : π} : | ||
| MeromorphicAt fβ»ΒΉ x β MeromorphicAt f x := | ||
| β¨fun h β¦ by simpa only [inv_inv] using h.inv, MeromorphicAt.invβ© | ||
|
|
||
| lemma div {f g : π β π} {x : π} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) : | ||
| MeromorphicAt (f / g) x := | ||
| (div_eq_mul_inv f g).symm βΈ (hf.mul hg.inv) | ||
|
|
||
| end MeromorphicAt |