[Merged by Bors] - feat(analysis/ODE/picard_lindelof): Add corollaries to ODE solution existence theorem

[winstonyin]

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.

---

[kbuzzard]

I don't know the mathematics but I left some style comments.

[tb65536]

Here are some golfs.

[ocfnash]

Thanks for working on this and sorry we've been so slow reviewing.

The mathematical content, time_indep_cont_diff_on_nhds_is_picard_lindelof is certainly worth having but I think there are some minor points of style and also of structure that deserve attention.

First the minor points of style:

• As things stand, there is scope for you to use variables much more and it will make the content easier to read
• The set and metric namespaces are open so you can drop a lot of set. and metric. prefixes which will make things easier to read.
• Where possible, it is often preferable to leave type ascriptions out of quantified expressions. E.g., we usually prefer ∀ t rather than ∀ (t : ℝ) or ∀ t : ℝ
• It is sometimes (not always) desirable to drop redundant parentheses. E.g., we prefer ∃ f : ℝ → E, ... to ∃ (f : ℝ → E), ...
• We have special support for quantifying over sets. E.g., we prefer ∀ t ∈ s, ... to ∀ t, t ∈ s → ...
• We almost always try to name lemmas based on the type of hypothesis / conclusion rather than the mathematical content. E.g., we would prefer exists_forall_deriv_within_Icc_eq_of_lipschitz_of_is_picard_lindelof to ODE_solution_exists

As to the structure:

• I think the proposed: @[reducible] def is_picard_lindelof would be better as structure is_picard_lindelof so that we get named hypotheses.
• I would place it next to the existing structure picard_lindelof and use the comments and file doc string to explain that is_picard_lindelof is intended for use in the public API whereas structure picard_lindelof is just a convenience to avoid constantly invoking choice that is used as an internal API
• I would restate exists_forall_deriv_within_Icc_eq_of_lipschitz_of_continuous using your new is_picard_lindelof and I would probably drop all the proposed new ODE_solution_exists. lemmas: they don't look worth it to me.

Please feel free to push back if you have applications that challenge these suggestions, and thanks again for this work.

[winstonyin]

Thanks for the comments, @ocfnash ! The benefit of is_picard_lindelof is that it is a Prop, and the constants L, R, C behind a ∃ can be discharged without invoking choice. The Lipschitz constant, for instance, often merely exists. Writing it as a non-Prop structure seems to remove this benefit and also make it essentially the same as the existing picard_lindelof. In fact, statements like ∃ (ε : ℝ) (hε : 0 < ε), is_picard_lindelof (λ t, v) (t₀ - ε) t₀ (t₀ + ε) x₀ will no longer work because it is not a Prop. Am I missing something?

One way to keep the structure a Prop is by writing

structure is_picard_lindelof
  {E : Type*} [normed_add_comm_group E] (v : ℝ → E → E) (t_min t₀ t_max : ℝ) (x₀ : E) (L R C : ℝ≥0) : Prop :=
(lipschitz : ...) (cont : ...) (norm_le : ...) (C_mul_le_R : ...)

and use it with ∃ L R C, is_picard_lindelof v t_min t₀ t_max x₀ L R C. Is this how you're imagining it?

[ocfnash]

The benefit of is_picard_lindelof is that it is a Prop, and ... Am I missing something?

You are not missing anything and I agree with your remarks: what I wrote was not quite right. Here is the sort of thing that I was attempting to suggest:

structure is_picard_lindelof {E : Type*} [normed_add_comm_group E]
  (v : ℝ → E → E) (t_min t₀ t_max : ℝ) (x₀ : E) (L : ℝ≥0) (R C : ℝ) : Prop :=
(lipschitz' : ∀ t ∈ Icc t_min t_max, lipschitz_on_with L (v t) (closed_ball x₀ R))
(cont : ∀ x ∈ closed_ball x₀ R, continuous_on (λ t, v t x) (Icc t_min t_max))
(norm_le' : ∀ (t ∈ Icc t_min t_max) (x ∈ closed_ball x₀ R), ∥v t x∥ ≤ C)
(C_mul_le_R : C * max (t_max - t₀) (t₀ - t_min) ≤ R)

@[reducible] def exists_is_picard_lindelof
  {E : Type*} [normed_add_comm_group E] (v : ℝ → E → E) (t_min t₀ t_max : ℝ) (x₀ : E) : Prop :=
∃ L R C (hR : 0 ≤ R), is_picard_lindelof v t_min t₀ t_max x₀ L R C

I think this is probably a good design, especially if it is possible to share some of the code with picard_lindelof. I am being told to close my laptop now so I'll have to come back to this again tomorrow.

[winstonyin]

Those are very helpful comments. I've implemented structure is_picard_lindelof containing all the Prop hypotheses (including t₀ ∈ Icc t_min t_max and 0 ≤ R), removed all the ODE_solution_exists lemmas, renamed the theorems, tidied up the variables, and removed the extraneous set. and metric..

[ocfnash]

Thanks for all the work, I think this is close to being ready now.

[winstonyin]

I've implemented the suggestions you've made. I forgot to add one lemma which will be useful for #17140, so I've added it in the newest commit. Please kindly review also.

[ocfnash]

Thanks for sticking with this. This will be good to go once the final suggestions have been addressed.

bors d+

[bors]

✌️ winstonyin can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[winstonyin]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests