Differentiability of the natural map ℝ → ℂ

Stream: Is there code for X?

[Michael Stoll]

I'm looking for

import Mathlib

namespace Complex

lemma differentiable_ofReal : Differentiable ℝ ofReal' := by sorry

which I'm expecting to exist in Mathlib, but
@loogle "ifferentiable", "ofReal"

[loogle]

:shrug: nothing found

[Michael Stoll]

Can this really be missing, or am I looking for it in the wrong way?

[Johan Commelin]

cc @Yury G. Kudryashov

[Michael Stoll]

Here is a proof:

lemma differentiable_ofReal : Differentiable ℝ ofReal' := by
  intro x
  have H : HasDerivAt ofReal' 1 x
  · refine hasDerivAt_iff_tendsto.mpr ?_
    simp only [Real.norm_eq_abs, real_smul, ofReal_sub, mul_one, sub_self, norm_zero, mul_zero,
      tendsto_const_nhds_iff]
  exact ⟨_, H.hasFDerivAt⟩

(without investing too much thought).

[Ruben Van de Velde]

Can you derive it from isometry_ofReal?

[Michael Stoll]

There are docs#HasDerivAt.comp_ofReal and docs#HasDerivAt.ofReal_comp, which one could use, but it is a bit strange that the derivative of the function itself does not seem to be available.

[Michael Stoll]

A one-liner:

lemma differentiable_ofReal : Differentiable ℝ ofReal' :=
  fun x ↦ ⟨_, (HasDerivAt.ofReal_comp <| hasDerivAt_id x).hasFDerivAt⟩

[Michael Stoll]

Maybe this is better:

lemma hasDerivAt_ofReal (x : ℝ) : HasDerivAt ofReal' 1 x :=
  HasDerivAt.ofReal_comp <| hasDerivAt_id x

lemma differentiableAt_ofReal (x : ℝ) : DifferentiableAt ℝ ofReal' x :=
  (hasDerivAt_ofReal x).differentiableAt

lemma differentiable_ofReal : Differentiable ℝ ofReal' :=
  fun x ↦ ⟨_, (hasDerivAt_ofReal x).hasFDerivAt⟩

[Yury G. Kudryashov]

If all you need is Differentiable, then the shortest proof is Complex.ofRealClm.differentiable.

[Yury G. Kudryashov]

But we should add a bunch of lemmas about Complex.ofReal' to the library.

[Yury G. Kudryashov]

Do you volunteer to do that?

[Michael Stoll]

docs#Complex.ofRealClm
Now I know what "Clm" stands for :smile:

[Yury G. Kudryashov]

BTW, it should be renamed to ofRealCLM

[Yury G. Kudryashov]

(in this and several other definitions)

[Yury G. Kudryashov]

Same for Cle -> CLE

[Michael Stoll]

Yury G. Kudryashov said:

Do you volunteer to do that?

I can do that eventually.

I have a fairly long list of API lemmas that should go to various parts of Mathlib and that I'm planning to PR at some point; I can include the lemmas I've stated above (and perhaps more if somebody tells me what else might be needed) in that list.

[Yury G. Kudryashov]

We should also have lemmas about ContDiffAt etc (if we don't have them yet).

[Yury G. Kudryashov]

Possibly, about iterated derivatives.

[Anatole Dedecker]

Yury G. Kudryashov said:

BTW, it should be renamed to ofRealCLM

Or ofRealL?

[Jireh Loreaux]

I prefer CLM personally. The L is too closely tied to notation.

[Jireh Loreaux]

And what would you call a non-continuous version (nevermind that we don't need one in this case)?

[Anatole Dedecker]

We have some names with the small l I believe?

[Jireh Loreaux]

My point is it doesn't adhere to the naming convention, e.g. Complex.OfReall. Or did you mean subscript \_l?

[Ruben Van de Velde]

Michael Stoll said:

Yury G. Kudryashov said:

Do you volunteer to do that?

I can do that eventually.

I have a fairly long list of API lemmas that should go to various parts of Mathlib and that I'm planning to PR at some point; I can include the lemmas I've stated above (and perhaps more if somebody tells me what else might be needed) in that list.

By the way, I recommend starting on making such PRs sooner rather than later, both to prevent the task from seeming insurmountable and so other people can use your work already

[Anatole Dedecker]

Jireh Loreaux said:

My point is it doesn't adhere to the naming convention, e.g. Complex.OfReall. Or did you mean subscript \_l?

Yes I meant subscript.

[Jireh Loreaux]

Yeah, that's possible, I suppose, but it still feels like we're letting notation infect naming.

[Yury G. Kudryashov]

#10018 fixes Clm/Cle