PhyslibAlpha.ClassicalMechanics.NortonDome.PosPartPow

Powers of the positive part

i. Overview

The function `y ↦ max (y - c) 0 ^ (n + 2)` vanishes to the left of `c` and is a polynomial to its right. It is differentiable everywhere, including at `c`, and is `C^(n+1)`. Functions of this shape are the standard witnesses for the failure of uniqueness of ODEs with a non-Lipschitz right-hand side, of which the Norton dome is the physical instance.

ii. Key results

`hasDerivAt_max_sub_pow` is the derivative `(n + 2) max (y - c) 0 ^ (n + 1)`, at every point.
`contDiff_max_sub_pow` is the `C^(n+1)` regularity.

iii. Table of contents

A. The derivative
B. Regularity

iv. References

- Norton, J. D., *The dome: an unexpectedly simple failure of determinism*, Philosophy of Science 75 (2008), 786–798.

A. The derivative

By cases: to the left of `c` the function vanishes near the point, to the right it agrees near the point with `(y - c) ^ (n + 2)`, and at `c` the difference quotient is `max t 0 ^ (n + 1)`, which tends to zero.

B. Regularity

By induction on `n`: the derivative of the `(n + 3)`-rd power is a constant multiple of the `(n + 2)`-nd, which is `C^(n+1)` by the induction hypothesis.

2 declarations

theorem

The derivative of $(\max(y - c, 0))^{n+2}$ is $(n + 2)(\max(x - c, 0))^{n + 1}$

#hasDerivAt_max_sub_pow

For any real numbers $c$ and $x$ , and any natural number $n$ , the function $f(y) = (\max(y - c, 0))^{n+2}$ is differentiable at $x$ with derivative $f'(x) = (n + 2) (\max(x - c, 0))^{n + 1}$ . This derivative holds for all $x \in \mathbb{R}$ , including the point $x = c$ .

theorem

The function $(\max(y - c, 0))^{n+2}$ is $C^{n+1}$

#contDiff_max_sub_pow

For any real constant $c$ and any natural number $n$ , the function $f(y) = (\max(y - c, 0))^{n + 2}$ is $(n+1)$ -times continuously differentiable, denoted as $C^{n+1}$ .