English
The divisor of a meromorphic function f on U at a point z is 0 unless z ∈ U and f is meromorphic there; when defined, it equals the order meromorphicOrderAt(f,z) untop₀.
Русский
Делитель мероморфной функции f на U в точке z равен 0, если z ∉ U или f не мероморфна; иначе делитель равен meromorphicOrderAt(f,z) untop₀.
LaTeX
$$$\text{divisor}(f, U)(z) = \begin{cases} (meromorphicOrderAt(f, z)).untop_0, & \text{если } MeromorphicOn(f, U) \land z \in U; \\ 0, & \text{иначе}. \end{cases}$$$
Lean4
/-- The divisor of a meromorphic function `f`, mapping a point `z` to the order of `f` at `z`, and to
zero if the order is infinite.
-/
noncomputable def divisor (f : 𝕜 → E) (U : Set 𝕜) : Function.locallyFinsuppWithin U ℤ
where
toFun := fun z ↦ if MeromorphicOn f U ∧ z ∈ U then (meromorphicOrderAt f z).untop₀ else 0
supportWithinDomain' z
hz := by
by_contra h₂z
simp [h₂z] at hz
supportLocallyFiniteWithinDomain' :=
by
simp_all only [Function.support_subset_iff, ne_eq, ite_eq_right_iff, WithTop.untop₀_eq_zero, and_imp,
Classical.not_imp, not_or, implies_true, ← supportDiscreteWithin_iff_locallyFiniteWithin]
by_cases hf : MeromorphicOn f U
· filter_upwards [mem_codiscrete_subtype_iff_mem_codiscreteWithin.1
hf.codiscrete_setOf_meromorphicOrderAt_eq_zero_or_top]
simp only [Set.mem_image, Set.mem_setOf_eq, Subtype.exists, exists_and_left, exists_prop, exists_eq_right_right,
Pi.ofNat_apply, ite_eq_right_iff, WithTop.untop₀_eq_zero, and_imp]
tauto
· simp [hf, Pi.zero_def]
