## Stream: new members

### Topic: Fundamental Theorem of Calculus

#### Benjamin (Nov 02 2020 at 17:45):

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 (Nov 02 2020 at 17:55):

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 (Nov 02 2020 at 18:51):

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 (Nov 03 2020 at 00:17):

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

#### Yury G. Kudryashov (Nov 03 2020 at 00:17):

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

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.

(deleted)

(deleted)

#### Yury G. Kudryashov (Nov 03 2020 at 00:27):

Feel free to implement this plan.

#### Yury G. Kudryashov (Nov 03 2020 at 00:28):

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).

#### Benjamin (Nov 03 2020 at 00:37):

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

#### Yury G. Kudryashov (Nov 03 2020 at 01:02):

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 (Nov 03 2020 at 01:04):

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

#### Yury G. Kudryashov (Nov 03 2020 at 01:05):

(together with deriv_within (Icc a b) versions)

#### Benjamin Davidson (Nov 03 2020 at 01:06):

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 (Nov 03 2020 at 01:06):

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

#### Benjamin Davidson (Nov 03 2020 at 05:06):

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),

end interval_integral

#### Yury G. Kudryashov (Nov 03 2020 at 06:12):

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

#### Yury G. Kudryashov (Nov 03 2020 at 06:15):

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 (Nov 03 2020 at 06:16):

The types miss some quantifiers and possibly more assumptions.

#### Benjamin Davidson (Nov 03 2020 at 06:46):

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 (Nov 03 2020 at 08:34):

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 (Nov 03 2020 at 12:00):

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 (Nov 03 2020 at 12:00):

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

#### Benjamin Davidson (Nov 03 2020 at 19:53):

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 (Nov 04 2020 at 00:58):

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 (Nov 04 2020 at 17:08):

@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.

It's OK

#### Yury G. Kudryashov (Nov 04 2020 at 21:35):

In many cases statements with Ioi and Ici are equivalent.

#### Benjamin Davidson (Nov 04 2020 at 22:14):

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 (Nov 05 2020 at 03:10):

The implication goes in the other direction.

#### Yury G. Kudryashov (Nov 05 2020 at 03:12):

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 (Nov 05 2020 at 03:13):

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 (Nov 05 2020 at 03:17):

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

Got it, thanks!!

#### Benjamin Davidson (Nov 08 2020 at 08:38):

#4945 (work in progress)

#### Ramon Fernandez Mir (Dec 08 2020 at 17:43):

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 (Dec 08 2020 at 19:08):

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

#### Yury G. Kudryashov (Dec 08 2020 at 19:09):

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 (Dec 09 2020 at 07:39):

@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.