English
There exist n and C such that the nth iterate of next is contracting with constant C, independent of the chosen initial base point in the ball.
Русский
Существуют n и C, такие что n-я итерация next является сжимающей с константой C независимо от выбранной начальной точки внутри шара.
LaTeX
$$$\\exists n\\in\\mathbb{N},\\exists C\\ge 0:\\forall x\\in\\overline{B}(x_0,r),\\ ContractingWith\\ C\\ (\\text{next hf hx})^{[n]}.$$$
Lean4
/-- If the time-dependent vector field `f` and the curve `α` are continuous, then `f t (α t)` is the
derivative of `picard f t₀ x₀ α`. -/
theorem hasDerivWithinAt_picard_Icc (ht₀ : t₀ ∈ Icc tmin tmax) (hf : ContinuousOn (uncurry f) ((Icc tmin tmax) ×ˢ u))
(hα : ContinuousOn α (Icc tmin tmax)) (hmem : ∀ t ∈ Icc tmin tmax, α t ∈ u) (x₀ : E) {t : ℝ}
(ht : t ∈ Icc tmin tmax) : HasDerivWithinAt (picard f t₀ x₀ α) (f t (α t)) (Icc tmin tmax) t :=
by
apply HasDerivWithinAt.const_add
have : Fact (t ∈ Icc tmin tmax) :=
⟨ht⟩ -- needed to synthesise `FTCFilter` for `Icc`
apply
intervalIntegral.integral_hasDerivWithinAt_right
_ -- need `CompleteSpace E` and `Icc`
(continuousOn_comp hf hα hmem |>.stronglyMeasurableAtFilter_nhdsWithin measurableSet_Icc t)
(continuousOn_comp hf hα hmem _ ht)
apply ContinuousOn.intervalIntegrable
apply continuousOn_comp hf hα hmem |>.mono
by_cases h : t < t₀
· rw [uIcc_of_gt h]
exact Icc_subset_Icc ht.1 ht₀.2
· rw [uIcc_of_le (not_lt.mp h)]
exact Icc_subset_Icc ht₀.1 ht.2
