English
If logDeriv f equals logDeriv g on a region and for all points in the region, the equality of f and g propagates via scalar multiplication, then the equivalence holds.
Русский
Если logDeriv f совпадает logDeriv g на области, и для всех точек области равенство f и g передается через скалярное умножение, тогда равенство сохраняется.
LaTeX
$$$\displaystyle \operatorname{EqOn}(\logDeriv f, \logDeriv g)\; s \Longrightarrow \exists z \neq 0:\; \operatorname{EqOn}(f, z \cdot g)\; s$$$
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 right derivative `B'` at every point of `[a, b)`;
* `f` has right derivative `f'` at every point of `[a, b)`;
* we have `f' x ≤ B' x` on `[a, b)`.
Then `f x ≤ B x` everywhere on `[a, b]`. -/
theorem image_le_of_deriv_right_le_deriv_boundary {f f' : ℝ → ℝ} {a b : ℝ} (hf : ContinuousOn f (Icc a b))
(hf' : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x) {B B' : ℝ → ℝ} (ha : f a ≤ B a)
(hB : ContinuousOn B (Icc a b)) (hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x)
(bound : ∀ x ∈ Ico a b, f' x ≤ B' x) : ∀ ⦃x⦄, x ∈ Icc a b → f x ≤ B x :=
image_le_of_liminf_slope_right_le_deriv_boundary hf ha hB hB' fun x hx _ hr =>
(hf' x hx).liminf_right_slope_le (lt_of_le_of_lt (bound x hx) hr)
