English
Given differentiable functions f, g on a region s where they do not vanish, the log-derivatives are equal on s if and only if f is a nonzero scalar multiple of g on s.
Русский
Пусть f, g дифференцируемы на области s и не обращаются к нулю; тогда logDeriv f = logDeriv g на s тогда и только тогда, когда существует не нулевой коэффициент λ с f = λ g на s.
LaTeX
$$$\displaystyle \operatorname{EqOn}\bigl(\logDeriv f, \logDeriv g\bigr)\; s \,\Longleftrightarrow \, \exists z \,(z \neq 0) \land \operatorname{EqOn}(f, z \cdot g)\; s$$$
Lean4
theorem logDeriv_eqOn_iff [IsRCLikeNormedField 𝕜] {f g : 𝕜 → 𝕜'} {s : Set 𝕜} (hf : DifferentiableOn 𝕜 f s)
(hg : DifferentiableOn 𝕜 g s) (hs2 : IsOpen s) (hsc : IsPreconnected s) (hgn : ∀ x ∈ s, g x ≠ 0)
(hfn : ∀ x ∈ s, f x ≠ 0) : EqOn (logDeriv f) (logDeriv g) s ↔ ∃ z : 𝕜', z ≠ 0 ∧ EqOn f (z • g) s :=
by
rcases s.eq_empty_or_nonempty with rfl | ⟨t, ht⟩
· simpa using ⟨1, one_ne_zero⟩
· constructor
· refine fun h ↦ ⟨f t * (g t)⁻¹, by grind, fun y hy ↦ ?_⟩
have hderiv : s.EqOn (deriv (f * g⁻¹)) (deriv f * g⁻¹ - f * deriv g / g ^ 2) :=
by
intro z hz
rw [deriv_mul (hf.differentiableAt (hs2.mem_nhds hz)) ((hg.differentiableAt (hs2.mem_nhds hz)).inv (hgn z hz))]
simp only [Pi.inv_apply, show g⁻¹ = (fun x => x⁻¹) ∘ g by rfl, deriv_inv, neg_mul,
deriv_comp z (differentiableAt_inv (hgn z hz)) (hg.differentiableAt (hs2.mem_nhds hz)), mul_neg, Pi.sub_apply,
Pi.mul_apply, comp_apply, Pi.div_apply, Pi.pow_apply]
ring
have hfg : EqOn (deriv (f * g⁻¹)) 0 s :=
hderiv.trans fun z hz ↦
by
simp only [Pi.sub_apply, Pi.mul_apply, Pi.inv_apply, Pi.div_apply, Pi.pow_apply, Pi.zero_apply]
grind [logDeriv_apply, Pi.div_apply]
letI := IsRCLikeNormedField.rclike 𝕜
obtain ⟨a, ha⟩ := hs2.exists_is_const_of_deriv_eq_zero hsc (hf.mul (hg.inv hgn)) hfg
grind [Pi.mul_apply, Pi.inv_apply, Pi.smul_apply, smul_eq_mul]
· rintro ⟨z, hz0, hz⟩ x hx
simp [logDeriv_apply, hz.deriv hs2 hx, hz hx, deriv_const_smul _ (hg.differentiableAt (hs2.mem_nhds hx)),
mul_div_mul_left (deriv g x) (g x) hz0]
