characteristic_sub_characteristic_inv_at_zero

English

Away from zero, the difference between characteristic functions equals log of meromorphicTrailingCoeffAt f 0.

Русский

Вне нуля разность характеристических функций равна log MeromorphicTrailingCoeffAt f 0.

LaTeX

$$$\text{characteristic}(f) - \text{characteristic}(f^{-1}) = \log\|\text{meromorphicTrailingCoeffAt}(f,0)\|$$$

Lean4

/-- Helper lemma for the first part of the First Main Theorem: At 0, the difference between the
characteristic functions of `f` and `f⁻¹` equals `log ‖f 0‖`.
-/
theorem characteristic_sub_characteristic_inv_at_zero (h : MeromorphicOn f Set.univ) :
    characteristic f ⊤ 0 - characteristic f⁻¹ ⊤ 0 = log ‖f 0‖ := by
  calc
    characteristic f ⊤ 0 - characteristic f⁻¹ ⊤ 0
    _ = (characteristic f ⊤ - characteristic f⁻¹ ⊤) 0 := by simp
    _ = circleAverage (log ‖f ·‖) 0 0 - (divisor f Set.univ).logCounting 0 :=
      by
      rw [ValueDistribution.characteristic_sub_characteristic_inv h]
      rfl
    _ = log ‖f 0‖ := by simp

Похожие утверждения