English
Let P be a WeakFEPair. If either s ≠ 0 or f₀ = 0, and either s ≠ k or g₀ = 0, then Λ is differentiable at s.
Русский
Пусть P — слабый FEP-пар. При выполнении условий (s ≠ 0 или f₀ = 0) и (s ≠ k или g₀ = 0) функция Λ дифференцируема в точке s.
LaTeX
$$$((s \\neq 0) \\lor (f_0 = 0)) \\land ((s \\neq k) \\lor (g_0 = 0)) \\Rightarrow \\mathrm{DifferentiableAt}_{\\mathbb{C}}(\\Lambda)(s)$$$
Lean4
theorem differentiableAt_Λ {s : ℂ} (hs : s ≠ 0 ∨ P.f₀ = 0) (hs' : s ≠ P.k ∨ P.g₀ = 0) : DifferentiableAt ℂ P.Λ s :=
by
refine ((P.differentiable_Λ₀ s).sub ?_).sub ?_
· rcases hs with hs | hs
· simpa using (differentiableAt_inv hs).smul_const _
· simp [hs]
· rcases hs' with hs' | hs'
· apply DifferentiableAt.smul_const
apply (differentiableAt_const _).div ((differentiableAt_const _).sub (differentiable_id _))
simpa [sub_eq_zero, eq_comm]
· simp [hs']
