PhyslibAlpha.ClassicalMechanics.NortonDome.Sqrt

Calculus of the real square root near zero

i. Overview

Two facts about the real square root at zero, where Mathlib's calculus does not reach: the cube `√y ^ 3` is differentiable everywhere, with derivative `(3/2) √x`, and `√` is not Lipschitz on any interval `[0, ε]`. The first gives the derivative of the potential of the Norton dome, the second the failure of the Picard–Lindelöf hypothesis for its force.

ii. Key results

`hasDerivAt_sqrt_pow_three` is the derivative of `√y ^ 3` at every real number.
`not_lipschitzOnWith_sqrt` is the failure of the Lipschitz property of `√` on `[0, ε]`.

iii. Table of contents

A. The derivative of the cube of the square root
B. The square root is not Lipschitz at zero

iv. References

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

A. The derivative of the cube of the square root

To the left of zero the square root vanishes, to the right the chain rule applies, and at zero the difference quotient of `√t ^ 3 = t √t` is `√t`, which tends to zero.

B. The square root is not Lipschitz at zero

A bound `√y ≤ K y` on `[0, ε]` gives `1 ≤ K √y` for every positive `y ≤ ε`, which fails at `y = min ε (1 / (2K + 1)²)`.

2 declarations

theorem

The derivative of $(\sqrt{x})^3$ is $\frac{3}{2} \sqrt{x}$ for all $x \in \mathbb{R}$

#hasDerivAt_sqrt_pow_three

For any real number $x$ , the function $f(y) = (\sqrt{y})^3$ is differentiable at $x$ with a derivative equal to $\frac{3}{2} \sqrt{x}$ . In particular, although the square root function $\sqrt{y}$ itself is not differentiable at $x = 0$ , its cube $(\sqrt{y})^3$ is differentiable at $x = 0$ with derivative $0$ . (Note: for $y < 0$ , $\sqrt{y}$ is defined to be $0$ ).

theorem

The real square root is not Lipschitz on $[0, \epsilon]$ for $\epsilon > 0$

#not_lipschitzOnWith_sqrt

For any non-negative real number $K$ and any $\epsilon > 0$ , the real square root function $x \mapsto \sqrt{x}$ is not Lipschitz continuous with constant $K$ on the closed interval $[0, \epsilon]$ .