Zulip Chat Archive

Stream: new members

Topic: Fundamental Theorem of Calculus


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Nov 02 2020 at 18:51):

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

view this post on Zulip Yury G. Kudryashov (Nov 03 2020 at 00:17):

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

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Nov 03 2020 at 00:19):

(deleted)

view this post on Zulip Yury G. Kudryashov (Nov 03 2020 at 00:19):

(deleted)

view this post on Zulip Yury G. Kudryashov (Nov 03 2020 at 00:27):

Feel free to implement this plan.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Benjamin (Nov 03 2020 at 00:37):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Nov 03 2020 at 01:05):

(together with deriv_within (Icc a b) versions)

view this post on Zulip 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

view this post on Zulip Yury G. Kudryashov (Nov 03 2020 at 01:06):

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

view this post on Zulip 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

view this post on Zulip Yury G. Kudryashov (Nov 03 2020 at 06:12):

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

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Nov 03 2020 at 06:16):

The types miss some quantifiers and possibly more assumptions.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Nov 04 2020 at 21:35):

It's OK

view this post on Zulip Yury G. Kudryashov (Nov 04 2020 at 21:35):

In many cases statements with Ioi and Ici are equivalent.

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Nov 05 2020 at 03:10):

The implication goes in the other direction.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Benjamin Davidson (Nov 05 2020 at 05:53):

Got it, thanks!!

view this post on Zulip Benjamin Davidson (Nov 08 2020 at 08:38):

#4945 (work in progress)

view this post on Zulip 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 :-)

view this post on Zulip Yury G. Kudryashov (Dec 08 2020 at 19:08):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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