English
The map next hf hx α has the form toPicard: toFun; its value at t is picard(f,t0,x,α.compProj)(t).
Русский
Оператор next имеет вид перехода к Пикару: next hf hx α (t) = picard(f,t0,x,α.compProj)(t).
LaTeX
$$next(hf,hx,α)(t) = picard(f,t0,x,α.compProj)(t)$$
Lean4
/-- The map on `FunSpace` defined by `picard`, some `n`-th iterate of which will be a contracting
map -/
noncomputable def next (hf : IsPicardLindelof f t₀ x₀ a r L K) (hx : x ∈ closedBall x₀ r) (α : FunSpace t₀ x₀ r L) :
FunSpace t₀ x₀ r L where
toFun t := picard f t₀ x α.compProj t
lipschitzWith :=
LipschitzWith.of_dist_le_mul fun t₁ t₂ ↦
by
rw [dist_eq_norm, picard_apply, picard_apply, add_sub_add_left_eq_sub,
integral_interval_sub_left (intervalIntegrable_comp_compProj hf _ t₁)
(intervalIntegrable_comp_compProj hf _ t₂),
Subtype.dist_eq, Real.dist_eq]
apply intervalIntegral.norm_integral_le_of_norm_le_const
intro t ht
have ht : t ∈ Icc tmin tmax := subset_trans uIoc_subset_uIcc (uIcc_subset_Icc t₂.2 t₁.2) ht
exact hf.norm_le _ ht _ <| α.mem_closedBall hf.mul_max_le
mem_closedBall₀ := by simp [hx]
