Using `ContDiffOn` for partial integration

Stream: Is there code for X?

[Alex Kontorovich]

Here's a problem I'm facing. I want to apply partial integration to prove:
$\int_a^b x φ'(x) dx = b φ(b) - a φ(a) - \int_a^b φ(x) dx$
for a continuously differentiable function φ. So I would think that I should apply docs#intervalIntegral.integral_mul_deriv_eq_deriv_mul to a function satisfying ContDiffOn ℝ 1 φ [[a, b]]. The theorem requires that I use a closed interval [[a, b]] (presumably necessary because we'll be evaluating φ at a and b). I also need to know that φ has derivative deriv φ on [[a, b]], and that deriv φ is continuous on [[a, b]]. The problem is that, as far as I can tell, the assumption ContDiffOn can only tell me that HasDerivAt φ (deriv φ x) x and ContinuousOn (deriv φ) hold on the open interval $(a,b)$, which of course is not sufficient for the application. Is that really true? (And hence I shouldn't assume ContDiffOn, but just directly assume the two properties that I need, right?) Or is there a better way to use the ContDiffOn API that I'm missing? Thanks! Here's a MWE:

import Mathlib.MeasureTheory.Integral.IntegralEqImproper

open BigOperators Interval Topology Set

example {φ : ℝ → ℝ} {a b : ℝ} (a_le_b : a ≤ b)
    (φDiff : ContDiffOn ℝ 1 φ [[a, b]]) :
    ∫ (x : ℝ) in a..b, x * deriv φ x =
      b * φ b - a * φ a - ∫ (x : ℝ) in a..b, φ x := by
  -- This is for the parts below:
  have φDiff' : ContDiffOn ℝ 1 φ (Ioo a b) := by
    apply φDiff.mono
    rw [uIcc_of_le a_le_b]
    exact Ioo_subset_Icc_self

  set u := fun (x : ℝ) ↦ x
  set u' := fun (x : ℝ) ↦ (1 : ℝ)
  have hu : ∀ x ∈ [[a, b]], HasDerivAt u (u' x) x :=
    fun x _ ↦ hasDerivAt_id' x
  have hu' : IntervalIntegrable u' MeasureTheory.volume a b := by
    apply Continuous.intervalIntegrable
    continuity

  -- Can't seem to prove this:
  have derivφ : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x := by sorry
  -- I can only prove this:
  have derivφ_Open : ∀ x ∈ Ioo a b, HasDerivAt φ (deriv φ x) x := by
    intro x hx
    have x_in_s : Set.Ioo a b ∈ 𝓝 x := isOpen_Ioo.mem_nhds hx
    exact (ContDiffAt.hasStrictDerivAt (φDiff'.contDiffAt x_in_s) (by simp)).hasDerivAt
  -- Can't seem to prove this:
  have derivφCont : ContinuousOn (deriv φ) [[a, b]] := by sorry
  -- I can only prove this:
  have derivφCont' : ContinuousOn (deriv φ) (Ioo a b) := by
    apply ContDiffOn.continuousOn (𝕜 := ℝ) (n := 0)
    exact (fun h => ((contDiffOn_succ_iff_deriv_of_isOpen isOpen_Ioo).1 h).2) φDiff'

  have hv' : IntervalIntegrable (deriv φ) MeasureTheory.volume a b :=
    derivφCont.intervalIntegrable
  convert intervalIntegral.integral_mul_deriv_eq_deriv_mul hu derivφ hu' hv' using 1
  simp [u]

[Alex Kontorovich]

I suppose I could assume ContDiffOn for some open set s containing [[a, b]]...? That's probably the easiest solution?

[Jireh Loreaux]

I'm not very familiar with this end of the library, but it seems to me from a mathematical perspective that probably docs#intervalIntegral.integral_mul_deriv_eq_deriv_mul could instead take arguments hu and hv involving docs#HasDerivWithinAt (within Set.uIcc a b), or else we could have a variant with these assumptions. But maybe I'm missing some subtlety here.

I have no idea whether this is the correct approach to your problem though.

[Vincent Beffara]

The version with HasDerivWithinAt could probably be obtained from the one that we have (using some kind of Schwarz reflection to extend a ContDiffOn function on Icc a b to a ContDiffOn function on a neighborhood. Alternatively, you can always work on Icc (a + e) (b - e) and let e go to 0 in the end.

[Antoine Chambert-Loir]

If I read correctly what docs#ContDiffOn says, it seems to me that it includes the required condition on the extreme points when you apply it with s = Set.uIcc a b. In any case, this is what “a neighborhood within s of each point” means.

[Floris van Doorn]

docs#intervalIntegral.integral_deriv_mul_eq_sub is proven using docs#intervalIntegral.integral_eq_sub_of_hasDerivAt, which is a special case of docs#intervalIntegral.integral_eq_sub_of_hasDeriv_right. But we can use the last lemma directly to get what you want.

import Mathlib.MeasureTheory.Integral.IntegralEqImproper

open BigOperators Interval Topology Set intervalIntegral MeasureTheory

set_option autoImplicit false
variable {A : Type*} [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A] {a b : ℝ}

theorem integral_deriv_mul_eq_sub' {u v u' v' : ℝ → A}
    (hu : ∀ x ∈ [[a, b]], HasDerivWithinAt u (u' x) [[a, b]] x)
    (hv : ∀ x ∈ [[a, b]], HasDerivWithinAt v (v' x) [[a, b]] x)
    (hu' : IntervalIntegrable u' volume a b)
    (hv' : IntervalIntegrable v' volume a b) :
    ∫ x in a..b, u' x * v x + u x * v' x = u b * v b - u a * v a := by
  have h2u : ContinuousOn u [[a, b]] :=
    fun x hx ↦ (hu x hx).continuousWithinAt
  have h2v : ContinuousOn v [[a, b]] :=
    fun x hx ↦ (hv x hx).continuousWithinAt
  apply integral_eq_sub_of_hasDeriv_right (h2u.mul h2v)
  · exact fun x hx ↦ (hu x <| mem_Icc_of_Ioo hx).mul (hv x <| mem_Icc_of_Ioo hx) |>.hasDerivAt
      (Icc_mem_nhds hx.1 hx.2) |>.hasDerivWithinAt
  · exact (hu'.mul_continuousOn h2v).add (hv'.continuousOn_mul h2u)

[Floris van Doorn]

@Antoine Chambert-Loir: ContDiffOn _ _ _ s only gives HasDerivAt only at points in the interior of s. docs#ContDiffOn.congr shows that ContDiffOn is independent of any values the function takes on points outside s. (But maybe I misunderstood what you were claiming.)

[Sébastien Gouëzel]

I think all the statements involving HasDerivAt on uIcc could (should?) also have versions using uIoo (except this is not a thing in mathlib) and assuming continuity on uIcc. We already have a version in this form, see docs#intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le, from which all the other ones can easily be derived.

[Antoine Chambert-Loir]

Floris van Doorn said:

Antoine Chambert-Loir: ContDiffOn _ _ _ s only gives HasDerivAt only at points in the interior of s. docs#ContDiffOn.congr shows that ContDiffOn is independent of any values the function takes on points outside s. (But maybe I misunderstood what you were claiming.)

I was just claiming that the doc string says otherwise.

[Vincent Beffara]

Sébastien Gouëzel said:

I think all the statements involving HasDerivAt on uIcc could (should?) also have versions using uIoo (except this is not a thing in mathlib) and assuming continuity on uIcc. We already have a version in this form, see docs#intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le, from which all the other ones can easily be derived.

Perhaps it would help discovery to have Ioo somewhere in the name? of_le does refer to one of the assumptions but does not point to the main difference when compared to docs#intervalIntegral.integral_eq_sub_of_hasDerivAt ... Or perhaps integral_eq_sub_of_continuousOn_of_hasDerivAt to stress the fact that the assumptions are on different sets?

[Sébastien Gouëzel]

Yes, the current name is very bad. I found it just by browing the file.

[Floris van Doorn]

I PR'd in #11886 incorporating Sebastien's suggestion.

[Antoine Chambert-Loir]

I come back about the significance of WithinAt etc. The docstrings talk about “neighborhoods of x within s”, and docs#nhdsWithin seems to agree with the mathematical meaning of a neighborhood of a point $x$ within a set $s$.
Provided this understanding is OK, when $s$ is an interval $[a;b]$, the bounds $a$ and $b$ belong to the relative interior, “withinAt” should say something.

[Floris van Doorn]

The docstring of ContinuousOn end with "neighborhood of x in s", which is meant in the sense of nhdsWithin.

[Alex Kontorovich]

Sébastien Gouëzel said:

I think all the statements involving HasDerivAt on uIcc could (should?) also have versions using uIoo (except this is not a thing in mathlib)

FYI There's a definition of uIoo and some API for it sitting around in #9598...

[Sébastien Gouëzel]

@Yury G. Kudryashov , are you still planning to have a look at #9598, or do you prefer if someone takes it over?

[Sébastien Gouëzel]

@Alex Kontorovich , if you split off the uIoo part from this PR in another PR, I'll merge it quickly! Often, small self-contained PRs get in much quicker than big PRs. You can have a look at how I split #11776 into small chunks for instance, it worked pretty well (with different reviewers with different expertise on the different bits, while noone would have looked at the whole thing...)

[Vincent Beffara]

Ah btw @Sébastien Gouëzel speaking of this, do you by any chance have code showing this?

lemma fourier_surjection_on_schwartz (f : 𝓢(ℝ, ℂ)) : ∃ g : 𝓢(ℝ, ℂ), 𝓕 g = f := sorry

Asking for a friend ;-)

[Sébastien Gouëzel]

I hope that within a few weeks, we should have in Mathlib the fact that the Fourier transform maps Schwartz to Schwartz. Then you can deduce your statement from Fourier inversion. My advice would be to keep the sorry in PNT until then. Current PRs in this direction are #11776, #11867 and #11868 by the way :-), with the latter two being mostly straightforward to review.

[Alex Kontorovich]

Sébastien Gouëzel said:

Alex Kontorovich , if you split off the uIoo part from this PR in another PR, I'll merge it quickly! Often, small self-contained PRs get in much quicker than big PRs. You can have a look at how I split #11776 into small chunks for instance, it worked pretty well (with different reviewers with different expertise on the different bits, while noone would have looked at the whole thing...)

I guess I didn't think #9598 was all that big... :( It's only ~600 lines. It's gotten a number of very useful comments and suggestions already, which have been addressed (to my knowledge), so I'm not sure why it's still sitting... (But of course I know we're all very busy!...) I guess if it sits for another week or so, I'll split off the uIoo bits...

[Alex Kontorovich]

Sébastien Gouëzel said:

I hope that within a few weeks, we should have in Mathlib the fact that the Fourier transform maps Schwartz to Schwartz. Then you can deduce your statement from Fourier inversion. My advice would be to keep the sorry in PNT until then. Current PRs in this direction are #11776, #11867 and #11868 by the way :-), with the latter two being mostly straightforward to review.

This is great! And it's good to know - Heather and I were (slowly) moving in that direction (after #9663, which turned into #9773), so we'll work on something else.

One nice thing about the PNT+ blueprint approach is that people are encouraged to publicly "claim" tasks before they start working on them, to minimize as much possible the possibility of duplicating efforts. I don't suppose that kind of "claim" mechanism can be made to work on the larger Mathlib project... (These zulip discussions are the next best thing, it seems?...)

[Sébastien Gouëzel]

Oops, sorry for the lack of coordination! Yes, Zulip is the best we have for this kind of discussion, but it's definitely not perfect.

[Jireh Loreaux]

Alex Kontorovich said:

I guess I didn't think #9598 was all that big... :( It's only ~600 lines. It's gotten a number of very useful comments and suggestions already, which have been addressed (to my knowledge), so I'm not sure why it's still sitting... (But of course I know we're all very busy!...) I guess if it sits for another week or so, I'll split off the uIoo bits...

Obviously this isn't always possible, but I think shooting for < 200 lines, and ideally even less, is a good goal in general.

[Alex Kontorovich]

Of course no worries at all! I'm just imagining if one could build some big public ledger, a "blueprint dependency graph"-type map of Mathlib, somehow organizing what everyone's working on and has laid claim to...

[Alex Kontorovich]

Jireh Loreaux said:

Obviously this isn't always possible, but I think shooting for < 200 lines, and ideally even less, is a good goal in general.

Ah, that's good to know, thanks. I was imagining that anything <1000 lines is not "too" big. But good to know that ~200 is the max target...

[Ruben Van de Velde]

I think that's what projects could be used for

[Alex Kontorovich]

Oh cool!! I didn't know about that. (But it seems it's not used so much in practice...?)

[Yury G. Kudryashov]

Hi, I have very little free time because of my new job. Feel free to unassign any PR from me. I'm sorry for not saying it out loud earlier.