Antiderivative of ODE

Stream: new members

[Max Bobbin]

I've been working on a lean file where I prove the antiderivative for a bunch of functions, here is the topic , and I'm at the point where I want to do analytical solutions to ODEs. I wanted to start with the simple case of y' = y, but I found that the general solution algorithm that the other antiderivative proofs followed isn't enough for this. Any suggestions are appreciated.

Here is the set-up that I had for y' = y

theorem anti_deriv_self
{k: ℝ}
(f : ℝ → ℝ)
(hf : ∀ x, has_deriv_at f (k*(f x)) x) :
(f = λ x, (f 0)*real.exp(k*x)) :=

[Heather Macbeth]

@Max Bobbin

import analysis.special_functions.exp_deriv

theorem anti_deriv_self
  {k: ℝ}
  (f : ℝ → ℝ)
  (hf : ∀ x, has_deriv_at f (k*(f x)) x) :
  (f = λ x, (f 0)*real.exp(k*x)) :=
begin
  have : ∀ x, has_deriv_at (λ x, real.exp (- k * x) * f x) 0 x,
  { intros x,
    convert (has_deriv_at_mul_const k).neg.exp.mul (hf x),
    { ext x,
      ring_nf },
    { ring_nf } },
  ext x,
  have hx : 0 ≤ x := sorry, -- need another variant of MVT working with right endpoints
  have : real.exp (-k * x) * f x = f 0,
  { convert @constant_of_has_deriv_right_zero _ _ _ _ 0 x _ (λ y hy, (this y).has_deriv_within_at) x _,
    { simp },
    { intros x hx,
      exact (this x).continuous_at.continuous_within_at },
    { rw set.right_mem_Icc,
      exact hx } },
  convert congr_arg ((*) (real.exp (k * x))) this using 1,
  { rw [← mul_assoc, ← real.exp_add],
    ring_nf,
    simp },
  { ring }
end

[Heather Macbeth]

The tool here is docs#constant_of_has_deriv_right_zero, that a function with zero derivative is constant. But this exercise reveals that some variants of that theorem are missing from the library. There should be a version where the conclusion is equality with the right rather than left endpoint of the interval (needed for the case x ≤ 0), and there should be a version assuming has_deriv_at rather than continuous_within_at + has_deriv_within_at. Feel free to add these to the library!

[Heather Macbeth]

Here's the most commonly used special case, which should be its own lemma and which would clean up the proof above quite a bit:

theorem constant_of_has_deriv_right_zero' {E : Type u_1} [normed_group E] [normed_space ℝ E]
  {f : ℝ → E} {a b : ℝ} (hderiv : ∀ (x : ℝ), x ∈ set.Icc a b → has_deriv_at f 0 x) (h : a ≤ b) :
  f b = f a :=
sorry

[Max Bobbin]

@Heather Macbeth Thank you! This is helpful! I will use this and update this thread with what I achieve

[Max Bobbin]

what does the "@" symbol do for the proof?

[Violeta Hernández]

Makes all arguments explicit

[Max Bobbin]

Ah ok, thank you!