Zulip Chat Archive
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 FTC2 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, letf
be its derivative, introduceF₂
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 (Nov 03 2020 at 00:19):
(deleted)
Yury G. Kudryashov (Nov 03 2020 at 00:19):
(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).
Heather Macbeth (Nov 03 2020 at 00:29):
Possible collaborators  @Benjamin Davidson was asking me about this the other day, and @Anatole Dedecker might be interested too.
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 12 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, FTC2 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),
add_sub_cancel']
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?

If you
apply interval_integral.integral_has_deriv_within_at_right
then it should figure outt
based ons
automatically. 
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.
Yury G. Kudryashov (Nov 04 2020 at 21:35):
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.
Benjamin Davidson (Nov 05 2020 at 05:53):
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.
Yury G. Kudryashov (Dec 09 2020 at 15:01):
If you have some specific questions, ask them here, please.
Last updated: May 18 2021 at 17:44 UTC