Mixing `ContDiffOn` and `deriv`

Stream: Is there code for X?

[Alex Kontorovich]

What's a quick way to show this?

import Mathlib

theorem ContDiffOn.hasDeriv_deriv {φ : ℝ → ℂ} {s : Set ℝ} (φDiff : ContDiffOn ℝ 1 φ s) {x : ℝ} (x_in_s : x ∈ s) :
    HasDerivAt φ (deriv φ x) x := by
  sorry

Thanks!

[Alex Kontorovich]

Also this one please: (basically trying to extract the expected information out of ContDiff _ 1)

import Mathlib

theorem ContDiffOn.continuousOn_deriv {φ : ℝ → ℂ} {a b : ℝ}
    (φDiff : ContDiffOn ℝ 1 φ (Set.uIcc a b)) :
    ContinuousOn (deriv φ) (Set.uIcc a b) := by
  sorry

Thanks!

[Tomas Skrivan]

The second one is almost solved by

import Mathlib

theorem ContDiffOn.continuousOn_deriv {φ : ℝ → ℂ} {a b : ℝ}
    (φDiff : ContDiffOn ℝ 1 φ (Set.uIcc a b)) :
    ContinuousOn (deriv φ) (Set.uIcc a b) := by
  apply ContDiffOn.continuousOn (𝕜:=ℝ) (n:=0)
  apply (fun h => ((contDiffOn_succ_iff_deriv_of_isOpen sorry).1 h).2)
  assumption

It would work on Set.Ioo a b, the closed interval needs some more massaging. This is also nice example for fun_prop, a tactic that would ideally solve this automatically but it fails completely here.

[Patrick Massot]

I’m not sure the first one is true.

[Patrick Massot]

And indeed the following isn’t super promising:

example : ContDiffOn ℝ 1 (fun x : ℝ ↦ |x|) {0} := by
  apply contDiffOn_id.congr
  simp

[Patrick Massot]

So you lemma would apply to the absolute value function with s = {0}, x = 0 and φ = abs.

[Alex Kontorovich]

Argh. You would think whatever ContDiffOn _ 1 is doing under the hood, it means "once continuously differentiable"... which in particular would be (a) differentiable, and (b) the derivative would be continuous. Not so, you say!... :(

[Alex Kontorovich]

Ok, what if s in the first one is restricted to an interval Set.Ioo a b with a < b...?

[Patrick Massot]

Then there is no problem. The whole discussion is what it means to be differentiable on a set that is not open. On an open set there is no subtlety.

[Patrick Massot]

The problem is your statement mixes an assumption that see only the restriction of φ to s with a conclusion that has nothing to do with s.

[Alex Kontorovich]

Ok good; and is there easy API to conclude HasDerivAt φ (deriv φ x) x? (I didn't find it...)

[Alex Kontorovich]

Patrick Massot said:

The problem is your statement mixes an assumption that see only the restriction of φ to s with a conclusion that has nothing to do with s.

(Well, I'd asked for $x\in s$, so not nothing...?)

[Patrick Massot]

This is not the conclusion.

[Patrick Massot]

HasDerivAt has nothing specific to s.

[Junyan Xu]

There's docs#ContDiffOn.contDiffAt asking s is a neighborhood of x

[Patrick Massot]

Sure, asking to s is open is too much, being a neighborhood of x is enough.

[Alex Kontorovich]

Thanks, and is there then API connecting ContDiffAt with $n\ge1$ to HasDerivAt f (deriv f x) x...?

[Junyan Xu]

Yes, there are docs#ContDiffAt.hasStrictDerivAt and docs#HasStrictDerivAt.hasDerivAt

[Alex Kontorovich]

Ah, perfect! ContDiffAt.hasStrictDerivAt is what I couldn't find...