English
If two differentiable f,g have equal derivatives on an open connected set and the derivatives are equal to a fixed G-valued map, then f and g differ by a constant on that set.
Русский
Если две дифференцируемые функции имеют одинаковые производные на открытом связном множестве и эти производные равны фиксированной карте G, то f и g различаются константой на этом множестве.
LaTeX
$$$IsOpen s \\Rightarrow IsPreconnected s \\Rightarrow DifferentiableOn 𝕜 f s \\Rightarrow DifferentiableOn 𝕜 g s \\Rightarrow (fderiv 𝕜 f x = fderiv 𝕜 g x) ∀ x ∈ s \\Rightarrow s.EqOn f g s$$$
Lean4
theorem isLittleO_pow_succ {x₀ : E} {n : ℕ} (hs : Convex ℝ s) (hx₀s : x₀ ∈ s)
(hff' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hf' : f' =o[𝓝[s] x₀] fun x ↦ ‖x - x₀‖ ^ n) :
(fun x ↦ f x - f x₀) =o[𝓝[s] x₀] fun x ↦ ‖x - x₀‖ ^ (n + 1) :=
by
rw [Asymptotics.isLittleO_iff] at hf' ⊢
intro c hc
simp_rw [norm_pow, pow_succ, ← mul_assoc, norm_norm]
simp_rw [norm_pow, norm_norm] at hf'
have : ∀ᶠ x in 𝓝[s] x₀, segment ℝ x₀ x ⊆ s ∧ ∀ y ∈ segment ℝ x₀ x, ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n :=
by
have h1 : ∀ᶠ x in 𝓝[s] x₀, x ∈ s := eventually_mem_nhdsWithin
filter_upwards [h1, hs.eventually_nhdsWithin_segment hx₀s (hf' hc)] with x hxs h
refine ⟨hs.segment_subset hx₀s hxs, fun y hy ↦ (h y hy).trans ?_⟩
gcongr
exact norm_sub_le_of_mem_segment hy
filter_upwards [this] with x ⟨h_segment, h⟩
convert
(convex_segment x₀ x).norm_image_sub_le_of_norm_hasFDerivWithin_le (f := fun x ↦ f x - f x₀) (y := x) (x := x₀)
(s := segment ℝ x₀ x) ?_ h (left_mem_segment ℝ x₀ x) (right_mem_segment ℝ x₀ x) using
1
· simp
· simp only [hasFDerivWithinAt_sub_const_iff]
exact fun x hx ↦ (hff' x (h_segment hx)).mono h_segment
