4.6. LocalMultiplicity.MeromorphicAt🔗

Jacobians.LocalMultiplicity.MeromorphicAt — source

MMeromorphicAt

f : M → ℂ is meromorphic at x : M iff its representative in the canonical chart at x, namely f ∘ (chartAt ℂ x).symm : ℂ → ℂ, is meromorphic at the chart image (chartAt ℂ x) x in the standard sense.

This is a chart-pullback definition. It is conditionally chart-independent on a complex analytic manifold; the unconditional discharge is deferred (see the file header).

def MMeromorphicAt (_I : ModelWithCorners ℂ ℂ ℂ) (f : M → ℂ) (x : M) : Prop

MMeromorphicOn

f : M → ℂ is meromorphic on s : Set M iff it is meromorphic at each point of s.

def MMeromorphicOn (I : ModelWithCorners ℂ ℂ ℂ) (f : M → ℂ) (s : Set M) : Prop

mmeromorphicOrderAt

The order of a meromorphic function f : M → ℂ at x : M, computed by chart pullback. Returns ⊤ if f is identically zero in a punctured neighborhood, a finite negative integer for poles, zero for regular nonzero points, and a positive integer for zeros (matching meromorphicOrderAt's convention).

Chart-independence is deferred; see file header.

def mmeromorphicOrderAt (_I : ModelWithCorners ℂ ℂ ℂ) (f : M → ℂ) (x : M) :
    WithTop ℤ

zero

The zero function is meromorphic at every point.

lemma zero : MMeromorphicAt I (0 : M → ℂ) x

const

Constant functions are meromorphic.

lemma const (c : ℂ) : MMeromorphicAt I (fun _ : M => c) x

add

The sum of two functions meromorphic at x is meromorphic at x.

lemma add (hf : MMeromorphicAt I f x) (hg : MMeromorphicAt I g x) :
    MMeromorphicAt I (f + g) x

mul

The product of two functions meromorphic at x is meromorphic at x.

lemma mul (hf : MMeromorphicAt I f x) (hg : MMeromorphicAt I g x) :
    MMeromorphicAt I (f * g) x

div

Pointwise quotient of two meromorphic functions is meromorphic.

lemma div (hf : MMeromorphicAt I f x) (hg : MMeromorphicAt I g x) :
    MMeromorphicAt I (f / g) x

prod

Finite products of MMeromorphicAt functions are MMeromorphicAt.

lemma prod {ι : Type*} {s : Finset ι} {F : ι → M → ℂ}
    (hF : ∀ i ∈ s, MMeromorphicAt I (F i) x) :
    MMeromorphicAt I (∏ i ∈ s, F i) x

fun_prod

Finite-prod variant: a function-valued ∏ i, F i z is MMeromorphicAt.

lemma fun_prod {ι : Type*} {s : Finset ι} {F : ι → M → ℂ}
    (hF : ∀ i ∈ s, MMeromorphicAt I (F i) x) :
    MMeromorphicAt I (fun y => ∏ i ∈ s, F i y) x

sum

Finite sums of MMeromorphicAt functions are MMeromorphicAt.

lemma sum {ι : Type*} {s : Finset ι} {F : ι → M → ℂ}
    (hF : ∀ i ∈ s, MMeromorphicAt I (F i) x) :
    MMeromorphicAt I (∑ i ∈ s, F i) x

fun_sum

Finite-sum variant: a function-valued ∑ i, F i z is MMeromorphicAt.

lemma fun_sum {ι : Type*} {s : Finset ι} {F : ι → M → ℂ}
    (hF : ∀ i ∈ s, MMeromorphicAt I (F i) x) :
    MMeromorphicAt I (fun y => ∑ i ∈ s, F i y) x

const_smul

Multiplication of a meromorphic function by a complex scalar is meromorphic.

lemma const_smul (c : ℂ) (hf : MMeromorphicAt I f x) :
    MMeromorphicAt I (c • f) x

zero

The zero function is meromorphic on every set.

lemma zero : MMeromorphicOn I (0 : M → ℂ) s

const

Constant functions are meromorphic on every set.

lemma const (c : ℂ) : MMeromorphicOn I (fun _ : M => c) s

add

The sum of two functions meromorphic on s is meromorphic on s.

lemma add (hf : MMeromorphicOn I f s) (hg : MMeromorphicOn I g s) :
    MMeromorphicOn I (f + g) s

mul

The product of two functions meromorphic on s is meromorphic on s.

lemma mul (hf : MMeromorphicOn I f s) (hg : MMeromorphicOn I g s) :
    MMeromorphicOn I (f * g) s

neg

The negation of a function meromorphic on s is meromorphic on s.

lemma neg (hf : MMeromorphicOn I f s) : MMeromorphicOn I (-f) s

sub

The difference of two functions meromorphic on s is meromorphic on s.

lemma sub (hf : MMeromorphicOn I f s) (hg : MMeromorphicOn I g s) :
    MMeromorphicOn I (f - g) s

inv

The pointwise inverse of a function meromorphic on s is meromorphic on s.

lemma inv (hf : MMeromorphicOn I f s) : MMeromorphicOn I f⁻¹ s

div

The quotient of two functions meromorphic on s is meromorphic on s.

lemma div (hf : MMeromorphicOn I f s) (hg : MMeromorphicOn I g s) :
    MMeromorphicOn I (f / g) s

pow

A natural-number power of a function meromorphic on s is meromorphic on s.

lemma pow (hf : MMeromorphicOn I f s) (n : ℕ) : MMeromorphicOn I (f ^ n) s

zpow

An integer power of a function meromorphic on s is meromorphic on s.

lemma zpow (hf : MMeromorphicOn I f s) (n : ℤ) : MMeromorphicOn I (f ^ n) s

const_smul

A complex scalar multiple of a function meromorphic on s is meromorphic on s.

lemma const_smul (c : ℂ) (hf : MMeromorphicOn I f s) :
    MMeromorphicOn I (c • f) s

prod

A finite product of functions meromorphic on s is meromorphic on s.

lemma prod {ι : Type*} {t : Finset ι} {F : ι → M → ℂ}
    (hF : ∀ i ∈ t, MMeromorphicOn I (F i) s) :
    MMeromorphicOn I (∏ i ∈ t, F i) s

fun_prod

Finite-product variant: the function fun y => ∏ i, F i y is meromorphic on s.

lemma fun_prod {ι : Type*} {t : Finset ι} {F : ι → M → ℂ}
    (hF : ∀ i ∈ t, MMeromorphicOn I (F i) s) :
    MMeromorphicOn I (fun y => ∏ i ∈ t, F i y) s

sum

A finite sum of functions meromorphic on s is meromorphic on s.

lemma sum {ι : Type*} {t : Finset ι} {F : ι → M → ℂ}
    (hF : ∀ i ∈ t, MMeromorphicOn I (F i) s) :
    MMeromorphicOn I (∑ i ∈ t, F i) s

fun_sum

Finite-sum variant: the function fun y => ∑ i, F i y is meromorphic on s.

lemma fun_sum {ι : Type*} {t : Finset ι} {F : ι → M → ℂ}
    (hF : ∀ i ∈ t, MMeromorphicOn I (F i) s) :
    MMeromorphicOn I (fun y => ∑ i ∈ t, F i y) s

comp_chart_transition_eqOn

A neighborhood-of-e x rewrite for the doubly-pulled-back representative. On every y ∈ e.target ∩ e.symm ⁻¹' (chartAt ℂ x).source, the function (f ∘ (chartAt ℂ x).symm) ∘ ((chartAt ℂ x) ∘ e.symm) agrees with f ∘ e.symm.

lemma comp_chart_transition_eqOn (_hxe : x ∈ e.source) :
    Set.EqOn ((f ∘ (chartAt ℂ x).symm) ∘ ((chartAt ℂ x) ∘ e.symm))
      (f ∘ e.symm)
      (e.target ∩ e.symm ⁻¹' (chartAt ℂ x).source)

comp_chart_transition_mem_nhds

The set on which the doubly-pulled-back representative agrees with the single-chart representative is a neighborhood of e x.

lemma comp_chart_transition_mem_nhds (hxe : x ∈ e.source) :
    e.target ∩ e.symm ⁻¹' (chartAt ℂ x).source ∈ nhds (e x)

MMeromorphicAt.iff_of_chart

Chart independence of MMeromorphicAt. If e is any chart with x ∈ e.source, and the transition (chartAt ℂ x) ∘ e.symm is analytic at e x with nonzero derivative, then MMeromorphicAt I f x is equivalent to the standard meromorphy of f ∘ e.symm at e x.

Both hypotheses are automatic on a complex analytic manifold (chart transitions are analytic biholomorphisms); see analyticAt_chart_transition_of_atlas (still open) for the discharge.

lemma MMeromorphicAt.iff_of_chart
    (hxe : x ∈ e.source)
    (h_an : AnalyticAt ℂ ((chartAt ℂ x) ∘ e.symm) (e x))
    (h_deriv : deriv ((chartAt ℂ x) ∘ e.symm) (e x) ≠ 0) :
    MMeromorphicAt I f x ↔ MeromorphicAt (f ∘ e.symm) (e x)

mmeromorphicOrderAt_eq_of_chart

Chart independence of mmeromorphicOrderAt. Under the same hypotheses as iff_of_chart, the order computed by chart pullback at the canonical chart agrees with the standard meromorphicOrderAt of f ∘ e.symm at e x.

lemma mmeromorphicOrderAt_eq_of_chart
    (hxe : x ∈ e.source)
    (h_an : AnalyticAt ℂ ((chartAt ℂ x) ∘ e.symm) (e x))
    (h_deriv : deriv ((chartAt ℂ x) ∘ e.symm) (e x) ≠ 0) :
    mmeromorphicOrderAt I f x = meromorphicOrderAt (f ∘ e.symm) (e x)

analyticAt_chart_transition_of_isManifold

The chart transition between two charts in the atlas of a complex analytic manifold is analytic at every interior point of its source. This is the unconditional discharge of the analyticity hypothesis used by MMeromorphicAt.iff_of_chart and mmeromorphicOrderAt_eq_of_chart.

lemma analyticAt_chart_transition_of_isManifold
    [IsManifold 𝓘(ℂ, ℂ) ω M]
    {e e' : OpenPartialHomeomorph M ℂ}
    (he : e ∈ atlas ℂ M) (he' : e' ∈ atlas ℂ M)
    {x : M} (hxe : x ∈ e.source) (hxe' : x ∈ e'.source) :
    AnalyticAt ℂ (e' ∘ e.symm) (e x)

deriv_chart_transition_of_isManifold_ne_zero

The derivative of the chart transition between two atlas charts is nonzero at every interior point of its source on a complex analytic manifold.

lemma deriv_chart_transition_of_isManifold_ne_zero
    [IsManifold 𝓘(ℂ, ℂ) ω M]
    {e e' : OpenPartialHomeomorph M ℂ}
    (he : e ∈ atlas ℂ M) (he' : e' ∈ atlas ℂ M)
    {x : M} (hxe : x ∈ e.source) (hxe' : x ∈ e'.source) :
    deriv (e' ∘ e.symm) (e x) ≠ 0

MMeromorphicAt.iff_of_isManifold

Unconditional chart independence of MMeromorphicAt. For any chart e ∈ atlas ℂ M of a complex analytic manifold containing x in its source, MMeromorphicAt I f x is equivalent to ordinary meromorphy of f ∘ e.symm at e x. Specializes MMeromorphicAt.iff_of_chart by discharging the analyticity and derivative-non-vanishing hypotheses on [IsManifold 𝓘(ℂ, ℂ) ω M].

lemma MMeromorphicAt.iff_of_isManifold
    [IsManifold 𝓘(ℂ, ℂ) ω M]
    (he : e ∈ atlas ℂ M)
    (hxe : x ∈ e.source) :
    MMeromorphicAt 𝓘(ℂ, ℂ) f x ↔ MeromorphicAt (f ∘ e.symm) (e x)

mmeromorphicOrderAt_eq_of_isManifold

Unconditional chart independence of mmeromorphicOrderAt. For any chart e ∈ atlas ℂ M of a complex analytic manifold containing x in its source, the chart-pullback order equals the ordinary meromorphicOrderAt of f ∘ e.symm at e x.

lemma mmeromorphicOrderAt_eq_of_isManifold
    [IsManifold 𝓘(ℂ, ℂ) ω M]
    (he : e ∈ atlas ℂ M)
    (hxe : x ∈ e.source) :
    mmeromorphicOrderAt 𝓘(ℂ, ℂ) f x = meromorphicOrderAt (f ∘ e.symm) (e x)