differentiable_completedLFunction

English

Under the standard hypotheses, the function s ↦ completedLFunction Φ s is differentiable for all s.

Русский

При стандартных гипотезах функция s ↦ completedLFunction Φ s дифференцируема по всем s.

LaTeX

$$$$\text{Differentiable} (\,s\mapsto \mathrm{completedLFunction}(\Phi, s)\,).$$$$

Lean4

/-- Special case of `differentiableAt_completedLFunction` asserting differentiability everywhere
under suitable hypotheses.
-/
theorem differentiable_completedLFunction (hΦ₂ : Φ 0 = 0) (hΦ₃ : ∑ j, Φ j = 0) :
    Differentiable ℂ (completedLFunction Φ) := fun s ↦ differentiableAt_completedLFunction Φ s (.inr hΦ₂) (.inr hΦ₃)

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