deriv_LFunctionTrivChar₁_apply_of_ne_one

English

If hs: s ≠ 1, then deriv LFunctionTrivChar₁ n s = (s − 1) deriv LFunctionTrivChar n s + LFunctionTrivChar n s.

Русский

Если s ≠ 1, то производная LFunctionTrivChar₁ n s равна (s−1) произведной LFunctionTrivChar n s плюс LFunctionTrivChar n s.

LaTeX

$$$\dfrac{d}{ds} LFunctionTrivChar_1(n,s) = (s-1) \dfrac{d}{ds} LFunctionTrivChar(n,s) + LFunctionTrivChar(n,s) \quad (s \neq 1)$$$

Lean4

theorem deriv_LFunctionTrivChar₁_apply_of_ne_one {s : ℂ} (hs : s ≠ 1) :
    deriv (LFunctionTrivChar₁ n) s = (s - 1) * deriv (LFunctionTrivChar n) s + LFunctionTrivChar n s :=
  by
  have H : deriv (LFunctionTrivChar₁ n) s = deriv (fun w ↦ (w - 1) * LFunctionTrivChar n w) s :=
    by
    refine eventuallyEq_iff_exists_mem.mpr ?_ |>.deriv_eq
    exact ⟨_, isOpen_ne.mem_nhds hs, fun _ hw ↦ Function.update_of_ne (Set.mem_setOf.mp hw) ..⟩
  rw [H, deriv_fun_mul (by fun_prop) (differentiableAt_LFunction _ s (.inl hs)), deriv_sub_const, deriv_id'', one_mul,
    add_comm]

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