English
If logDeriv f equals logDeriv g on a region and certain differentiability hypotheses hold, then for all y in that region, f(y) equals g(y) provided f(a) equals g(a).
Русский
Если logDeriv f совпадает с logDeriv g на области и соблюдены условия дифференцируемости, тогда для всех y в этой области f(y) = g(y), если f(a) = g(a).
LaTeX
$$$\displaystyle \forall y\in[ a,b],\; f(y)=g(y)\quad\text{если}\quad f(a)=g(a)\text{ и условия дифференцирования выполняются}$$$
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` whenever `f x = B x`.
Then `f x ≤ B x` everywhere on `[a, b]`. -/
theorem image_le_of_deriv_right_lt_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 → f' x < B' x) : ∀ ⦃x⦄, x ∈ Icc a b → f x ≤ B x :=
image_le_of_liminf_slope_right_lt_deriv_boundary' hf (fun x hx _ hr => (hf' x hx).liminf_right_slope_le hr) ha hB hB'
bound
