Integral powers of a C^n function

Mathlib provides ContDiffAt.pow for natural powers and ContDiffAt.inv for the inverse of a nonvanishing function, but no lemma for an integral power. This file supplies the missing combination: an integral power of f is as smooth as f is, either away from a zero of f or for a nonnegative exponent. The hypothesis is the one carried by Mathlib's DifferentiableAt.zpow.

Main results

• ContDiffWithinAt.zpow: fun z ↦ f z ^ (m : ℤ) is C^n within a set at a point where f is C^n and either f does not vanish or m is nonnegative.
• ContDiffAt.zpow, ContDiffOn.zpow and ContDiff.zpow: the remaining members of the family, with the hypotheses of DifferentiableOn.zpow and Differentiable.zpow.

theorem ContDiffWithinAt.zpow {𝕜 : Type u_1} {E : Type u_2} {𝕜' : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {f : E → 𝕜'} {s : Set E} {x : E} {m : ℤ} {n : WithTop ℕ∞} (hf : ContDiffWithinAt 𝕜 n f s x) (h : f x ≠ 0 ∨ 0 ≤ m) : ContDiffWithinAt 𝕜 n (fun (z : E) => f z ^ m) s x

An integral power of a C^n function is C^n within a set at a point where the function does not vanish, and also, whatever the value there, for a nonnegative exponent.

theorem ContDiffAt.zpow {𝕜 : Type u_1} {E : Type u_2} {𝕜' : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {f : E → 𝕜'} {x : E} {m : ℤ} {n : WithTop ℕ∞} (hf : ContDiffAt 𝕜 n f x) (h : f x ≠ 0 ∨ 0 ≤ m) : ContDiffAt 𝕜 n (fun (z : E) => f z ^ m) x

An integral power of a C^n function is C^n at a point where the function does not vanish, and also, whatever the value there, for a nonnegative exponent.

theorem ContDiffOn.zpow {𝕜 : Type u_1} {E : Type u_2} {𝕜' : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {f : E → 𝕜'} {s : Set E} {m : ℤ} {n : WithTop ℕ∞} (hf : ContDiffOn 𝕜 n f s) (h : (∀ z ∈ s, f z ≠ 0) ∨ 0 ≤ m) : ContDiffOn 𝕜 n (fun (z : E) => f z ^ m) s

An integral power of a C^n function is C^n on a set where the function does not vanish, and also, whatever its values there, for a nonnegative exponent.

theorem ContDiff.zpow {𝕜 : Type u_1} {E : Type u_2} {𝕜' : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {f : E → 𝕜'} {m : ℤ} {n : WithTop ℕ∞} (hf : ContDiff 𝕜 n f) (h : (∀ (z : E), f z ≠ 0) ∨ 0 ≤ m) : ContDiff 𝕜 n fun (z : E) => f z ^ m

An integral power of a C^n function is C^n if the function does not vanish, and also, whatever its values, for a nonnegative exponent.