coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Question on Coq-Interval: i_bisect_diff x vs. i_bisect taylor x 1

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] Question on Coq-Interval: i_bisect_diff x vs. i_bisect taylor x 1
Date: Thu, 17 Jan 2019 16:42:06 +0000
Accept-language: de-DE, en-US
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga05.intel.com
Dlp-product: dlpe-windows
Dlp-reaction: no-action
Dlp-version: 11.0.400.15
Ironport-phdr: 9a23:IGafqBaDy9e6/Cod7fs4CKL/LSx+4OfEezUN459isYplN5qZr8i4bnLW6fgltlLVR4KTs6sC17KG9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCa+bL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjA57m/Zl9BwgqxYrhKvpRN/wpLbb46aOvdlYqPdZNcXSXZdUspNSSBMBJ63YYsVD+oGOOZVt4fxqUYJrRSgCgmsGPnvyjhQhnPuwKY01OUhHh3G3AM6Ad0OtHrYp8jyOacXUOC60KnIwi/dYPNSwzv984/IfQ4uofGQR7JwdtLRxFIuFwPDklWft4jlMymJ2eQKtmiW9uxtXv+hhW4grgF+uDmvxsE0h4nIgIIV1k7L9SFjzIkoO9K1TlNwb928EJZIqi2XM5V6TtkiTmxooio3yqMKtYS0cSUE0Jgr2h/SZvKdf4WG7B/vTvidLDl8iX5/Zb6yhAu+/VC9xuD9UsS4ykhGoypKn9XWqHwBzR3e58iBR/Bg5EmuwyyP2BrW6uxcIUA7i67bK5k5z741mZocq1jPEy/slEX3iq+Walsr+uyy5+v7ZbXmo4eQN45yig7gLqQjgtGzDOAmPgQUX2WW+f6w2b398UHjT7hHgOU6kqzDv5DbIcQbqLS5AwhQ0os77ha/Diup0NQCknYZKFJJYgmHj4/3NFHBPPD4F/C/g0y3nTdqwfDGIqPuApHXInffl7fheK5x61RAxwor0dBf+5VUB6kdL/L0Q0/9rcDXDhskMwOv2OvnE9V81oYGWW2VGKOZMaXSsUWJ5u01OeWMapUV637BLK1v7Pn3yHQ9hFU1fK+z3JJRZmryVqBtJFzcan7xiP8AF30Lt0wwVrq5pkeFVGsZXHG/UL4m4Sl/QKenBofKS4TnyOiE3Sy7F5BSIHtBB1+QC3DwX4SCR/oILimVJ5kywXQ/SbG9Rtp5hlmVvwjgxu8/d7uGymgjrZvmkeNNyajWnBA2+yZzCp3EgWCLU2xw2GgPQm1vhfwtkQlG0l6GlJNArblAD9UKvqFIVBs3MdjXyOkoU4mvCDKERc+ATROdevvjATw1SYtukdoBah4gXdSkkh3HmSGtBu1Nmg==

Dear Guillaume,

> My guess is that i_bisect_diff is getting confused by the absolute value.
> If you
> remove it, the bounds should get much closer to the ones from
> i_bisect_taylor.

Thanks for the explanation! I guess the best option is then to use
i_bisect_taylor x 1 instead of i_bisect_diff.

Removing Rabs does lead to the expected result (i_bisect_taylor is better by
about a factor of 3 or 4 than i_bisect_diff, but i_bisect_diff is much better
than i_bisect). What does not work is keeping Rabs and changing the x range
such that the term inside of Rabs does not change the sign - i_bisect_diff
and i_bisect are still the same then.

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

[Coq-Club] Question on Coq-Interval: i_bisect_diff x vs. i_bisect taylor x 1, Soegtrop, Michael, 01/17/2019
- Re: [Coq-Club] Question on Coq-Interval: i_bisect_diff x vs. i_bisect taylor x 1, Guillaume Melquiond, 01/17/2019
  - RE: [Coq-Club] Question on Coq-Interval: i_bisect_diff x vs. i_bisect taylor x 1, Soegtrop, Michael, 01/17/2019
    - Re: [Coq-Club] Question on Coq-Interval: i_bisect_diff x vs. i_bisect taylor x 1, Guillaume Melquiond, 01/17/2019
      - RE: [Coq-Club] Question on Coq-Interval: i_bisect_diff x vs. i_bisect taylor x 1, Soegtrop, Michael, 01/17/2019