• ht₀ : t₀ ∈ set.Icc t_min t_max
• hR : 0 ≤ R
• lipschitz : ∀ (t : ℝ), t ∈ set.Icc t_min t_max → lipschitz_on_with L (v t) (metric.closed_ball x₀ R)
• cont : ∀ (x : E), x ∈ metric.closed_ball x₀ R → continuous_on (λ (t : ℝ), v t x) (set.Icc t_min t_max)
• norm_le : ∀ (t : ℝ), t ∈ set.Icc t_min t_max → ∀ (x : E), x ∈ metric.closed_ball x₀ R → ‖v t x‖ ≤ C
• C_mul_le_R : C * linear_order.max (t_max - t₀) (t₀ - t_min) ≤ R

Prop structure holding the hypotheses of the Picard-Lindelöf theorem.

The similarly named picard_lindelof structure is part of the internal API for convenience, so as not to constantly invoke choice, but is not intended for public use.

• to_fun : ℝ → E → E
• t_min : ℝ
• t_max : ℝ
• t₀ : ↥(set.Icc self.t_min self.t_max)
• x₀ : E
• C : nnreal
• R : nnreal
• L : nnreal
• is_pl : is_picard_lindelof self.to_fun self.t_min ↑(self.t₀) self.t_max self.x₀ self.L ↑(self.R) ↑(self.C)

This structure holds arguments of the Picard-Lipschitz (Cauchy-Lipschitz) theorem. It is part of the internal API for convenience, so as not to constantly invoke choice. Unless you want to use one of the auxiliary lemmas, use exists_forall_deriv_within_Icc_eq_of_lipschitz_of_continuous instead of using this structure.

The similarly named is_picard_lindelof is a bundled Prop holding the long hypotheses of the Picard-Lindelöf theorem as named arguments. It is used as part of the public API.

• to_fun : ↥(set.Icc v.t_min v.t_max) → E
• map_t₀' : self.to_fun v.t₀ = v.x₀
• lipschitz' : lipschitz_with v.C self.to_fun

The space of curves $γ \colon [t_{\min}, t_{\max}] \to E$ such that $γ(t₀) = x₀$ and $γ$ is Lipschitz continuous with constant $C$. The map sending $γ$ to $\mathbf Pγ(t)=x₀ + ∫_{t₀}^{t} v(τ, γ(τ))\,dτ$ is a contracting map on this space, and its fixed point is a solution of the ODE $\dot x=v(t, x)$.