English
The logarithmic counting function is a group homomorphism from the group of locally finite supports on univ to real-valued functions, i.e., logCounting : locallyFinsuppWithin(univ) ℤ →+ (ℝ → ℝ).
Русский
Логарифмическая счетная функция является гомоморфизмом группы от локально конечной поддержки на всей области к вещественным функциям: logCounting : locallyFinsuppWithin(univ) ℤ →+ (ℝ → ℝ).
LaTeX
$$$\text{logCounting} : \bigl(\text{locallyFinsuppWithin}(\text{univ}, \mathbb{Z})\bigr) \to \mathbb{R}^{\mathbb{R}}\quad \text{ является гомоморхи́змом }(\mathbb{Z},+)$$$
Lean4
/-- The difference between the characteristic functions of `f` and `f - const` simplifies to the
difference between the proximity functions.
-/
@[simp]
theorem characteristic_sub_characteristic_eq_proximity_sub_proximity (h : MeromorphicOn f Set.univ) (a₀ : E) :
characteristic f ⊤ - characteristic (f · - a₀) ⊤ = proximity f ⊤ - proximity (f · - a₀) ⊤ := by
simp [← Pi.sub_def, characteristic, logCounting_sub_const h]
