What's the correct way to talk about indefinite integrals?

Stream: new members

[Ilmārs Cīrulis]

For example, I want to say that indefinite integral of 2 * x is x ^ 2 + C.
What's the correct way to formulate such statement?

Thank you!

[Kenny Lau]

@Ilmārs Cīrulis The Fundamental Theorem of Calculus in Lean is:

theorem integral_deriv_eq_sub' (f) (hderiv : deriv f = f')
    (hdiff : ∀ x ∈ uIcc a b, DifferentiableAt ℝ f x) (hcont : ContinuousOn f' (uIcc a b)) :
    ∫ y in a..b, f' y = f b - f a

[Kenny Lau]

so I think the statement you want will be that the derivative of x^2 is 2*x

[Kenny Lau]

import Mathlib

lemma foo (c : ℝ) : deriv (fun x : ℝ ↦ (x ^ 2 : ℝ)) c = 2 * c := by simp
lemma foo' : deriv (fun x : ℝ ↦ (x ^ 2 : ℝ)) = (fun c ↦ 2 * c) := by simp
lemma foo'' : deriv (· ^ 2 : ℝ → ℝ) = (2 * ·) := by simp

[ZhiKai Pong]

Ilmārs Cīrulis said:

For example, I want to say that indefinite integral of 2 * x is x ^ 2 + C.
What's the correct way to formulate such statement?

Thank you!

If you need the + C explicitly, I asked something similar in #new members > equality of derivatives

tldr: use docs#is_const_of_deriv_eq_zero