logCounting — Mathlib

English

For any complex constant c, radius R ≠ 0, and integer-valued D with finite support, the finsum identity holds: the sum over u of D(u)(log R − log||c−u||) equals the finsum over u of D(u) log(R||c−u||^{-1}) plus D(c) log R.

Русский

Для константы c, радиуса R ≠ 0 и функции D с конечной опорой выполняется равенство: сумма finsum_u D(u)(log R − log||c−u||) = сумма finsum_u D(u) log(R||c−u||^{-1}) + D(c) log R.

LaTeX

$$$\sum^{\infty}_{u} D(u)\bigl(\log R - \log \|c-u\|\bigr) = \sum^{\infty}_{u} D(u) \log\bigl(R \|c-u\|^{-1}\bigr) + D(c)\log R, \quad (R \neq 0,\ D\text{ finite support})$$$

Lean4

/-- Definition of the logarithmic counting function, as a group morphism mapping functions `D` with
locally finite support to maps `ℝ → ℝ`.  Given `D`, the result map `logCounting D` takes `r : ℝ` to
a logarithmically weighted measure of values that `D` takes within the disk `∣z∣ ≤ r`.

Implementation Note: In case where `z = 0`, the term `log (r * ‖z‖⁻¹)` evaluates to zero, which is
typically different from `log r - log ‖z‖ = log r`. The summand `(D 0) * log r` compensates this,
producing cleaner formulas when the logarithmic counting function is used in the main theorems of
Value Distribution Theory.  We refer the reader to page 164 of [Lang: Introduction to Complex
Hyperbolic Spaces](https://link.springer.com/book/10.1007/978-1-4757-1945-1) for more details, and
to the lemma `countingFunction_finsum_eq_finsum_add` for a formal statement.
-/
noncomputable def logCounting {E : Type*} [NormedAddCommGroup E] [ProperSpace E] :
    locallyFinsuppWithin (univ : Set E) ℤ →+ (ℝ → ℝ)
    where
  toFun D := fun r ↦ ∑ᶠ z, D.toClosedBall r z * log (r * ‖z‖⁻¹) + (D 0) * log r
  map_zero' := by aesop
  map_add' D₁
    D₂ := by
    simp only [map_add, coe_add, Pi.add_apply, Int.cast_add]
    ext r
    have {A B C D : ℝ} : A + B + (C + D) = A + C + (B + D) := by ring
    rw [Pi.add_apply, this]
    congr 1
    · have h₁s : ((D₁.toClosedBall r).support ∪ (D₂.toClosedBall r).support).Finite :=
        by
        apply Set.finite_union.2
        constructor <;> apply finiteSupport _ (isCompact_closedBall 0 |r|)
      repeat
        rw [finsum_eq_sum_of_support_subset (s := h₁s.toFinset)]
        try simp_rw [← Finset.sum_add_distrib, ← add_mul]
      repeat
        intro x hx
        by_contra
        simp_all
    · ring

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