ContinuousOn_derivWithin_of_deriv

Stream: Is there code for X?

[Alex Kontorovich]

Any suggestions for how to do something like the below, that is, replace derivWithin with deriv (given that I only care about both on the same set as "Within"...)?

import Mathlib

lemma ContinuousOn_derivWithin_of_deriv (φ : ℝ → ℂ) (a b : ℝ)
    (h : ContinuousOn (deriv φ) (Set.uIcc a b)) :
    ContinuousOn (derivWithin φ (Set.uIcc a b)) (Set.uIcc a b) := by sorry

[Vincent Beffara]

Is this true without assuming differentiability? E.g. one could conceive of a function that is nowhere differentiable but right differentiable at 0 with right derivative 1, then it is differentiable within Icc 0 1 at 0, it has deriv identically 0 but derivWithin is discontinuous at 0.

[Alex Kontorovich]

Ok sure, let's add differentiability:

import Mathlib

lemma ContinuousOn_derivWithin_of_deriv {φ : ℝ → ℂ} {a b : ℝ}
    (φDiff : ContDiffOn ℝ 1 φ (Set.uIcc a b)) :
    ContinuousOn (derivWithin φ (Set.uIcc a b)) (Set.uIcc a b) := by sorry

[Sébastien Gouëzel]

@loogle ContDiffOn, ContinuousOn, derivWithin

[Michael Stoll]

@loogle ContDiffOn, ContinuousOn, derivWithin

[loogle]

:search: ContDiffOn.continuousOn_derivWithin

[Sébastien Gouëzel]

Loogle is amazing, and our library is also amazing :-)

[Michael Stoll]

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type uF} [inst_1 : NormedAddCommGroup F]
 [inst_2 : NormedSpace 𝕜 F] {n : ℕ∞} {f₂ : 𝕜 → F} {s₂ : Set 𝕜}, ContDiffOn 𝕜 n f₂ s₂ → UniqueDiffOn 𝕜 s₂ →
 1 ≤ n → ContinuousOn (derivWithin f₂ s₂) s₂

Pretty close...

[Sébastien Gouëzel]

(It won't cover exactly your use case, as for a = b then uIcc a bis not a set of unique differentiability, but since any function is continuous on a singleton you should be fine)