Differentiability of `(f x)^n`

Stream: mathlib4

[Yury G. Kudryashov]

Is it possible that fun x ↦ f x ^ n, n : ℤ, is differentiable at a, n ≠ 0, f a ≠ 0, but f is not differentiable at a? Here f is a function from a NontriviallyNormedField to itself. If the field is a CompleteSpace, then I can use the inverse function theorem to prove existence of a local smooth n-th root near (f a)^n. Is it true without the CompleteSpace assumption?

[Yury G. Kudryashov]

#xy: I'm trying to understand if I can drop the differentiability assumption in logDeriv_fun_pow in #12804.

[Kevin Buzzard]

Sure: f(x)=1 if x is irrational and -1 if x is rational, and n=2 (which makes me think that perhaps you've not asked the question you meant to ask?)

[Yaël Dillies]

Maybe f itself is continuous?

[Yaël Dillies]

I think I have a counterexample to that modified question

[Yury G. Kudryashov]

Probably, replacing DifferentiableAt with ContinuousAt isn't worth it.

[Yaël Dillies]

Ah no, my counterexample doesn't work because you're asking for the function to be to the field itself

[Antoine Chambert-Loir]

If you can make it work via completeness, then it works without because it suffices to prove the required asymptotic behavior after injection to the completed field.

[Yury G. Kudryashov]

Of course, my "proof" was wrong (left inverse vs right inverse).