English
If two functions have the same right derivative and share the same derivative data on a region, then their log-derivatives obey the product rule with derivatives of the second function.
Русский
Пусть две функции имеют одинаковую правую производную и общую производную на области; тогда их логарифмические производные удовлетворяют правилу произведения с производной второй функции.
LaTeX
$$$\displaystyle \logDeriv (f \circ g) = \logDeriv f \circ g \cdot \operatorname{deriv} g$$$
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)`;
* for each `x ∈ [a, b)` the right-side limit inferior of `(f z - f x) / (z - x)`
is bounded above by `B'`.
Then `f x ≤ B x` everywhere on `[a, b]`. -/
theorem image_le_of_liminf_slope_right_le_deriv_boundary {f : ℝ → ℝ} {a b : ℝ} (hf : ContinuousOn f (Icc a b))
{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` actually says `liminf (f z - f x) / (z - x) ≤ B' x`
(bound : ∀ x ∈ Ico a b, ∀ r, B' x < r → ∃ᶠ z in 𝓝[>] x, slope f x z < r) : ∀ ⦃x⦄, x ∈ Icc a b → f x ≤ B x :=
by
have Hr : ∀ x ∈ Icc a b, ∀ r > 0, f x ≤ B x + r * (x - a) := fun x hx r hr =>
by
apply image_le_of_liminf_slope_right_lt_deriv_boundary' hf bound
· rwa [sub_self, mul_zero, add_zero]
· exact hB.add (continuousOn_const.mul (continuousOn_id.sub continuousOn_const))
· intro x hx
exact (hB' x hx).add (((hasDerivWithinAt_id x (Ici x)).sub_const a).const_mul r)
· intro x _ _
rw [mul_one]
exact (lt_add_iff_pos_right _).2 hr
exact hx
intro x hx
have : ContinuousWithinAt (fun r => B x + r * (x - a)) (Ioi 0) 0 :=
continuousWithinAt_const.add (continuousWithinAt_id.mul continuousWithinAt_const)
convert continuousWithinAt_const.closure_le _ this (Hr x hx) using 1 <;> simp
