ppow — Mathlib

English

ppow is the pointwise power of arithmetic functions: it is ζ when the exponent is 0 and f(x)^k otherwise.

Русский

ppow — поэлементное возведение арифметической функции в степень: при k=0 равно ζ, иначе f(x)^k.

LaTeX

$$$$ (f^{ppow} k)(x) = \begin{cases} \zeta(x), & k = 0, \\ f(x)^k, & k > 0. \end{cases} $$$$

Lean4

/-- This is the pointwise power of `ArithmeticFunction`s. -/
def ppow (f : ArithmeticFunction R) (k : ℕ) : ArithmeticFunction R :=
  if h0 : k = 0 then ζ else ⟨fun x ↦ f x ^ k, by simp_rw [map_zero, zero_pow h0]⟩

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