Indeterminate Integral

Stream: Is there code for X?

[Max Bobbin]

I was wondering if there is a way to take an indeterminate integral of a single-variable function. I was trying to work backwards from the derivative of a function and show that if a function has this as its derivative, the function must be this, for example:

import data.real.basic
import analysis.calculus.deriv

example
(f f' : ℝ → ℝ)
(hf : ∀ x, has_deriv_at f (f' x) x)
(hf' : f' = λ x, 2*x)
:
∀(C:ℝ), f = λ x, x^2 + C
:=
begin

end

I was trying to prove it by contradiction, but I couldn't quite figure it out.

[Eric Wieser]

The statement is false; I think you meant "exists" not "forall"

[Max Bobbin]

Ok, my bad, I was thinking it would be for any constant C, because it is true that x^2 +2 and x^2 +3 both have the derivative 2*x

[Max Bobbin]

With changing the statement to exists, where would I start with proving this? I'm having trouble finding a way to do an antiderivative in Lean

[Mauricio Collares]

Something using docs#is_const_of_deriv_eq_zero applied to λ x, f x - x^2?

[Max Bobbin]

I made progress with that, and I think its the right track, but I ran into an illogical argument. While going through, I ended with a goal of f x - x^2 = f x, which implies that x^2 = 0.

import data.real.basic
import analysis.calculus.deriv
import analysis.calculus.mean_value


example
(f f' : ℝ → ℝ) {x y :ℝ}
(hf : ∀ x, has_deriv_at f (f' x) x)
(hf' : f' = λ x, 2*x)
:
f = λ x, x^2
:=
begin
have h1: (λ x, f x - x^2) x = (λ x, f x - x^2) y,
apply is_const_of_deriv_eq_zero,
rw differentiable,
intro x,
specialize hf x,
apply has_deriv_at.differentiable_at,
convert hf,
funext,

end

[Max Bobbin]

nvm, I think I fixed it

[Eric Rodriguez]

you can certainly get to an unprovable proof state from a true statement

[Max Bobbin]

Yea, I see that. I've made progress. Currently I have the statement

has_deriv_at (λ (x : ℝ), x ^ 2) ?m_1 x

I feel like I should be able to prove this without having to write this as a premise, I was looking around the special function tab and trying to see if there was a lemma for this

[Max Bobbin]

wait, I was overthinking it. Its just has_deriv_at.pow :laughing:

[Mauricio Collares]

Eric Rodriguez said:

you can certainly get to an unprovable proof state from a true statement

But in this case the statement is not true, I think (the conclusion should be ∃(C:ℝ), f = λ x, x^2 + C)

[Mauricio Collares]

A very ugly version:

import data.real.basic
import analysis.calculus.deriv
import analysis.calculus.mean_value

example
(f f' : ℝ → ℝ)
(hf : ∀ x, has_deriv_at f (f' x) x)
(hf' : f' = λ x, 2*x)
:
∃(C:ℝ), f = λ x, x^2 + C
:=
begin
  have h1 : ∀ (x y : ℝ), (λ x, f x - x^2) x = (λ x, f x - x^2) y,
  { apply is_const_of_deriv_eq_zero,
    { apply differentiable.add,
      { intro x, exact (hf x).differentiable_at },
      { simp }},
    { intro x,
      rw [deriv_sub, sub_eq_zero],
      { simpa [hf'] using (hf x).deriv },
      { exact (hf x).differentiable_at },
      { simp }}},
  use f 0,
  ext z,
  specialize h1 z 0,
  simp at h1,
  linarith,
end

[Max Bobbin]

Thank you! I was almost there but got stuck, realized I needed my have statement to be forall. I was using lambda function. Thank you for the help!