Commit 2022-10-28 02:45 f97c17d5

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.