Fundamental Theorem of Calculus

Stream: new members

[Benjamin]

Out of curiosity, what work remains to be done in Lean to prove the second FTC? Is it something a Lean beginner could help with? I'm also curious about related calculus theorems like Taylor's theorem.

[Johan Commelin]

I think @Yury G. Kudryashov recently said that it was not too hard. But I guess it helps if you have some experience with the library.

[Patrick Massot]

It's not too hard if you put enough assumptions. If you assume that $f'$ is continuous then $\int_a^b f'(t)\,dt = f(b) - f(a)$ can be deduced from what we already have.

[Yury G. Kudryashov]

Here is a sketch of the proof of the "easy" version from @Heather Macbeth :

[Yury G. Kudryashov]

The easy version of FTC-2 would go like this, right?

• docs#norm_image_sub_le_of_norm_deriv_le_segment' to prove, under appropriate hypotheses,

theorem constant_of_deriv_zero
  (hf : ∀ x ∈ Icc a b, has_deriv_within_at F 0 (Icc a b) x) :
  ∀ x ∈ Icc a b, F x = F a := sorry

theorem eq_of_deriv_eq {f : ℝ → E}
  (hF₁ : ∀ x ∈ Icc a b, has_deriv_within_at F₁ (f x) (Icc a b) x)
  (hF₂ : ∀ x ∈ Icc a b, has_deriv_within_at F₂ (f x) (Icc a b) x)
  (h_init : F₁ a = F₂ a) :
  ∀ x ∈ Icc a b, F₁ x = F₂ x := sorry

• given F₁ which is 1x continuously differentiable, let f be its derivative, introduce F₂ satisfying

F₂ u = F₁ a + ∫ x in a..u, f x,

apply docs#integral_has_deriv_at_right to prove that F₂ has derivative f

• conclude that F₁ = F₂, i.e., F₁ a - F₁ u = ∫ x in a..u, f x.

[Yury G. Kudryashov]

(deleted)

[Yury G. Kudryashov]

(deleted)

[Yury G. Kudryashov]

Feel free to implement this plan.

[Yury G. Kudryashov]

It's important to assume only right differentiability and right continuity if we want this theorem to work without modifications for piecewise smooth functions (e.g., for contour integrals along polygonal curves).

[Heather Macbeth]

Possible collaborators -- @Benjamin Davidson was asking me about this the other day, and @Anatole Dedecker might be interested too.

[Benjamin]

When you say weak version, does that mean the strongest version is out of reach for now?

[Yury G. Kudryashov]

I think that the weak version can be done in 1-2 evenings. The strongest version can be done but it will require much more time.

[Yury G. Kudryashov]

Also I think that we should have constant_of_right_deriv_zero and eq_of_right_deriv_eq in mathlib anyway.

[Yury G. Kudryashov]

(together with deriv_within (Icc a b) versions)

[Benjamin Davidson]

I was just working on this the other day! I'd be up to collaborating with anyone else who is interested in this

[Yury G. Kudryashov]

And once you have these theorems, FTC-2 a few lines of code away.

[Benjamin Davidson]

I modified what I had already done to follow Heather's sketch. Note that the proof depends on constant_of_right_deriv_zero, which remains unproven , and which I modified so that its goal is now for x ∈ Ico a b, not Icc. I copied and pasted all the variables declared throughout measure_theory.interval_integral.

import measure_theory.interval_integral
noncomputable theory
open topological_space (second_countable_topology)
open measure_theory set classical filter
open continuous_linear_map (fst snd smul_right sub_apply smul_right_apply coe_fst' coe_snd' map_sub)
open_locale classical topological_space filter

namespace interval_integral

variables {α β 𝕜 E F : Type*} [decidable_linear_order α] [measurable_space α] [measurable_space E] [normed_group E]
variables [second_countable_topology E] [complete_space E] [normed_space ℝ E] [borel_space E]
variables {f : ℝ → E} {c ca cb : E} {l l' la la' lb lb' : filter ℝ} {lt : filter β}
  {a b z : ℝ} {u v ua ub va vb : β → ℝ}

theorem constant_of_right_deriv_zero
  (hf : ∀ x ∈ Ico a b, has_deriv_within_at f 0 (Ioi x) x) :
  ∀ x ∈ Icc a b, f x = f a :=
sorry

theorem eq_of_right_deriv_eq {f' g : ℝ → E} (x ∈ Ico a b)
  (hf : has_deriv_within_at f (f' x) (Ioi x) x)
  (hg :  has_deriv_within_at g (f' x) (Ioi x) x)
  (h_init : f a = g a) :
  f x = g x :=
sorry

theorem has_deriv_at_right_integrable {y ∈ Ico a b} [FTC_filter y (𝓝[Ioi y] y) (𝓝[Ioi y] y)]
  {f' : ℝ → E}
  (hderiv : has_deriv_within_at f (f' y) (Ioi y) y)
  (hcont : continuous_within_at f' (Ioi y) y)
  (hintg : interval_integrable f' volume a y) :
  ∫ x in a..y, f' x = f y - f a :=
by rw [eq_of_right_deriv_eq y H hderiv
        ((integral_has_deriv_within_at_right hintg hcont).const_add (f a)) (by simp),
      add_sub_cancel']

end interval_integral

[Yury G. Kudryashov]

You shouldn't assume [FTC_filter ...]. You should use one of the available instances instead.

[Yury G. Kudryashov]

I suggest that you start with constant_of_right_deriv_zero and eq_of_right_deriv_eq because right now their declared types are unprovable.

[Yury G. Kudryashov]

The types miss some quantifiers and possibly more assumptions.

[Benjamin Davidson]

Yury G. Kudryashov said:

You shouldn't assume [FTC_filter ...]. You should use one of the available instances instead.

What are the available instances?

[Benjamin Davidson]

I think I figured out what you meant about constant_of_right_deriv_zero.

theorem constant_of_right_deriv_zero (hcont : continuous_on f (Icc a b))
  (hderiv : ∀ x ∈ Ico a b, has_deriv_within_at f 0 (Ioi x) x) :
  ∀ x ∈ Icc a b, f x = f a :=
by simpa only [zero_mul, norm_le_zero_iff, sub_eq_zero] using
  λ x hx, norm_image_sub_le_of_norm_deriv_right_le_segment
    hcont hderiv (λ y hy, by rw norm_le_zero_iff) x hx

[Yury G. Kudryashov]

Benjamin Davidson said:

Yury G. Kudryashov said:

You shouldn't assume [FTC_filter ...]. You should use one of the available instances instead.

What are the available instances?

docs#interval_integral.FTC_filter

[Yury G. Kudryashov]

There are four instances: (a, pure a, ⊥), (a, 𝓝[Ici a], 𝓝[Ioi a]), (a, 𝓝[Iic a], 𝓝[Iic a]), and (a, 𝓝 a, 𝓝 a).

[Benjamin Davidson]

Hmm... I'm not totally sure how to do that but I'll try to see if I can figure it out.

Does the proof for constant_of_right_deriv_zero look okay?

[Yury G. Kudryashov]

Benjamin Davidson said:

Hmm... I'm not totally sure how to do that but I'll try to see if I can figure it out.

Does the proof for constant_of_right_deriv_zero look okay?

1. If you apply interval_integral.integral_has_deriv_within_at_right then it should figure out t based on s automatically.

2. Yes, the proof of constant_of_right_deriv_zero looks okay.

[Benjamin Davidson]

@Yury G. Kudryashov Update: Right now I can get it to work if I swap Ioi for Ici in a couple of places. I'm not sure if that's permissible, but regardless I'm trying to assess if I can do it without making those changes.

[Yury G. Kudryashov]

It's OK

[Yury G. Kudryashov]

In many cases statements with Ioi and Ici are equivalent.

[Benjamin Davidson]

Okay, that's what I figured. I was trying to see if I could derive (for example) has_deriv_within_at f (f' y) t y from has_deriv_within_at f (f' y) s y given s ⊆ t but have not been successful.

[Yury G. Kudryashov]

The implication goes in the other direction.

[Yury G. Kudryashov]

However, has_deriv_within_at f f' (Ici x) x is equivalent to has_deriv_within_at f f' (Ioi x) x.

[Yury G. Kudryashov]

I added those Ioi x theorems to mean_value.lean but now I think that I was wrong, and we should use Ici x. I don't expect that you will do the migration. Just use Ici x whenever it's more convenient for you.

[Yury G. Kudryashov]

If you need this equivalence, then you can leave sorry in your PR, and I'll fill it in.

[Benjamin Davidson]

Got it, thanks!!

[Benjamin Davidson]

#4945 (work in progress)

[Ramon Fernandez Mir]

Hello @Benjamin Davidson and @Yury G. Kudryashov . Are you currently working on the second part of FTC? I saw that there's a branch with some progress. I realised that I needed it to prove something else and I ended up stuck in the same place! Namely showing something along the lines:

-- ⊢ continuous_on (λ (x : ℝ), (∫ (y : ℝ) in a..x, f' y) + f a) (Icc a b)

I believe it should more or less follow from is_compact.exists_forall_ge and a few lemmas about interval_integral. In any case, I'd be happy to help so let me know if you have a plan :-)

[Yury G. Kudryashov]

Actually, we know that the integral of a continuous function is differentiable, not only continuous.

[Yury G. Kudryashov]

My plan was to give new users another week or two to make a PR, then do it myself if it will not be done yet.

[Benjamin Davidson]

@Ramon Fernandez Mir @Yury G. Kudryashov Sorry it's been taking me so long, I've gotten stuck on a couple of parts of it and have been trying to figure them out but to no avail as of yet. I did manage to fix some of it, though, so I'll push those changes now so that you can see them. I would definitely appreciate some assistance with the remaining pieces.

[Yury G. Kudryashov]

If you have some specific questions, ask them here, please.