E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
f₁ f₂ : FunSpace v
n : ℕ
t : ↑(Icc v.tMin v.tMax)
⊢ (↑v.L * abs (↑t - ↑v.t₀)) ^ n / ↑n ! * dist f₁ f₂ ≤ (↑v.L * tDist v) ^ n / ↑n ! * dist f₁ f₂
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
f₁ f₂ : FunSpace v
n : ℕ
⊢ dist ((next^[n]) f₁) ((next^[n]) f₂) ≤ (↑v.L * tDist v) ^ n / ↑n ! * dist f₁ f₂
refine' dist_le_of_forall fun t => (dist_iterate_next_apply_le _ _ _ _).trans _
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
f₁ f₂ : FunSpace v
n : ℕ
t : ↑(Icc v.tMin v.tMax)
this : abs (↑t - ↑v.t₀) ≤ tDist v
⊢ (↑v.L * abs (↑t - ↑v.t₀)) ^ n / ↑n ! * dist f₁ f₂ ≤ (↑v.L * tDist v) ^ n / ↑n ! * dist f₁ f₂
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
f₁ f₂ : FunSpace v
n : ℕ
t : ↑(Icc v.tMin v.tMax)
⊢ (↑v.L * abs (↑t - ↑v.t₀)) ^ n / ↑n ! * dist f₁ f₂ ≤ (↑v.L * tDist v) ^ n / ↑n ! * dist f₁ f₂
have : |(t - v.t₀ : ℝ)| ≤ v.tDist := v.dist_t₀_le t
no goals
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
inst✝ : CompleteSpace E
f₁ f₂ : FunSpace v
n : ℕ
t : ↑(Icc v.tMin v.tMax)
this : abs (↑t - ↑v.t₀) ≤ tDist v
⊢ (↑v.L * abs (↑t - ↑v.t₀)) ^ n / ↑n ! * dist f₁ f₂ ≤ (↑v.L * tDist v) ^ n / ↑n ! * dist f₁ f₂
gcongr