English
If logDeriv f equals logDeriv g on an open preconnected set under suitable differentiability and nonvanishing hypotheses, then f is a nonzero scalar multiple of g on that set.
Русский
Если logDeriv f совпадает с logDeriv g на открытом предподсоединённом множестве при подходящих услових дифференцируемости и ненулевых значениях, то f = z g на этом множестве для некоторого не нулевого z.
LaTeX
$$$\displaystyle \forall s:\, \, \text{IsOpen}(s)\,\; (\text{DifferentiableOn } f \, s) \land (\text{DifferentiableOn } g \, s)\;\Rightarrow\;\Bigl(\operatorname{EqOn}(\logDeriv f, \logDeriv g)\, s \leftrightarrow \exists z \; z \neq 0 \land \operatorname{EqOn}(f, z \cdot g)\, s\Bigr)$$$
Lean4
/-- General fencing theorem for continuous functions with an estimate on the derivative.
Let `f` and `B` be continuous functions on `[a, b]` such that
* `f a ≤ B a`;
* `B` has derivative `B'` everywhere on `ℝ`;
* for each `x ∈ [a, b)` the right-side limit inferior of `(f z - f x) / (z - x)`
is bounded above by a function `f'`;
* we have `f' x < B' x` whenever `f x = B x`.
Then `f x ≤ B x` everywhere on `[a, b]`. -/
theorem image_le_of_liminf_slope_right_lt_deriv_boundary {f f' : ℝ → ℝ} {a b : ℝ}
(hf : ContinuousOn f (Icc a b))
-- `hf'` actually says `liminf (f z - f x) / (z - x) ≤ f' x`
(hf' : ∀ x ∈ Ico a b, ∀ r, f' x < r → ∃ᶠ z in 𝓝[>] x, slope f x z < r) {B B' : ℝ → ℝ} (ha : f a ≤ B a)
(hB : ∀ x, HasDerivAt B (B' x) x) (bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x) :
∀ ⦃x⦄, x ∈ Icc a b → f x ≤ B x :=
image_le_of_liminf_slope_right_lt_deriv_boundary' hf hf' ha (fun x _ => (hB x).continuousAt.continuousWithinAt)
(fun x _ => (hB x).hasDerivWithinAt) bound
