Vincent's 5 Oct rad(xx) proof
Vincent, P1788
On 5 Oct 2012, at 13:26, 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.
...
> * |m - (a+b)/2| ≤ |m' - (a+b)/2|.
> * m ≤ m'.
... I believe your proof is correct, however you left out one step of argument, and I was puzzled for a bit ...
> If m' = m, then r = b-m < b'-m' ≤ r'. So, let us assume that m' > m.
Here you need to point out that this implies m' > (a+b)/2 else m' is between m and (a+b)/2, which contradicts the first * relation above. Hence that relation reduces to what you give in the next line:
> Then (a+b)/2 - m ≤ m' - (a+b)/2, i.e. r = b-m ≤ m'-a ≤ r'.
>
> So, in every case, r ≤ r'.
Nice stuff. Simple, but not trivial.
You write "...seems true for any interval type". That's not the point, is it? You've proved it for any *number format*. The type never appears; indeed your proof relies on being able to choose an arbitrary interval. Otherwise you might have [a,b] contained in [a',b'], both T-intervals, but both [a,b'] and [a',b] not T-intervals so your argument using transitivity would fail.
John