Re: a draft motion on midpoint and radius
On 2012-10-05 14:26:47 +0200, Vincent Lefevre wrote:
> On 2012-10-04 15:36:34 +0100, John Pryce wrote:
> > Example 2: for an arbitrary type
> > r = rad(xx) shall be increasing under set inclusion.
> > That is xx \subseteq yy implies rad(xx) <= rad(yy).
> > That seems less obvious, even with Vladik's specification for
> > inf-sup interval types. Vladik: is it true there?
>
> This seems true for any interval type. Indeed, let us consider
> bounded, non-empty intervals. The question is:
[...]
Same text with ASCII characters for Windows users:
If X is included in Y, do we necessarily have rad_F(X) <= rad_F(Y)?
Let us first answer for rad (not rounded): if the property is satisfied
for rad, it will be for rad_F; and if it is not satisfied for rad (but
I'll show that this is impossible), this will yield counter-examples for
rad_F (e.g. by translating the intervals so that the left bound of their
hull is larger than the maximum radius of the considered intervals).
By transitivity, the problem can be reduced to X = [a,b] and Y = [a,b']
with b' > b.
One has:
* m = mid_F([a,b]) such that
for all x in F, |m - (a+b)/2| <= |x - (a+b)/2|.
* m' = mid_F([a,b']) such that
for all x in F, |m' - (a+b')/2| <= |x - (a+b')/2|.
* r = rad([a,b]) = mag([a,b] - m) = max(m-a,b-m).
* r' = rad([a,b']) = mag([a,b'] - m') = max(m'-a,b'-m').
A simple figure: [a m m' b b']
The only consequences of the first two properties that will be used are:
* |m - (a+b)/2| <= |m' - (a+b)/2|.
* m <= m'.
If b-m <= m-a, then r = m-a <= m'-a <= r'. Now let us assume that
b-m > m-a. In this case, r = b-m and (a+b)/2 - m > 0.
If m' = m, then r = b-m < b'-m' <= r'. So, let us assume that m' > m.
Then (a+b)/2 - m <= m' - (a+b)/2, i.e. r = b-m <= m'-a <= r'.
So, in every case, r <= r'.
--
Vincent Lefèvre <vincent@xxxxxxxxxx> - Web: <http://www.vinc17.net/>
100% accessible validated (X)HTML - Blog: <http://www.vinc17.net/blog/>
Work: CR INRIA - computer arithmetic / AriC project (LIP, ENS-Lyon)