mathlib

f97c17d5 - feat(analysis/ODE/picard_lindelof): Add corollaries to ODE solution existence theorem (#16348)

feat(analysis/ODE/picard_lindelof): Add corollaries to ODE solution existence theorem (#16348) We add some corollaries to the existence theorem of solutions to autonomous ODEs (Picard-Lindelöf / Cauchy-Lipschitz theorem). * `is_picard_lindelof`: Predicate for the very long hypotheses of the Picard-Lindelöf theorem. * When applying `exists_forall_deriv_within_Icc_eq_of_lipschitz_of_continuous` directly to unite with a goal, Lean introduces a long list of goals with many meta-variables. The predicate makes the proof of these hypotheses more manageable. * Certain variables in the hypotheses, such as the Lipschitz constant, are often obtained from other facts non-constructively, so it is less convenient to directly use them to satisfy hypotheses (needing `Exists.some`). We avoid this problem by stating these non-`Prop` hypotheses under `∃`. * Solution `f` exists on any subset `s` of some closed interval, where the derivative of `f` is defined by the value of `f` within `s` only. * Solution `f` exists on any open subset `s` of some closed interval. * There exists `ε > 0` such that a solution `f` exists on `(t₀ - ε, t₀ + ε)`. * As a simple example, we show that time-independent, locally continuously differentiable ODEs satisfy `is_picard_lindelof` and hence a solution exists within some open interval.