Using FTC for a function which is continuous on a subset

Stream: new members

[Michael Novak]

I work with a function defined on an interval and also continuous there, since I will also want to work with derivatives of this function, as I understood it, in lean you should define it on the entire real line (with meaningless values outside the interval), because an interval is not a normed-space so the derivative definition doesn't work for it. Now I want use the first part of the Fundamental Theorem of Calculus on the integral of this function over a closed interval which is a subset of the interval that the function is continuous on. In the Math in Lean text they show how to do this when the function is continuous on all the real line. I tried to find similar theorems for ContinuousOn, but they didn't work. I don't know much Measure theory, so I don't know exactly which modification I need to make. I would appreciate if you could explain me what I should do.

[Aaron Liu]

can you write down the theorem statement you want?

[Michael Novak]

I can, but there will probably be a bit too much irrelevant details to the general problem. Do you still want me to send it?

[Michael Rothgang]

From your message, it's not clear what exactly your problem is --- what statement are you looking, which ones did you look at, why did they "not work". I cannot help you this abstractly; please give us something to work on.

[Michael Rothgang]

Of course, if you can abstract the lemma you want to apply from your application, that is also nice. But even saying "this is my motivating application, this lemma would solve it, here's where I'm stuck trying to prove it" would make it possible to help you.

[Michael Rothgang]

In general, there should be a version of FTC on a subset, and I'd be surprised if mathlib doesn't have it already.

[Michael Novak]

So I've written the idea of what I want to do in a more general settings, the problem is in the last line, where I don't really use the correct theorems:

import Mathlib

open MeasureTheory intervalIntegral

theorem the_idea {I : Set ℝ} [I.OrdConnected] {f : ℝ → ℝ} (h : ContinuousOn f I) (x₀ x : I) :
    deriv (fun t ↦  ∫ τ in x₀..t, f t) x = f x :=
  have cont_on_subinterval : ContinuousOn f (Set.uIcc x₀ x) := by
    have h' : (Set.uIcc x₀ x : Set ℝ) ⊆ I := by
      apply (I.ordConnected_iff_uIcc_subset_left x₀.mem).mp (by assumption) x.mem
    exact h.mono h'
  integral_hasStrictDerivAt_right cont_on_subinterval.intervalIntegrable
    (cont_on_subinterval.stronglyMeasurableAtFilter_nhdsWithin _ _) h.continuousAt.hasDerivAt.deriv
   sorry

[Kevin Buzzard]

This code doesn't compile (at least on the web editor). If your question is "how do I prove x" then it's probably better to post code with a sorry rather than with errors (code with errors is always confusing, at least for me). (but I confess I am not really following the thread caefully)

[Michael Novak]

Kevin Buzzard said:

This code doesn't compile (at least on the web editor). If your question is "how do I prove x" then it's probably better to post code with a sorry rather than with errors (code with errors is always confusing, at least for me). (but I confess I am not really following the thread caefully)

Is it o.k how I added the sorry now? The reason I added the work in progress proof is that I wanted to show what I tried to do so far.

[Aaron Liu]

there's errors before the sorry

[Kevin Buzzard]

I don't know anything about this part of the library but I do understand the errors in the code you're posting:

Application type mismatch: The argument
  ContinuousOn.stronglyMeasurableAtFilter_nhdsWithin cont_on_subinterval ?m.56 ?m.57
has type
  StronglyMeasurableAtFilter f (nhdsWithin ?m.57 (Set.uIcc ↑x₀ ↑x)) ?m.55
but is expected to have type
  StronglyMeasurableAtFilter f (nhds ↑x) volume

means "you made a term of type StronglyMeasurableAtFilter (the wrong filter)" and

Invalid field `hasDerivAt`: The environment does not contain `Function.hasDerivAt`
  ContinuousOn.continuousAt h
has type
  I ∈ nhds ?m.64 → ContinuousAt f ?m.64

means "you wrote (something which is a function).hasDerivAt and that makes no sense".

If you're stuck then post code with no errors. That's much better than posting code with errors.

[Michael Novak]

Kevin Buzzard said:

I don't know anything about this part of the library but I do understand the errors in the code you're posting:

Application type mismatch: The argument
  ContinuousOn.stronglyMeasurableAtFilter_nhdsWithin cont_on_subinterval ?m.56 ?m.57
has type
  StronglyMeasurableAtFilter f (nhdsWithin ?m.57 (Set.uIcc ↑x₀ ↑x)) ?m.55
but is expected to have type
  StronglyMeasurableAtFilter f (nhds ↑x) volume

means "you gave StronglyMeasurableAtFilter the wrong filter" and

Invalid field `hasDerivAt`: The environment does not contain `Function.hasDerivAt`
  ContinuousOn.continuousAt h
has type
  I ∈ nhds ?m.64 → ContinuousAt f ?m.64

means "you wrote something.hasDerivAt and that makes no sense"

I honestly don't know how to use this theorem, because I didn't learn measure theory yet. I just tried to do something analogous to how this was used in the Math in Lean text. So, my question in a nutshell is how to use this theorem in my case? What are the correct parameters?

[Michael Novak]

If it's more helpful to just send the theorem statement without anything I tried, then here it is:

import Mathlib

open MeasureTheory intervalIntegral

theorem the_idea {I : Set ℝ} [I.OrdConnected] {f : ℝ → ℝ} (h : ContinuousOn f I) (x₀ x : I) :
    deriv (fun t ↦  ∫ τ in x₀..t, f τ) x = f x := sorry

[Kevin Buzzard]

Michael Novak said:

So, my question in a nutshell is how to use this theorem in my case?

Again let me stress that I don't know this part of the library at all. But my understanding of your question in a nutshell is that it is: "I have a goal of the form A = B. How do I apply a theorem whose conclusion is HasStrictDerivAt (something) to close this goal?" and so my answer is "you can't do that, because the conclusion of the theorem you want to use to close the goal is not of the form A = B".

[Aaron Liu]

I think you wrote it wrong

[Aaron Liu]

you put ∫ τ in x₀..t, f t but it should be ∫ τ in x₀..t, f τ

[Michael Novak]

Aaron Liu said:

you put ∫ τ in x₀..t, f t but it should be ∫ τ in x₀..t, f τ

Yes, you are right, thank you. Although it doesn't solve the problem.

[Michael Novak]

Just in case it will be useful for someone, here is how they do it in the Math in Lean text for a function which is continuous on the entire real line:

example (f : ℝ → ℝ) (hf : Continuous f) (a b : ℝ) : deriv (fun u ↦ ∫ x : ℝ in a..u, f x) b = f b :=
  (integral_hasStrictDerivAt_right (hf.intervalIntegrable _ _) (hf.stronglyMeasurableAtFilter _ _)
        hf.continuousAt).hasDerivAt.deriv

[Aaron Liu]

so you don't have enough assumptions

[Aaron Liu]

to conclude the conclusion

[Michael Novak]

Aaron Liu said:

so you don't have enough assumptions

Could you explain what do you mean in more detail?

[Kevin Buzzard]

And also the brackets are different in the MIL version, which makes all the difference. In the MIL version they use the theorem to get HasStrictDerivAt (something) , and then they apply HasStrictDerivAt.hasDerivAt etc. So one of your problems is that you haven't correctly parsed what's going on in MIL and so have failed to replicate it. Do you understand dot notation?

[Michael Novak]

Kevin Buzzard said:

And also the brackets are different in the MIL version, which makes all the difference. In the MIL version they use the theorem to get HasStrictDerivAt (something) , and then they apply HasStrictDerivAt.hasDerivAt etc. So one of your problems is that you haven't correctly parsed what's going on in MIL and so have failed to replicate it. Do you understand dot notation?

Yes, you are absolutely right, Thank you!. I only noticed this now. I'll try to see if this solve the issue.

[Aaron Liu]

Michael Novak said:

Aaron Liu said:

so you don't have enough assumptions

Could you explain what do you mean in more detail?

I have a function f := fun τ => if τ > 0 then 1 else -1 (= a step function) and an interval I := Set.Iic 0 (= the nonpositive reals) that f is continuous on the interval and a points x₀ = x = 0 in the interval but the derivative of the integral is not consistent with the theorem statement

[Aaron Liu]

since we're not differentiable at zero the deriv gives a junk value of 0

[Aaron Liu]

but f x = -1

[Kevin Buzzard]

Here is another way of writing the MIL proof, where I unravel some of the dot notation.

example (f : ℝ → ℝ) (hf : Continuous f) (a b : ℝ) : deriv (fun u ↦ ∫ x : ℝ in a..u, f x) b = f b := by
  apply HasDerivAt.deriv
  apply HasStrictDerivAt.hasDerivAt
  exact (integral_hasStrictDerivAt_right (hf.intervalIntegrable _ _) (hf.stronglyMeasurableAtFilter _ _) hf.continuousAt)

Let X be (integral_hasStrictDerivAt_right (hf.intervalIntegrable _ _) (hf.stronglyMeasurableAtFilter _ _) hf.continuousAt). The point is that the type of X is HasStrictDerivAt (something) so X.hasDerivAt means HasStrictDerivAt.hasDerivAt X, which has type HasDerivAt (something) etc etc.

[Michael Novak]

Aaron Liu said:

Michael Novak said:

Aaron Liu said:

so you don't have enough assumptions

Could you explain what do you mean in more detail?

I have a function f := if x > 0 then 1 else -1 (= a step function) and an interval Set.Iic 0 (= the nonpositive reals) that f is continuous on the interval and a points x₀ = x = 0 in the interval but the derivative of the integral is not consistent with the theorem statement

I see what you are saying. If I know that the function is continuously differentiable on the interval will it help? And in general how do we solve this issue? Because it seems like this only happens because we can't just define differentiable functions on subsets (or even just intervals) and we have to define the function on the entire real line. It seems like more of an issue of how we try to represent the function in lean, isn't it?

[Aaron Liu]

but this function f is continuously differentiable on the interval

[Aaron Liu]

so the problem is you're trying to take properties of the function on the interval into a derivative that can reach off the interval

[Aaron Liu]

so how about saying you have a derivative on the interval instead with docs#HasDerivWithinAt

[Kevin Buzzard]

Yes, if you're working with functions and you only care about their values on a subset then you need to restrict your entire application of calculus to the subset (and there are tools to do this).

[Michael Novak]

Aaron Liu said:

but this function f is continuously differentiable on the interval

It's probably not an important point, but why is it continuously differentiable? We only assumed it is continuous

[Aaron Liu]

the counterexample I gave

[Aaron Liu]

it's constant (=> continuously differentiable) on the interval

[Michael Novak]

Aaron Liu said:

the counterexample I gave

Oh, got you

[Kevin Buzzard]

This error from above

Application type mismatch: The argument
  ContinuousOn.stronglyMeasurableAtFilter_nhdsWithin cont_on_subinterval ?m.56 ?m.57
has type
  StronglyMeasurableAtFilter f (nhdsWithin ?m.57 (Set.uIcc ↑x₀ ↑x)) ?m.55
but is expected to have type
  StronglyMeasurableAtFilter f (nhds ↑x) volume

means "you're asking questions about neighbourhoods of x which might not be fully contained within the subset and these questions cannot be sensible in your context" (for example neighbourhoods of the form $(-\epsilon,\epsilon)$ in Aaron's example).

[Michael Novak]

I think I understand the issue, but I'm just too unfamiliar with the jargon of of measure theory, so it might take me a bit of a long time to understand exactly how to use derivative within a subset here. If by chance it's already clear to you what to do, I would really appreciate if you could tell me, but if not, it's totally fine, I'll try to work a bit and see if I can figure it out.

[Aaron Liu]

basically don't do theorem statements that look like deriv f x = f' x

[Aaron Liu]

instead you want to write stuff that looks like HasDerivWithinAt f (f' x) I x

[Michael Novak]

Aaron Liu said:

instead you want to write stuff that looks like HasDerivWithinAt f f' I x

Oh really? That seems quite annoying. Is that normal in Mathlib? Is there a plan to make it possible to work with differentiable functions on subsets of normed spaces, so we don't have to dill with this? And also thank you very much for the help, I'm obviously not angry at you that this has to work like that.

[Aaron Liu]

I feel like this is normal in mathlib

[Aaron Liu]

why do you say it is annoying

[Michael Novak]

Ideally I would like to be able to just define my function on the interval and just use normal deriv, like in a textbook.

[Aaron Liu]

in textbook we say a function has a derivative if it satisfies ...
and by abuse of language we can say the derivative of a function is equal to a value if it has that derivative (since derivatives are unique)

[Kevin Buzzard]

But it's not normal deriv. Normal deriv means (f(x+h)-f(x))/h where h tends to zero and is allowed to take positive and negative values when doing so. That's what normal derivative means. So if you have a function on [0,1] and you want to talk about it being differentiable at 1 then you really are not using the normal derivative. Formalisation cares about these details, even if your textbook doesn't.

[Michael Novak]

Kevin Buzzard said:

But it's not normal deriv. Normal deriv means (f(x+h)-f(x))/h where h tends to zero and is allowed to take positive and negative values when doing so. That's what normal derivative means. So if you have a function on [0,1] and you want to talk about it being differentiable at 1 then you really are not using the normal derivative. Formalisation cares about these details, even if your textbook doesn't.

But in the textbook definition (at least how I learned it) you also have the demand that x+h is in the interval. Just like (0.5, 1] is not an open ball with center 1 in the real line, but it is an open ball with center 1 inside [0, 1].

[Kevin Buzzard]

Right, and that's called HasDerivWithin because you are demanding that you are within the interval, so it's not the same as HasDeriv (which doesn't)

[Aaron Liu]

Kevin Buzzard said:

Right, and that's called HasDerivWithin

Not quite, we have HasDerivWithinAt but I didn't find HasDerivWithin or HasDerivOn

[Michael Novak]

The new version of the theorem I'm trying to prove is:

import Mathlib

open MeasureTheory intervalIntegral

theorem the_idea {I : Set ℝ} [I.OrdConnected] {f : ℝ → ℝ}  (h : ContinuousOn f I) (x₀ x : I) :
  HasDerivWithinAt (fun t ↦  ∫ τ in x₀..t, f τ) (f x) I x := sorry

I'm trying to use integral_hasDerivWithinAt_right, but I struggle a bit to find the right parameters. If you have some hints, I would greatly appreciate it.

[Aaron Liu]

oh I think I can do this one now

[Aaron Liu]

everything's a bit more complicated because you have a convex set

[Aaron Liu]

instead of just an interval

[Michael Novak]

Aaron Liu said:

everything's a bit more complicated because you have a convex set

I proved already that the function is continuous on the subinterval. Maybe it could be helpful:

  have cont_on_subinterval : ContinuousOn f (Set.uIcc x₀ x) := by
    have h' : (Set.uIcc x₀ x : Set ℝ) ⊆ I := by
      apply (I.ordConnected_iff_uIcc_subset_left x₀.mem).mp (by assumption) x.mem
    exact h.mono h'

[Aaron Liu]

I did it!

import Mathlib

open MeasureTheory intervalIntegral

theorem the_idea {I : Set ℝ} [I.OrdConnected] {f : ℝ → ℝ} (h : ContinuousOn f I) (x₀ x : I) :
    HasDerivWithinAt (fun t ↦ ∫ τ in x₀..t, f τ) (f x) I x :=
  have : intervalIntegral.FTCFilter x (nhdsWithin x I) (nhdsWithin x I) := by
    refine @intervalIntegral.FTCFilter.mk x (nhdsWithin x I) (nhdsWithin x I) ⟨?_⟩ ?_ ?_ ?_
    · rw [Filter.tendsto_smallSets_iff]
      intro t ht
      rw [mem_nhdsWithin_iff_exists_mem_nhds_inter] at ht
      obtain ⟨u, hu, hut⟩ := ht
      obtain ⟨a, b, haxb, habx, habu⟩ := exists_Icc_mem_subset_of_mem_nhds hu
      have hab : Set.Icc a b ∩ I ∈ nhdsWithin x.1 I := Set.inter_comm _ _ ▸ inter_mem_nhdsWithin I habx
      filter_upwards [Filter.prod_mem_prod hab hab] with (i, j) ⟨hi, hj⟩
      refine subset_trans (Set.subset_inter ?_ ?_) hut
      · refine subset_trans ?_ habu
        intro k hk
        exact ⟨hi.1.1.trans hk.1.le, hk.2.trans hj.1.2⟩
      · intro k hk
        exact Set.Icc_subset I hi.2 hj.2 (Set.Ioc_subset_Icc_self hk)
    · exact pure_le_nhdsWithin x.2
    · exact nhdsWithin_le_nhds
    · exact @Filter.inf_isMeasurablyGenerated _ _ _ _ _ (Set.OrdConnected.measurableSet ‹_›).principal_isMeasurablyGenerated
  intervalIntegral.integral_hasDerivWithinAt_right ((h.mono (Set.OrdConnected.uIcc_subset ‹_› x₀.2 x.2)).intervalIntegrable)
    (h.stronglyMeasurableAtFilter_nhdsWithin (Set.OrdConnected.measurableSet ‹_›) x) (h.continuousWithinAt x.2)

[Michael Novak]

Wow! Thank you so much! I didn't expect that something which looks like should be almost immediate will take so much work. If I was working on a normal closed interval would it be shorter? Could this theorem get into Mathlib? It seems quite useful.

[Aaron Liu]

if you were doing a closed interval

[Aaron Liu]

I think it would probably be just the last two lines