Real-power calculus for the majorants

The majorant proofs use the exported derivative interface. The private implementation import keeps complex-power calculus and inner-product norm calculus out of their environments.

theorem Majorants.hasDerivAt_realPower {x p : ℝ} (h : x ≠ 0 ∨ 1 ≤ p) : HasDerivAt (fun (x : ℝ) => x ^ p) (p * x ^ (p - 1)) x

Real-power differentiation without exposing the implementation imports.

theorem Majorants.hasDerivAt_absolutePower (x : ℝ) {p : ℝ} (hp : 1 < p) : HasDerivAt (fun (x : ℝ) => |x| ^ p) (p * |x| ^ (p - 2) * x) x

The absolute-power derivative, keeping norm calculus behind this interface.

theorem HasDerivAt.burkholderRealPower {f : ℝ → ℝ} {f' p x : ℝ} (hf : HasDerivAt f f' x) (h : f x ≠ 0 ∨ 1 ≤ p) : HasDerivAt (fun (y : ℝ) => f y ^ p) (f' * p * f x ^ (p - 1)) x

Differentiate a real power through the majorants' calculus interface.

theorem DifferentiableAt.burkholderRealPower {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {p : ℝ} {x : E} (hf : DifferentiableAt ℝ f x) (h : f x ≠ 0 ∨ 1 ≤ p) : DifferentiableAt ℝ (fun (y : E) => f y ^ p) x

Preserve differentiability through the majorants' real-power interface.