logCounting_eval_zero — Mathlib

English

Away from zero, the difference between the characteristic functions of f and f−1 equals the log of the trailing coefficient of f at 0, and the boundedness is controlled by circle averages; the full statement relates circleAverage, divisor, and logCounting.

Русский

За пределами нуля разность характеристических функций f и f−1 равна логарифму коэффициента на нуле; полное утверждение связывает окружностные средние, делитель и logCounting.

LaTeX

$$$\text{characteristic } f ⊤ R - \text{characteristic } f^{-1} ⊤ R = \text{circleAverage}(\log\|f\cdot\|)0R - (\text{divisor } f univ).\logCounting R$$$

Lean4

/-- Evaluation of the logarithmic counting function at zero yields zero.
-/
@[simp]
theorem logCounting_eval_zero : logCounting f a 0 = 0 := by by_cases h : a = ⊤ <;> simp [logCounting, h]

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