Zulip Chat Archive

What's the simplest way to prove things like the following (basically fundamental theorem of calculus, plus continuity)? (Maybe I need more than just ContinuousAt; feel free to add more assumptions...)

import Mathlib

open Topology

example (f : ℝ → ℝ) (x : ℝ) (h : ContinuousAt f x) :
  (fun y ↦ (∫ t in x..y, f t) - (y - x) * f x) =o[𝓝 x] (fun y ↦ y - x) := by
  sorry

example (f : ℝ → ℝ) (x : ℝ) (h : ContinuousAt f x) :
  (fun y ↦ (∫ t in x..y, f (t+(y-x))) - (y - x) * f x) =o[𝓝 x] (fun y ↦ y - x) := by
  sorry

Thanks!

Johan Commelin (Dec 29 2023 at 17:33):

cc @Yury G. Kudryashov

Yury G. Kudryashov (Dec 29 2023 at 17:35):

Isn't it HasDerivAt?

Yury G. Kudryashov (Dec 29 2023 at 17:35):

Let me find the theorem

Yury G. Kudryashov (Dec 29 2023 at 17:37):

The first example is docs#intervalIntegral.integral_hasDerivAt_right

Yury G. Kudryashov (Dec 29 2023 at 17:38):

I think that ContinuousAt f b should imply StronglyMeasurableAtFilter f (nhds b), let me try to prove it.

Yury G. Kudryashov (Dec 29 2023 at 17:39):

Is there a typo in the second example? Substituting t = y gives f (2y - x), probably not what you want.

Yury G. Kudryashov (Dec 29 2023 at 17:44):

Yury G. Kudryashov said:

I think that ContinuousAt f b should imply StronglyMeasurableAtFilter f (nhds b), let me try to prove it.

No, it doesn't. But ∀ᶠ a in 𝓝 x, ContinuousAt f a does, see docs#ContinuousAt.stronglyMeasurableAtFilter

Yury G. Kudryashov (Dec 29 2023 at 17:51):

import Mathlib

open MeasureTheory Topology

example (f : ℝ → ℝ) (x : ℝ) (h : ∀ᶠ a in 𝓝 x, ContinuousAt f a) :
    (fun y ↦ (∫ t in x..y, f t) - (y - x) * f x) =o[𝓝 x] (fun y ↦ y - x) := by
  have hi : IntervalIntegrable f volume x x := by simp [intervalIntegrable_iff]
  have hmeas : StronglyMeasurableAtFilter f (𝓝 x) :=
    ContinuousAt.stronglyMeasurableAtFilter isOpen_interior interior_subset _
      (mem_interior_iff_mem_nhds.2 h)
  have hd := intervalIntegral.integral_hasDerivAt_right hi hmeas h.self_of_nhds
  simpa [sub_mul] using hd.isLittleO

Yury G. Kudryashov (Dec 29 2023 at 17:52):

We should add lemmas for the first 2 haves. IMHO, we should replace the existing ContinuousAt.stronglyMeasurableAtFilter with the new lemma.

Yury G. Kudryashov (Dec 29 2023 at 17:52):

@Sebastien Gouezel What do you think about it? I mean, assuming ∀ᶠ a in 𝓝 x, ContinuousAt f a in ContinuousAt.stronglyMeasurableAtFilter.

Sébastien Gouëzel (Dec 29 2023 at 17:57):

I think the assumption ∀ᶠ a in 𝓝 x, ContinuousAt f a is very convoluted: it is a complicated way of saying that there is a neighborhood of x on which f is continuous. I am not sure that it would be more usable than the version we have currently. The best assumptions for the example, I think, would be to assume continuous just at a, and global measurability.

Alex Kontorovich (Dec 29 2023 at 19:57):

Yury G. Kudryashov said:

Is there a typo in the second example? Substituting t = y gives f (2y - x), probably not what you want.

Yes exactly, and when y is in a neighborhood of x, f(2 y - x) should be close to f x... I just want to use continuity once more inside the integrand... (But I now think I can figure out how to do that...) Thanks!!