more picard_lindelof

Stream: Is there code for X?

[Winston Yin]

There's docs#exists_forall_deriv_within_Icc_eq_of_lipschitz_of_continuous in analysis.ODE.picard_lindelof, which of course is very nice. It seems to me that we need a bunch of weaker variants of these, e.g. for time-independent ODEs, equation being cont_diff, etc. Do these exist or should I make a couple of these?

[Winston Yin]

For example, I have already written one for time-independent cont_diff ODEs:

theorem exists_forall_deriv_within_Ioo_eq_of_cont_diff
  {E : Type*} [normed_add_comm_group E] [normed_space ℝ E] [complete_space E] [proper_space E]
  {v : E → E} (hv : cont_diff ℝ 1 v) (t₀ : ℝ) (x₀ : E) :
  ∃ (ε : ℝ) (hε : ε > 0) (f : ℝ → E), f t₀ = x₀ ∧ ∀ t ∈ metric.ball t₀ ε, has_deriv_at f (v (f t)) t :=

[Winston Yin]

I've made a PR (#16348) for some corollaries to the existence theorem of ODE solutions. It seems easier to me to write the very long hypotheses of the theorem as a single existential is_picard_lindelof. Using the corollaries, it is shown that time-independent cont_diff ODEs have solutions in an open interval. Comments welcome!

[Junyan Xu]

You might as well make is_picard_lindelof a structure; it will not be a Prop but you can wrap a nonempty around it. The main advantage would be that when filling in the is_picard_lindelof hypothesis, people can be clear about which condition they're proving by using the { field := proof, ... } syntax.

[Winston Yin]

Such a structure already exists, i.e. docs#picard_lindelof. Are you suggesting that the hypothesis (h : is_picard_lindelof ...) be replaced by (h : nonempty (picard_lindelof E))?

[Junyan Xu]

Oh it exists. But you can't wrap picard_lindelof inside nonempty because your conclusions use some data fields of picard_lindelof. So maybe define is_picard_lindelof as a structure and have picard_lindelof extend it?

[Junyan Xu]

No, extends is not correct way to do it, you need to state that to_fun, t_min, t₀, t_max, x₀ satisfy the nonempty (is_picard_lindelof _ _ _ _ _) predicate. Also beware that t₀, C, R have different types in docs#exists_forall_deriv_within_Icc_eq_of_lipschitz_of_continuous than in docs#picard_lindelof.

[Winston Yin]

Also beware that t₀, C, R have different types in docs#exists_forall_deriv_within_Icc_eq_of_lipschitz_of_continuous than in docs#picard_lindelof.

Yes, for is_picard_lindelof I've followed the typing in docs#exists_forall_deriv_within_Icc_eq_of_lipschitz_of_continuous.

[Winston Yin]

is_picard_lindelof as a structure would include fields L, C, R, yes? Don't we run into the same problem that we cannot satisfy the L field by obtaining a Lipschitz constant L from some ∃ L?

[Winston Yin]

What I mean is, when the goal is ℝ for, say, the Lipschitz constant, we want to get it from a theorem like cont_diff_at.exists_lipschitz_on_with, but Lean wouldn't allow me to do obtain ⟨L, ...⟩ := cont_diff_at.exists_lipschitz_on_with because the goal is not a Prop.

[Winston Yin]

So in terms of user experience, when I see a goal like nonempty (is_picard_lindelof ...), I'd be first tempted to do:

⟨{ L := begin ... end,
  R := begin ... end,
  C := begin ... end,
  etc }⟩

and I'd run into the problem with Exists.elim into a non-Prop goal. On the other hand, if I state is_picard_lindelof as one predicate, I'd be more inclined to construct the L, C, R first, then do refine ⟨L, C, R, _⟩, naturally avoiding this problem.

[Winston Yin]

Would somebody be interested to review this PR (#16348)? It's got some review on the style but still needs comments on the maths.

[Moritz Doll]

I'll try to find some time to look into it. Fyi there is a dedicated PR reviews stream which is better suited for pinging PRs

[Winston Yin]

I didn’t know that! Thanks