The distance of from a point $x$ to a set $A$ is defined by $$ d(x,S) = \inf\{d(x,a)\mid a\in A\}, $$ where you may choose the setting to be $\mathbb R^n$, a Banach space or a complete metric space.
This is of interest in constructive analysis and my own theory called abstract Stone duality, as explained below, but I believe that my question is meaningful to classical real analysts, whose intuition I am seeking.
Here $A$ is fixed and I am considering the real valued function $d(x)=d(x,A)$.
My picture is that $A$ is the sea and we are on an island that is foggy (so you can't see the sea) but you can measure the altitude, which is equal to the (nearest) distance to the sea. So the geography of the island consists of conical hills.
Although the altitude is a scalar (it doesn't tell you which way to get to the sea), so long as you're not at the summit of a hill, there is a unique path that goes straight down to the sea on a $45^\circ$ slope.
My conjecture is that $D\cup A$ is dense, where $D$ is the subspace on which $d(x)$ is differentiable.
For any point $x$, even a summit, there is a straight line $[x,a]$ of length $d(x)$, with $a\in A$. Let's call any open segment of such a line a downward path and let $D_0$ be the union of all such segments. Then $D_0\cup A$ is dense.
By simple Euclidean geometry (if we're working in $\mathbb R^n$), any two downward paths through a point of $D_0$ are co-linear.
If $D_0$ is open then it coincides with $D$ and my conjecture follows.
Is this necessarily true?
Here is the context of my question:
In Bishop-style constructive analysis, a subset $S$ of a metric space is said to be located if $f(x,S)$ is a real number and not just a lower real. Many classical theorems become constructively valid once locatedness is added as a hypothesis.
In various forms of constructive topology (including mine, called abstract Stone duality), there is a concept called overtness that is lattice-dual to compactness. For example, familiar results using with words closed, compact and Hausdorff have duals with the words open, overt and discrete.
However, overtness is invisible (vacuously true) in the classical setting, so I am trying to show how it is related to more familiar ideas, by concentrating on the metric case.
What is important is not the overt subspace $A$ qua subspace, but the predicate $\lozenge U$ on open subspaces of whether $U\cap A$ is inhabited. This satisfies $$ \lozenge \bigcup\{U_i\mid i\in I\} \Longrightarrow \exists i\in I. \lozenge U_i. $$
Since $\lozenge$ preserves unions in this sense, we need only consider its values at \emph{basic} open subspaces, which are the balls $B_r(x)$ in the case of a metric space. So we write $$ d(x) \lt r \iff \lozenge B_r(x). $$
This function has the following properties: $$ d(x) < r \iff \exists r'. d(x) < r' < r $$ $$ d(x) < r \land d(x,y)\lt s \Longrightarrow d(y)< r+s $$ $$ d(x) < r \land \epsilon\gt 0 \Longrightarrow \exists y. d(x,y)< r\land d(y)<\varepsilon $$
In fact $d(x)$ is in general only an upper real number, so the function $d$ is upper semi-continuous. They are real-valued and continuous iff the subspace is also closed; for simplicity we assume this here.
The subspace in question is $A = \{a\mid d(a)= 0\}$, where $d(a)=0$ means $\forall\varepsilon\gt 0.d(a)<\varepsilon$.
It is not difficult to show that this function $d$ is exactly the point--set distance $d(x,A)$ above.
However, where this may be of interest to classical real and numerical analysts is this analogy with the Newton--Raphson algorithm:
Newton's idea is that, given an approximant $x_0$ to a solution to $f(x)=0$ where $f$ is differentiable, we get a better approximant $$ x_1=x_0-\delta(x_0) \quad\mbox{where}\quad \delta(x) = f(x)/f'(x), $$ at least in certain good circumstances.
My observation is that $\delta(x)$ is like $d(x)$ above, except that
$\delta$ is a vector, but $d$ is a scalar; and
$d$ satisfies a triangle law, but $\delta$ doesn't.
Adding the triangle law is easy in logic but not of course in numerical analysis. The reason for asking about differentiability is to turn a scalar into a vector.
I would like then to find some weaker notion than the join-preserving operator that would be an abstraction of the Newton--Raphson algorithm.
The connection between locatedness and overtness above was first considered by Bas Spitters. My draft paper about these topics is Overt Subspaces of ${\mathbb R}^n$
NB This question is not my mathematical territory, so I do not know what are the appopriate tags, so others are welcome to change these.
