English
There exists a family of curves α with a compatible derivative condition and a Lipschitz constant L' such that αx t is differentiable with derivative f t (α x t) on the closed ball for all x in the ball.
Русский
Существует семейство кривых с дифференцируемостью по t и линейная константа L' такая, что α x t удовлетворяет необходимым условиям производной и Липшитца на замкнутом шаре.
LaTeX
$$$\\exists α:\\; \\forall x\\in\\overline{B}(x_0,r),\\exists L'>0:\\forall t\\in Icc(t_{min},t_{max}),\\ HasDerivWithinAt (α x) (f t (α x t)) (Icc t_{min},t_{max}) t.$$$
Lean4
/-- A time-independent, continuously differentiable ODE satisfies the hypotheses of the
Picard-Lindelöf theorem. -/
theorem of_contDiffAt_one [NormedSpace ℝ E] {f : E → E} {x₀ : E} (hf : ContDiffAt ℝ 1 f x₀) (t₀ : ℝ) :
∃ (ε : ℝ) (hε : 0 < ε) (a r L K : ℝ≥0) (_ : 0 < r),
IsPicardLindelof (fun _ ↦ f) (tmin := t₀ - ε) (tmax := t₀ + ε) ⟨t₀, (by simp [le_of_lt hε])⟩ x₀ a r L K :=
by
-- Obtain ball of radius `a` within the domain in which f is `K`-lipschitz
obtain ⟨K, s, hs, hl⟩ := hf.exists_lipschitzOnWith
obtain ⟨a, ha : 0 < a, has⟩ := Metric.mem_nhds_iff.mp hs
set L := K * a + ‖f x₀‖ + 1 with hL
have hL0 : 0 < L := by positivity
have hb (x : E) (hx : x ∈ closedBall x₀ (a / 2)) : ‖f x‖ ≤ L :=
by
rw [hL]
calc
‖f x‖ ≤ ‖f x - f x₀‖ + ‖f x₀‖ := norm_le_norm_sub_add _ _
_ ≤ K * ‖x - x₀‖ + ‖f x₀‖ := by
gcongr
rw [← dist_eq_norm, ← dist_eq_norm]
apply hl.dist_le_mul x _ x₀ (mem_of_mem_nhds hs)
apply subset_trans _ has hx
exact closedBall_subset_ball <| half_lt_self ha
_ ≤ K * a + ‖f x₀‖ := by
gcongr
rw [← mem_closedBall_iff_norm]
exact closedBall_subset_closedBall (half_le_self (le_of_lt ha)) hx
_ ≤ L := le_add_of_nonneg_right zero_le_one
let ε := a / L / 2 / 2
have hε0 : 0 < ε := by positivity
refine
⟨ε, hε0, ⟨a / 2, le_of_lt <| half_pos ha⟩, ⟨a / 2, le_of_lt <| half_pos ha⟩ / 2, ⟨L, le_of_lt hL0⟩, K,
half_pos <| half_pos ha, ?_⟩
apply of_time_independent hb <| hl.mono <| subset_trans (closedBall_subset_ball (half_lt_self ha)) has
rw [NNReal.coe_mk, add_sub_cancel_left, sub_sub_cancel, max_self, NNReal.coe_div, NNReal.coe_two, NNReal.coe_mk,
mul_comm, ← le_div_iff₀ hL0, sub_half, div_right_comm (a / 2), div_right_comm a]
