differentiable_LFunction_of_sum_zero

English

If the sum of Φ over ZMod N is zero, then LFunction Φ is differentiable everywhere in s.

Русский

Если сумма Φ по ZMod N равна нулю, то LFunction Φ дифференцируема по всей плоскости s.

LaTeX

$$$$\forall s \in \mathbb{C},\quad \text{DifferentiableAt}_{\mathbb{C}}(L(\Phi, \cdot), s).$$$$

Lean4

theorem differentiable_LFunction_of_sum_zero {Φ : ZMod N → ℂ} (hΦ : ∑ j, Φ j = 0) : Differentiable ℂ (LFunction Φ) :=
  fun s ↦ differentiableAt_LFunction Φ s (Or.inr hΦ)

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