English
If two continuous functions f and g on [a,b] have identical right derivatives and f(a)=g(a), then |f(x)−g(x)| ≤ 0 for all x in [a,b], i.e. f=g on [a,b].
Русский
Если f и g непрерывны на [a,b] и имеют одинаковую правую производную и f(a)=g(a), то они совпадают на всём [a,b].
LaTeX
$$$\displaystyle f=g\text{ on }[a,b]\quad\text{when } f(a)=g(a)\text{ and } \text{HasDerivRight } f = \text{HasDerivRight } g.$$$
Lean4
/-- A function on `[a, b]` with the norm of the right derivative bounded by `C`
satisfies `‖f x - f a‖ ≤ C * (x - a)`. -/
theorem norm_image_sub_le_of_norm_deriv_right_le_segment {f' : ℝ → E} {C : ℝ} (hf : ContinuousOn f (Icc a b))
(hf' : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x) (bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ C) :
∀ x ∈ Icc a b, ‖f x - f a‖ ≤ C * (x - a) := by
let g x := f x - f a
have hg : ContinuousOn g (Icc a b) := hf.sub continuousOn_const
have hg' : ∀ x ∈ Ico a b, HasDerivWithinAt g (f' x) (Ici x) x :=
by
intro x hx
simp [g, hf' x hx]
let B x := C * (x - a)
have hB : ∀ x, HasDerivAt B C x := by
intro x
simpa using (hasDerivAt_const x C).mul ((hasDerivAt_id x).sub (hasDerivAt_const x a))
convert image_norm_le_of_norm_deriv_right_le_deriv_boundary hg hg' _ hB bound
simp only [g, B]; rw [sub_self, norm_zero, sub_self, mul_zero]
