English
There exists a global Lipschitz-type control L' such that the derivative of the fixed-point map is bounded by L' times the distance in the initial data, uniformly over x in a closed ball and initial derivatives fixed.
Русский
Существует глобальная константа Л Lipschitz-ограничения L', так что производная отображения фиксированного точки ограничена L' по расстоянию в начальном условии, равномерно по x в шаре.
LaTeX
$$$\\exists L'\\ge 0:\\ \\forall x,y\\in B,\\forall \\alpha,\\beta:\\ IsFixedPt(\\text{next } hf hx), IsFixedPt(\\text{next } hf hy) \\implies dist(\\alpha,\\beta) \\le L' \\ dist(x,y).$$$
Lean4
/-- **Picard-Lindelöf (Cauchy-Lipschitz) theorem**, differential form. This version shows the
existence of a local flow and that it is Lipschitz continuous in the initial point. -/
theorem exists_forall_mem_closedBall_eq_hasDerivWithinAt_lipschitzOnWith (hf : IsPicardLindelof f t₀ x₀ a r L K) :
∃ α : E → ℝ → E,
(∀ x ∈ closedBall x₀ r,
α x t₀ = x ∧ ∀ t ∈ Icc tmin tmax, HasDerivWithinAt (α x) (f t (α x t)) (Icc tmin tmax) t) ∧
∃ L' : ℝ≥0, ∀ t ∈ Icc tmin tmax, LipschitzOnWith L' (α · t) (closedBall x₀ r) :=
by
have (x) (hx : x ∈ closedBall x₀ r) := FunSpace.exists_isFixedPt_next hf hx
choose α hα using this
set α' := fun (x : E) ↦ if hx : x ∈ closedBall x₀ r then α x hx |>.compProj else 0 with hα'
refine ⟨α', fun x hx ↦ ⟨?_, fun t ht ↦ ?_⟩, ?_⟩
· rw [hα']
beta_reduce
rw [dif_pos hx, FunSpace.compProj_val, ← hα, FunSpace.next_apply₀]
· rw [hα']
beta_reduce
rw [dif_pos hx, FunSpace.compProj_apply]
apply
hasDerivWithinAt_picard_Icc t₀.2 hf.continuousOn_uncurry (α x hx |>.continuous_compProj.continuousOn)
(fun _ ht' ↦ α x hx |>.compProj_mem_closedBall hf.mul_max_le) x ht |>.congr_of_mem
_ ht
intro t' ht'
nth_rw 1 [← hα]
rw [FunSpace.compProj_of_mem ht', FunSpace.next_apply]
· obtain ⟨L', h⟩ := FunSpace.exists_forall_closedBall_funSpace_dist_le_mul hf
refine ⟨L', fun t ht ↦ LipschitzOnWith.of_dist_le_mul fun x hx y hy ↦ ?_⟩
simp_rw [hα']
rw [dif_pos hx, dif_pos hy, FunSpace.compProj_apply, FunSpace.compProj_apply, ←
FunSpace.toContinuousMap_apply_eq_apply, ← FunSpace.toContinuousMap_apply_eq_apply]
have : Nonempty (Icc tmin tmax) := ⟨t₀⟩
apply ContinuousMap.dist_le_iff_of_nonempty.mp
exact h x y hx hy (α x hx) (α y hy) (hα x hx) (hα y hy)
