Antiderivative in Lean

Stream: general

[Max Bobbin]

I needed the antiderivative for a project I was working on in Lean, and with some help from the community, I was able to write a couple of theorems that give the antiderivative for some basic functions. I wanted to know how contributing to mathlib works and what the community thinks the naming convention should be. Here are the names I came up with:
antiderivative of a constant function: antideriv_const
antiderivative of a natural power: antideriv_pow
antiderivative of an integer power: antideriv_zpow

[Eric Wieser]

Those names look reasonable; have you read our #naming guide?

[Violeta Hernández]

Just to be really sure, the antiderivative isn't a thing in mathlib yet?

[Violeta Hernández]

And as a sidenote, how are you defining it? As a set of functions varying by a constant?

[Max Bobbin]

Eric Wieser said:

Those names look reasonable; have you read our #naming guide?

Yes, I looked through it and tried to make sure my proofs followed all the guidelines, I will of course look through it again to double check

[Max Bobbin]

Violeta Hernández said:

Just to be really sure, the antiderivative isn't a thing in mathlib yet?

I can give an example of the first one:

theorem antideriv_const
(f f' : ℝ → ℝ) (k : ℝ)
(hf : ∀ x, has_deriv_at f (f' x) x)
(hf' :  f' = λ x, k) :
(f = λ x, (k*x) + (f 0) ) :=
begin
   have h1: ∀(x y : ℝ), f x - (x*k) = f y - (y*k),
   {
    apply is_const_of_deriv_eq_zero,
    {
      rw differentiable,
      intro x,
      specialize hf x,
      apply has_deriv_at.differentiable_at,
      apply has_deriv_at.sub,
      {
        convert hf,
      },
      apply has_deriv_at_mul_const,
    },
    intro x,
    rw deriv_sub,
    rw sub_eq_zero,
    simp,
    rw has_deriv_at.deriv,
    rw hf' at hf,
    specialize hf x,
    simp at hf,
    apply hf,
    apply has_deriv_at.differentiable_at,
    specialize hf x,
    apply hf,
    simp,
  },
  ext z,
  specialize h1 z 0,
  apply eq_add_of_sub_eq',
  simp at h1,
  rw mul_comm at h1,
  exact h1,
end

[Max Bobbin]

I defined the goal to be the function plus the integrating constant (which is just the function evaluated at 0) and the hypothesises to say that f has a derivative and what that derivative is equal to

[Eric Wieser]

It's generally very uncommon to have hypotheses of the form hf : f = ... in mathlib, because the user could just rewrite by that hypothesis directly

[Max Bobbin]

Would it be better to do an implication statement instead? I don't understand what you mean by rewriting the hypothesis directly.

[Reid Barton]

theorem antideriv_const
(f : ℝ → ℝ) (k : ℝ)
(hf : ∀ x, has_deriv_at f k x) :
(f = λ x, (k*x) + (f 0) ) :=

[Max Bobbin]

Ah, ok I see what you mean. That makes more sense, I was misinterpreting. Let me change it to that

[Max Bobbin]

This is what it looks like now:

theorem antideriv_const
(f : ℝ → ℝ) (k : ℝ)
(hf : ∀ x, has_deriv_at f k x):
(f = λ x, (k*x) + (f 0) ) :=
begin
   have h1: ∀(x y : ℝ), f x - (x*k) = f y - (y*k),
   {
    apply is_const_of_deriv_eq_zero,
    {
      rw differentiable,
      intro x,
      specialize hf x,
      apply has_deriv_at.differentiable_at,
      apply has_deriv_at.sub,
      {
        convert hf,
      },
      apply has_deriv_at_mul_const,
    },
    intro x,
    rw deriv_sub,
    rw sub_eq_zero,
    simp,
    rw has_deriv_at.deriv,
    specialize hf x,
    apply hf,
    apply has_deriv_at.differentiable_at,
    specialize hf x,
    apply hf,
    simp,
  },
  ext z,
  specialize h1 z 0,
  apply eq_add_of_sub_eq',
  simp at h1,
  rw mul_comm at h1,
  exact h1,
end

[Eric Wieser]

I would imagine mathlib would like to be able to state things like "if the derivative is constant within an interval then the function is linear within that interval"; rather than requiring the derivative be constant everywhere

[Eric Wieser]

Probably there's some fderiv generalization for "connected" sets

[Eric Wieser]

The interval one could look like

theorem antideriv_const
(f : ℝ → ℝ) (a b k : ℝ)
(hf : ∀ x ∈ Icc a b, has_deriv_at f k x) (x) (hx : x ∈ Icc a b) :
f x =  (k*(x-a)) + (f a) :=

[Eric Wieser]

Someone else can likely give better advice than me here

[Max Bobbin]

That should be straight forward to prove. I think it would follow form the proof for constant everywhere

[Violeta Hernández]

You could probably generalize further to any interval

[Violeta Hernández]

Instead of a specific interval like Icc

[Johan Commelin]

Is there a docs#has_deriv_within_at ? I guess that's what you might want to use.

[Max Bobbin]

Violeta Hernández said:

You could probably generalize further to any interval

Do you mean instead of saying Icc a b, its just the derivative at x, where x is a member of a set of real numbers?