<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<link href="coqdoc.css" rel="stylesheet" type="text/css" />
<title>Flocq.Prop.Fprop_relative</title>
</head>
<body>
<div id="page">
<div id="header">
</div>
<div id="main">
<h1 class="libtitle">Library Flocq.Prop.Fprop_relative</h1>
<div class="code">
</div>
<div class="doc">
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
<div class="paragraph"> </div>
Copyright (C) 2010-2013 Sylvie Boldo
<br />
Copyright (C) 2010-2013 Guillaume Melquiond
<div class="paragraph"> </div>
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
<div class="paragraph"> </div>
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
<div class="paragraph"> </div>
<a name="lab21"></a><h1 class="section">Relative error of the roundings</h1>
</div>
<div class="code">
<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Flocq.Core.Fcore.html#"><span class="id" title="library">Fcore</span></a>.<br/>
<br/>
<span class="id" title="keyword">Section</span> <a name="Fprop_relative"><span class="id" title="section">Fprop_relative</span></a>.<br/>
<br/>
<span class="id" title="keyword">Variable</span> <span class="id" title="keyword">beta</span> : <a class="idref" href="Flocq.Core.Fcore_Zaux.html#radix"><span class="id" title="record">radix</span></a>.<br/>
<span class="id" title="keyword">Notation</span> <a name="bpow"><span class="id" title="abbreviation">bpow</span></a> <span class="id" title="var">e</span> := (<a class="idref" href="Flocq.Core.Fcore_Raux.html#bpow"><span class="id" title="definition">bpow</span></a> <span class="id" title="keyword">beta</span> <span class="id" title="var">e</span>).<br/>
<br/>
<span class="id" title="keyword">Section</span> <a name="Fprop_relative.Fprop_relative_generic"><span class="id" title="section">Fprop_relative_generic</span></a>.<br/>
<br/>
<span class="id" title="keyword">Variable</span> <a name="Fprop_relative.Fprop_relative_generic.fexp"><span class="id" title="variable">fexp</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a>.<br/>
<span class="id" title="keyword">Context</span> { <span class="id" title="var">prop_exp</span> : <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Valid_exp"><span class="id" title="class">Valid_exp</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.fexp"><span class="id" title="variable">fexp</span></a> }.<br/>
<br/>
<span class="id" title="keyword">Section</span> <a name="Fprop_relative.Fprop_relative_generic.relative_error_conversion"><span class="id" title="section">relative_error_conversion</span></a>.<br/>
<br/>
<span class="id" title="keyword">Variable</span> <a name="Fprop_relative.Fprop_relative_generic.relative_error_conversion.rnd"><span class="id" title="variable">rnd</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a>.<br/>
<span class="id" title="keyword">Context</span> { <span class="id" title="var">valid_rnd</span> : <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Valid_rnd"><span class="id" title="class">Valid_rnd</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.relative_error_conversion.rnd"><span class="id" title="variable">rnd</span></a> }.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="relative_error_lt_conversion"><span class="id" title="lemma">relative_error_lt_conversion</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">b</span>, (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#1cc22ba6849531267d3b25ca7b262449"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#b"><span class="id" title="variable">b</span></a>)%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
(<a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#32263a1c8b01baecdff9deb038955bc9"><span class="id" title="notation">≠</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.fexp"><span class="id" title="variable">fexp</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.relative_error_conversion.rnd"><span class="id" title="variable">rnd</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0f8d5ec6876eafaec2dca3581c24e3a0"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#1cc22ba6849531267d3b25ca7b262449"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>)%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">eps</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a><br/>
(<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#eps"><span class="id" title="variable">eps</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#1cc22ba6849531267d3b25ca7b262449"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#b"><span class="id" title="variable">b</span></a>)%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a> <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.fexp"><span class="id" title="variable">fexp</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.relative_error_conversion.rnd"><span class="id" title="variable">rnd</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (<a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">(</span></a>1 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#7de2d195108bdf12ab090711a555a032"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#eps"><span class="id" title="variable">eps</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">)</span></a>)%<span class="id" title="var">R</span>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="relative_error_le_conversion"><span class="id" title="lemma">relative_error_le_conversion</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">b</span>, (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#b"><span class="id" title="variable">b</span></a>)%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
(<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.fexp"><span class="id" title="variable">fexp</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.relative_error_conversion.rnd"><span class="id" title="variable">rnd</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0f8d5ec6876eafaec2dca3581c24e3a0"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>)%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">eps</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a><br/>
(<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#eps"><span class="id" title="variable">eps</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#b"><span class="id" title="variable">b</span></a>)%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a> <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.fexp"><span class="id" title="variable">fexp</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.relative_error_conversion.rnd"><span class="id" title="variable">rnd</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (<a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">(</span></a>1 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#7de2d195108bdf12ab090711a555a032"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#eps"><span class="id" title="variable">eps</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">)</span></a>)%<span class="id" title="var">R</span>.<br/>
<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.relative_error_conversion"><span class="id" title="section">relative_error_conversion</span></a>.<br/>
<br/>
<span class="id" title="keyword">Variable</span> <a name="Fprop_relative.Fprop_relative_generic.emin"><span class="id" title="variable">emin</span></a> <a name="Fprop_relative.Fprop_relative_generic.p"><span class="id" title="variable">p</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a>.<br/>
<span class="id" title="keyword">Hypothesis</span> <a name="Fprop_relative.Fprop_relative_generic.Hmin"><span class="id" title="variable">Hmin</span></a> : <span class="id" title="keyword">∀</span> <span class="id" title="var">k</span>, (<a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.emin"><span class="id" title="variable">emin</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#k"><span class="id" title="variable">k</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> (<a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#208bafb0e148fe7fb7dcd812c227f4ee"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#239a40728d107295b3cb2c790f57f9e9"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.fexp"><span class="id" title="variable">fexp</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#k"><span class="id" title="variable">k</span></a>)%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">Variable</span> <a name="Fprop_relative.Fprop_relative_generic.rnd"><span class="id" title="variable">rnd</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a>.<br/>
<span class="id" title="keyword">Context</span> { <span class="id" title="var">valid_rnd</span> : <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Valid_rnd"><span class="id" title="class">Valid_rnd</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.rnd"><span class="id" title="variable">rnd</span></a> }.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="relative_error"><span class="id" title="lemma">relative_error</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>,<br/>
(<a class="idref" href="Flocq.Prop.Fprop_relative.html#bpow"><span class="id" title="abbreviation">bpow</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.emin"><span class="id" title="variable">emin</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>)%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
(<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.fexp"><span class="id" title="variable">fexp</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.rnd"><span class="id" title="variable">rnd</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0f8d5ec6876eafaec2dca3581c24e3a0"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#1cc22ba6849531267d3b25ca7b262449"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#bpow"><span class="id" title="abbreviation">bpow</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>)%<span class="id" title="var">R</span>.<br/>
<br/>
</div>
<div class="doc">
1+ε property in any rounding
</div>
<div class="code">
<span class="id" title="keyword">Theorem</span> <a name="relative_error_ex"><span class="id" title="lemma">relative_error_ex</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>,<br/>
(<a class="idref" href="Flocq.Prop.Fprop_relative.html#bpow"><span class="id" title="abbreviation">bpow</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.emin"><span class="id" title="variable">emin</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>)%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">eps</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a><br/>
(<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#eps"><span class="id" title="variable">eps</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#1cc22ba6849531267d3b25ca7b262449"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#bpow"><span class="id" title="abbreviation">bpow</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1))%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a> <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.fexp"><span class="id" title="variable">fexp</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.rnd"><span class="id" title="variable">rnd</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (<a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">(</span></a>1 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#7de2d195108bdf12ab090711a555a032"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#eps"><span class="id" title="variable">eps</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">)</span></a>)%<span class="id" title="var">R</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="relative_error_F2R_emin"><span class="id" title="lemma">relative_error_F2R_emin</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">m</span>, <span class="id" title="keyword">let</span> <span class="id" title="var">x</span> := <a class="idref" href="Flocq.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> (<a class="idref" href="Flocq.Core.Fcore_defs.html#Float"><span class="id" title="constructor">Float</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Prop.Fprop_relative.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.emin"><span class="id" title="variable">emin</span></a>) <span class="id" title="keyword">in</span><br/>
(<a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#32263a1c8b01baecdff9deb038955bc9"><span class="id" title="notation">≠</span></a> 0)%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
(<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.fexp"><span class="id" title="variable">fexp</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.rnd"><span class="id" title="variable">rnd</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0f8d5ec6876eafaec2dca3581c24e3a0"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#1cc22ba6849531267d3b25ca7b262449"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#bpow"><span class="id" title="abbreviation">bpow</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>)%<span class="id" title="var">R</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="relative_error_F2R_emin_ex"><span class="id" title="lemma">relative_error_F2R_emin_ex</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">m</span>, <span class="id" title="keyword">let</span> <span class="id" title="var">x</span> := <a class="idref" href="Flocq.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> (<a class="idref" href="Flocq.Core.Fcore_defs.html#Float"><span class="id" title="constructor">Float</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Prop.Fprop_relative.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.emin"><span class="id" title="variable">emin</span></a>) <span class="id" title="keyword">in</span><br/>
<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">eps</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a><br/>
(<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#eps"><span class="id" title="variable">eps</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#1cc22ba6849531267d3b25ca7b262449"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#bpow"><span class="id" title="abbreviation">bpow</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1))%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a> <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.fexp"><span class="id" title="variable">fexp</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.rnd"><span class="id" title="variable">rnd</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (<a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">(</span></a>1 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#7de2d195108bdf12ab090711a555a032"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#eps"><span class="id" title="variable">eps</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">)</span></a>)%<span class="id" title="var">R</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="relative_error_round"><span class="id" title="lemma">relative_error_round</span></a> :<br/>
(0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.p"><span class="id" title="variable">p</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>,<br/>
(<a class="idref" href="Flocq.Prop.Fprop_relative.html#bpow"><span class="id" title="abbreviation">bpow</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.emin"><span class="id" title="variable">emin</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>)%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
(<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.fexp"><span class="id" title="variable">fexp</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.rnd"><span class="id" title="variable">rnd</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0f8d5ec6876eafaec2dca3581c24e3a0"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#1cc22ba6849531267d3b25ca7b262449"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#bpow"><span class="id" title="abbreviation">bpow</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.fexp"><span class="id" title="variable">fexp</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.rnd"><span class="id" title="variable">rnd</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>))%<span class="id" title="var">R</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="relative_error_round_F2R_emin"><span class="id" title="lemma">relative_error_round_F2R_emin</span></a> :<br/>
(0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.p"><span class="id" title="variable">p</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">m</span>, <span class="id" title="keyword">let</span> <span class="id" title="var">x</span> := <a class="idref" href="Flocq.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> (<a class="idref" href="Flocq.Core.Fcore_defs.html#Float"><span class="id" title="constructor">Float</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Prop.Fprop_relative.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.emin"><span class="id" title="variable">emin</span></a>) <span class="id" title="keyword">in</span><br/>
(<a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#32263a1c8b01baecdff9deb038955bc9"><span class="id" title="notation">≠</span></a> 0)%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
(<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.fexp"><span class="id" title="variable">fexp</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.rnd"><span class="id" title="variable">rnd</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0f8d5ec6876eafaec2dca3581c24e3a0"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#1cc22ba6849531267d3b25ca7b262449"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#bpow"><span class="id" title="abbreviation">bpow</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.fexp"><span class="id" title="variable">fexp</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.rnd"><span class="id" title="variable">rnd</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>))%<span class="id" title="var">R</span>.<br/>
<br/>
<span class="id" title="keyword">Variable</span> <a name="Fprop_relative.Fprop_relative_generic.choice"><span class="id" title="variable">choice</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="relative_error_N"><span class="id" title="lemma">relative_error_N</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>,<br/>
(<a class="idref" href="Flocq.Prop.Fprop_relative.html#bpow"><span class="id" title="abbreviation">bpow</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.emin"><span class="id" title="variable">emin</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>)%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
(<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.fexp"><span class="id" title="variable">fexp</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Znearest"><span class="id" title="definition">Znearest</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.choice"><span class="id" title="variable">choice</span></a>) <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0f8d5ec6876eafaec2dca3581c24e3a0"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#2f596a539cf733f1c05f7537bd65e225"><span class="id" title="notation">/</span></a>2 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#bpow"><span class="id" title="abbreviation">bpow</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>)%<span class="id" title="var">R</span>.<br/>
<br/>
</div>
<div class="doc">
1+ε property in rounding to nearest
</div>
<div class="code">
<span class="id" title="keyword">Theorem</span> <a name="relative_error_N_ex"><span class="id" title="lemma">relative_error_N_ex</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>,<br/>
(<a class="idref" href="Flocq.Prop.Fprop_relative.html#bpow"><span class="id" title="abbreviation">bpow</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.emin"><span class="id" title="variable">emin</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>)%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">eps</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a><br/>
(<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#eps"><span class="id" title="variable">eps</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#2f596a539cf733f1c05f7537bd65e225"><span class="id" title="notation">/</span></a>2 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#bpow"><span class="id" title="abbreviation">bpow</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1))%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a> <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.fexp"><span class="id" title="variable">fexp</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Znearest"><span class="id" title="definition">Znearest</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.choice"><span class="id" title="variable">choice</span></a>) <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (<a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">(</span></a>1 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#7de2d195108bdf12ab090711a555a032"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#eps"><span class="id" title="variable">eps</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">)</span></a>)%<span class="id" title="var">R</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="relative_error_N_F2R_emin"><span class="id" title="lemma">relative_error_N_F2R_emin</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">m</span>, <span class="id" title="keyword">let</span> <span class="id" title="var">x</span> := <a class="idref" href="Flocq.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> (<a class="idref" href="Flocq.Core.Fcore_defs.html#Float"><span class="id" title="constructor">Float</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Prop.Fprop_relative.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.emin"><span class="id" title="variable">emin</span></a>) <span class="id" title="keyword">in</span><br/>
(<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.fexp"><span class="id" title="variable">fexp</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Znearest"><span class="id" title="definition">Znearest</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.choice"><span class="id" title="variable">choice</span></a>) <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0f8d5ec6876eafaec2dca3581c24e3a0"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#2f596a539cf733f1c05f7537bd65e225"><span class="id" title="notation">/</span></a>2 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#bpow"><span class="id" title="abbreviation">bpow</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>)%<span class="id" title="var">R</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="relative_error_N_F2R_emin_ex"><span class="id" title="lemma">relative_error_N_F2R_emin_ex</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">m</span>, <span class="id" title="keyword">let</span> <span class="id" title="var">x</span> := <a class="idref" href="Flocq.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> (<a class="idref" href="Flocq.Core.Fcore_defs.html#Float"><span class="id" title="constructor">Float</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Prop.Fprop_relative.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.emin"><span class="id" title="variable">emin</span></a>) <span class="id" title="keyword">in</span><br/>
<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">eps</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a><br/>
(<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#eps"><span class="id" title="variable">eps</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#2f596a539cf733f1c05f7537bd65e225"><span class="id" title="notation">/</span></a>2 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#bpow"><span class="id" title="abbreviation">bpow</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1))%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a> <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.fexp"><span class="id" title="variable">fexp</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Znearest"><span class="id" title="definition">Znearest</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.choice"><span class="id" title="variable">choice</span></a>) <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (<a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">(</span></a>1 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#7de2d195108bdf12ab090711a555a032"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#eps"><span class="id" title="variable">eps</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">)</span></a>)%<span class="id" title="var">R</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="relative_error_N_round"><span class="id" title="lemma">relative_error_N_round</span></a> :<br/>
(0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.p"><span class="id" title="variable">p</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>,<br/>
(<a class="idref" href="Flocq.Prop.Fprop_relative.html#bpow"><span class="id" title="abbreviation">bpow</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.emin"><span class="id" title="variable">emin</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>)%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
(<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.fexp"><span class="id" title="variable">fexp</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Znearest"><span class="id" title="definition">Znearest</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.choice"><span class="id" title="variable">choice</span></a>) <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0f8d5ec6876eafaec2dca3581c24e3a0"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#2f596a539cf733f1c05f7537bd65e225"><span class="id" title="notation">/</span></a>2 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#bpow"><span class="id" title="abbreviation">bpow</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.fexp"><span class="id" title="variable">fexp</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Znearest"><span class="id" title="definition">Znearest</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.choice"><span class="id" title="variable">choice</span></a>) <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>))%<span class="id" title="var">R</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="relative_error_N_round_F2R_emin"><span class="id" title="lemma">relative_error_N_round_F2R_emin</span></a> :<br/>
(0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.p"><span class="id" title="variable">p</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">m</span>, <span class="id" title="keyword">let</span> <span class="id" title="var">x</span> := <a class="idref" href="Flocq.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> (<a class="idref" href="Flocq.Core.Fcore_defs.html#Float"><span class="id" title="constructor">Float</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Prop.Fprop_relative.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.emin"><span class="id" title="variable">emin</span></a>) <span class="id" title="keyword">in</span><br/>
(<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.fexp"><span class="id" title="variable">fexp</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Znearest"><span class="id" title="definition">Znearest</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.choice"><span class="id" title="variable">choice</span></a>) <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0f8d5ec6876eafaec2dca3581c24e3a0"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#2f596a539cf733f1c05f7537bd65e225"><span class="id" title="notation">/</span></a>2 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#bpow"><span class="id" title="abbreviation">bpow</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.fexp"><span class="id" title="variable">fexp</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Znearest"><span class="id" title="definition">Znearest</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic.choice"><span class="id" title="variable">choice</span></a>) <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>))%<span class="id" title="var">R</span>.<br/>
<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_generic"><span class="id" title="section">Fprop_relative_generic</span></a>.<br/>
<br/>
<span class="id" title="keyword">Section</span> <a name="Fprop_relative.Fprop_relative_FLT"><span class="id" title="section">Fprop_relative_FLT</span></a>.<br/>
<br/>
<span class="id" title="keyword">Variable</span> <a name="Fprop_relative.Fprop_relative_FLT.emin"><span class="id" title="variable">emin</span></a> <a name="Fprop_relative.Fprop_relative_FLT.prec"><span class="id" title="variable">prec</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a>.<br/>
<span class="id" title="keyword">Variable</span> <a name="Fprop_relative.Fprop_relative_FLT.Hp"><span class="id" title="variable">Hp</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Zlt"><span class="id" title="abbreviation">Zlt</span></a> 0 <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.prec"><span class="id" title="variable">prec</span></a>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="relative_error_FLT_aux"><span class="id" title="lemma">relative_error_FLT_aux</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">k</span>, (<a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.emin"><span class="id" title="variable">emin</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.prec"><span class="id" title="variable">prec</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#239a40728d107295b3cb2c790f57f9e9"><span class="id" title="notation">-</span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#k"><span class="id" title="variable">k</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> (<a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.prec"><span class="id" title="variable">prec</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#208bafb0e148fe7fb7dcd812c227f4ee"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#239a40728d107295b3cb2c790f57f9e9"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Core.Fcore_FLT.html#FLT_exp"><span class="id" title="definition">FLT_exp</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.emin"><span class="id" title="variable">emin</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.prec"><span class="id" title="variable">prec</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#k"><span class="id" title="variable">k</span></a>)%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">Variable</span> <a name="Fprop_relative.Fprop_relative_FLT.rnd"><span class="id" title="variable">rnd</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a>.<br/>
<span class="id" title="keyword">Context</span> { <span class="id" title="var">valid_rnd</span> : <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Valid_rnd"><span class="id" title="class">Valid_rnd</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.rnd"><span class="id" title="variable">rnd</span></a> }.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="relative_error_FLT"><span class="id" title="lemma">relative_error_FLT</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>,<br/>
(<a class="idref" href="Flocq.Prop.Fprop_relative.html#bpow"><span class="id" title="abbreviation">bpow</span></a> (<a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.emin"><span class="id" title="variable">emin</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.prec"><span class="id" title="variable">prec</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#239a40728d107295b3cb2c790f57f9e9"><span class="id" title="notation">-</span></a> 1) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>)%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
(<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> (<a class="idref" href="Flocq.Core.Fcore_FLT.html#FLT_exp"><span class="id" title="definition">FLT_exp</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.emin"><span class="id" title="variable">emin</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.prec"><span class="id" title="variable">prec</span></a>) <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.rnd"><span class="id" title="variable">rnd</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0f8d5ec6876eafaec2dca3581c24e3a0"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#1cc22ba6849531267d3b25ca7b262449"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#bpow"><span class="id" title="abbreviation">bpow</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.prec"><span class="id" title="variable">prec</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>)%<span class="id" title="var">R</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="relative_error_FLT_F2R_emin"><span class="id" title="lemma">relative_error_FLT_F2R_emin</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">m</span>, <span class="id" title="keyword">let</span> <span class="id" title="var">x</span> := <a class="idref" href="Flocq.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> (<a class="idref" href="Flocq.Core.Fcore_defs.html#Float"><span class="id" title="constructor">Float</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Prop.Fprop_relative.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.emin"><span class="id" title="variable">emin</span></a>) <span class="id" title="keyword">in</span><br/>
(<a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#32263a1c8b01baecdff9deb038955bc9"><span class="id" title="notation">≠</span></a> 0)%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
(<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> (<a class="idref" href="Flocq.Core.Fcore_FLT.html#FLT_exp"><span class="id" title="definition">FLT_exp</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.emin"><span class="id" title="variable">emin</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.prec"><span class="id" title="variable">prec</span></a>) <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.rnd"><span class="id" title="variable">rnd</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0f8d5ec6876eafaec2dca3581c24e3a0"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#1cc22ba6849531267d3b25ca7b262449"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#bpow"><span class="id" title="abbreviation">bpow</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.prec"><span class="id" title="variable">prec</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>)%<span class="id" title="var">R</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="relative_error_FLT_F2R_emin_ex"><span class="id" title="lemma">relative_error_FLT_F2R_emin_ex</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">m</span>, <span class="id" title="keyword">let</span> <span class="id" title="var">x</span> := <a class="idref" href="Flocq.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> (<a class="idref" href="Flocq.Core.Fcore_defs.html#Float"><span class="id" title="constructor">Float</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Prop.Fprop_relative.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.emin"><span class="id" title="variable">emin</span></a>) <span class="id" title="keyword">in</span><br/>
<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">eps</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a><br/>
(<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#eps"><span class="id" title="variable">eps</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#1cc22ba6849531267d3b25ca7b262449"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#bpow"><span class="id" title="abbreviation">bpow</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.prec"><span class="id" title="variable">prec</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1))%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a> <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> (<a class="idref" href="Flocq.Core.Fcore_FLT.html#FLT_exp"><span class="id" title="definition">FLT_exp</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.emin"><span class="id" title="variable">emin</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.prec"><span class="id" title="variable">prec</span></a>) <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.rnd"><span class="id" title="variable">rnd</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (<a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">(</span></a>1 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#7de2d195108bdf12ab090711a555a032"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#eps"><span class="id" title="variable">eps</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">)</span></a>)%<span class="id" title="var">R</span>.<br/>
<br/>
</div>
<div class="doc">
1+ε property in any rounding in FLT
</div>
<div class="code">
<span class="id" title="keyword">Theorem</span> <a name="relative_error_FLT_ex"><span class="id" title="lemma">relative_error_FLT_ex</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>,<br/>
(<a class="idref" href="Flocq.Prop.Fprop_relative.html#bpow"><span class="id" title="abbreviation">bpow</span></a> (<a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.emin"><span class="id" title="variable">emin</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.prec"><span class="id" title="variable">prec</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#239a40728d107295b3cb2c790f57f9e9"><span class="id" title="notation">-</span></a> 1) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>)%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">eps</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a><br/>
(<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#eps"><span class="id" title="variable">eps</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#1cc22ba6849531267d3b25ca7b262449"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#bpow"><span class="id" title="abbreviation">bpow</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.prec"><span class="id" title="variable">prec</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1))%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a> <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> (<a class="idref" href="Flocq.Core.Fcore_FLT.html#FLT_exp"><span class="id" title="definition">FLT_exp</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.emin"><span class="id" title="variable">emin</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.prec"><span class="id" title="variable">prec</span></a>) <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.rnd"><span class="id" title="variable">rnd</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (<a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">(</span></a>1 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#7de2d195108bdf12ab090711a555a032"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#eps"><span class="id" title="variable">eps</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">)</span></a>)%<span class="id" title="var">R</span>.<br/>
<br/>
<span class="id" title="keyword">Variable</span> <a name="Fprop_relative.Fprop_relative_FLT.choice"><span class="id" title="variable">choice</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="relative_error_N_FLT"><span class="id" title="lemma">relative_error_N_FLT</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>,<br/>
(<a class="idref" href="Flocq.Prop.Fprop_relative.html#bpow"><span class="id" title="abbreviation">bpow</span></a> (<a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.emin"><span class="id" title="variable">emin</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.prec"><span class="id" title="variable">prec</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#239a40728d107295b3cb2c790f57f9e9"><span class="id" title="notation">-</span></a> 1) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>)%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
(<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> (<a class="idref" href="Flocq.Core.Fcore_FLT.html#FLT_exp"><span class="id" title="definition">FLT_exp</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.emin"><span class="id" title="variable">emin</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.prec"><span class="id" title="variable">prec</span></a>) (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Znearest"><span class="id" title="definition">Znearest</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.choice"><span class="id" title="variable">choice</span></a>) <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0f8d5ec6876eafaec2dca3581c24e3a0"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#2f596a539cf733f1c05f7537bd65e225"><span class="id" title="notation">/</span></a>2 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#bpow"><span class="id" title="abbreviation">bpow</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.prec"><span class="id" title="variable">prec</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>)%<span class="id" title="var">R</span>.<br/>
<br/>
</div>
<div class="doc">
1+ε property in rounding to nearest in FLT
</div>
<div class="code">
<span class="id" title="keyword">Theorem</span> <a name="relative_error_N_FLT_ex"><span class="id" title="lemma">relative_error_N_FLT_ex</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>,<br/>
(<a class="idref" href="Flocq.Prop.Fprop_relative.html#bpow"><span class="id" title="abbreviation">bpow</span></a> (<a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.emin"><span class="id" title="variable">emin</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.prec"><span class="id" title="variable">prec</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#239a40728d107295b3cb2c790f57f9e9"><span class="id" title="notation">-</span></a> 1) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>)%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">eps</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a><br/>
(<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#eps"><span class="id" title="variable">eps</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#2f596a539cf733f1c05f7537bd65e225"><span class="id" title="notation">/</span></a>2 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#bpow"><span class="id" title="abbreviation">bpow</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.prec"><span class="id" title="variable">prec</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1))%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a> <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> (<a class="idref" href="Flocq.Core.Fcore_FLT.html#FLT_exp"><span class="id" title="definition">FLT_exp</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.emin"><span class="id" title="variable">emin</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.prec"><span class="id" title="variable">prec</span></a>) (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Znearest"><span class="id" title="definition">Znearest</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.choice"><span class="id" title="variable">choice</span></a>) <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (<a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">(</span></a>1 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#7de2d195108bdf12ab090711a555a032"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#eps"><span class="id" title="variable">eps</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">)</span></a>)%<span class="id" title="var">R</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="relative_error_N_FLT_round"><span class="id" title="lemma">relative_error_N_FLT_round</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>,<br/>
(<a class="idref" href="Flocq.Prop.Fprop_relative.html#bpow"><span class="id" title="abbreviation">bpow</span></a> (<a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.emin"><span class="id" title="variable">emin</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.prec"><span class="id" title="variable">prec</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#239a40728d107295b3cb2c790f57f9e9"><span class="id" title="notation">-</span></a> 1) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>)%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
(<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> (<a class="idref" href="Flocq.Core.Fcore_FLT.html#FLT_exp"><span class="id" title="definition">FLT_exp</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.emin"><span class="id" title="variable">emin</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.prec"><span class="id" title="variable">prec</span></a>) (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Znearest"><span class="id" title="definition">Znearest</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.choice"><span class="id" title="variable">choice</span></a>) <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0f8d5ec6876eafaec2dca3581c24e3a0"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#2f596a539cf733f1c05f7537bd65e225"><span class="id" title="notation">/</span></a>2 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#bpow"><span class="id" title="abbreviation">bpow</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.prec"><span class="id" title="variable">prec</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> (<a class="idref" href="Flocq.Core.Fcore_FLT.html#FLT_exp"><span class="id" title="definition">FLT_exp</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.emin"><span class="id" title="variable">emin</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.prec"><span class="id" title="variable">prec</span></a>) (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Znearest"><span class="id" title="definition">Znearest</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.choice"><span class="id" title="variable">choice</span></a>) <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>))%<span class="id" title="var">R</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="relative_error_N_FLT_F2R_emin"><span class="id" title="lemma">relative_error_N_FLT_F2R_emin</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">m</span>, <span class="id" title="keyword">let</span> <span class="id" title="var">x</span> := <a class="idref" href="Flocq.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> (<a class="idref" href="Flocq.Core.Fcore_defs.html#Float"><span class="id" title="constructor">Float</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Prop.Fprop_relative.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.emin"><span class="id" title="variable">emin</span></a>) <span class="id" title="keyword">in</span><br/>
(<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> (<a class="idref" href="Flocq.Core.Fcore_FLT.html#FLT_exp"><span class="id" title="definition">FLT_exp</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.emin"><span class="id" title="variable">emin</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.prec"><span class="id" title="variable">prec</span></a>) (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Znearest"><span class="id" title="definition">Znearest</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.choice"><span class="id" title="variable">choice</span></a>) <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0f8d5ec6876eafaec2dca3581c24e3a0"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#2f596a539cf733f1c05f7537bd65e225"><span class="id" title="notation">/</span></a>2 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#bpow"><span class="id" title="abbreviation">bpow</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.prec"><span class="id" title="variable">prec</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>)%<span class="id" title="var">R</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="relative_error_N_FLT_F2R_emin_ex"><span class="id" title="lemma">relative_error_N_FLT_F2R_emin_ex</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">m</span>, <span class="id" title="keyword">let</span> <span class="id" title="var">x</span> := <a class="idref" href="Flocq.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> (<a class="idref" href="Flocq.Core.Fcore_defs.html#Float"><span class="id" title="constructor">Float</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Prop.Fprop_relative.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.emin"><span class="id" title="variable">emin</span></a>) <span class="id" title="keyword">in</span><br/>
<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">eps</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a><br/>
(<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#eps"><span class="id" title="variable">eps</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#2f596a539cf733f1c05f7537bd65e225"><span class="id" title="notation">/</span></a>2 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#bpow"><span class="id" title="abbreviation">bpow</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.prec"><span class="id" title="variable">prec</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1))%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a> <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> (<a class="idref" href="Flocq.Core.Fcore_FLT.html#FLT_exp"><span class="id" title="definition">FLT_exp</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.emin"><span class="id" title="variable">emin</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.prec"><span class="id" title="variable">prec</span></a>) (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Znearest"><span class="id" title="definition">Znearest</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.choice"><span class="id" title="variable">choice</span></a>) <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (<a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">(</span></a>1 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#7de2d195108bdf12ab090711a555a032"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#eps"><span class="id" title="variable">eps</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">)</span></a>)%<span class="id" title="var">R</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="relative_error_N_FLT_round_F2R_emin"><span class="id" title="lemma">relative_error_N_FLT_round_F2R_emin</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">m</span>, <span class="id" title="keyword">let</span> <span class="id" title="var">x</span> := <a class="idref" href="Flocq.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> (<a class="idref" href="Flocq.Core.Fcore_defs.html#Float"><span class="id" title="constructor">Float</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Prop.Fprop_relative.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.emin"><span class="id" title="variable">emin</span></a>) <span class="id" title="keyword">in</span><br/>
(<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> (<a class="idref" href="Flocq.Core.Fcore_FLT.html#FLT_exp"><span class="id" title="definition">FLT_exp</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.emin"><span class="id" title="variable">emin</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.prec"><span class="id" title="variable">prec</span></a>) (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Znearest"><span class="id" title="definition">Znearest</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.choice"><span class="id" title="variable">choice</span></a>) <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0f8d5ec6876eafaec2dca3581c24e3a0"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#2f596a539cf733f1c05f7537bd65e225"><span class="id" title="notation">/</span></a>2 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#bpow"><span class="id" title="abbreviation">bpow</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.prec"><span class="id" title="variable">prec</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> (<a class="idref" href="Flocq.Core.Fcore_FLT.html#FLT_exp"><span class="id" title="definition">FLT_exp</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.emin"><span class="id" title="variable">emin</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.prec"><span class="id" title="variable">prec</span></a>) (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Znearest"><span class="id" title="definition">Znearest</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.choice"><span class="id" title="variable">choice</span></a>) <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>))%<span class="id" title="var">R</span>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="error_N_FLT_aux"><span class="id" title="lemma">error_N_FLT_aux</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>,<br/>
(0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#1cc22ba6849531267d3b25ca7b262449"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>)%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">eps</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">eta</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a><br/>
(<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#eps"><span class="id" title="variable">eps</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#2f596a539cf733f1c05f7537bd65e225"><span class="id" title="notation">/</span></a>2 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#bpow"><span class="id" title="abbreviation">bpow</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.prec"><span class="id" title="variable">prec</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1))%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a><br/>
(<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#eta"><span class="id" title="variable">eta</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#2f596a539cf733f1c05f7537bd65e225"><span class="id" title="notation">/</span></a>2 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#bpow"><span class="id" title="abbreviation">bpow</span></a> (<a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.emin"><span class="id" title="variable">emin</span></a>))%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a><br/>
(<a class="idref" href="Flocq.Prop.Fprop_relative.html#eps"><span class="id" title="variable">eps</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a><a class="idref" href="Flocq.Prop.Fprop_relative.html#eta"><span class="id" title="variable">eta</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a>0)%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> (<a class="idref" href="Flocq.Core.Fcore_FLT.html#FLT_exp"><span class="id" title="definition">FLT_exp</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.emin"><span class="id" title="variable">emin</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.prec"><span class="id" title="variable">prec</span></a>) (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Znearest"><span class="id" title="definition">Znearest</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT.choice"><span class="id" title="variable">choice</span></a>) <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (<a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">(</span></a>1 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#7de2d195108bdf12ab090711a555a032"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#eps"><span class="id" title="variable">eps</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#7de2d195108bdf12ab090711a555a032"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#eta"><span class="id" title="variable">eta</span></a>)%<span class="id" title="var">R</span>.<br/>
<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLT"><span class="id" title="section">Fprop_relative_FLT</span></a>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="error_N_FLT"><span class="id" title="lemma">error_N_FLT</span></a> :<br/>
<span class="id" title="keyword">∀</span> (<span class="id" title="var">emin</span> <span class="id" title="var">prec</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a>), (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#prec"><span class="id" title="variable">prec</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<span class="id" title="keyword">∀</span> (<span class="id" title="var">choice</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a>),<br/>
<span class="id" title="keyword">∀</span> (<span class="id" title="var">x</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a>),<br/>
<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">eps</span> <span class="id" title="var">eta</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a><br/>
(<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#eps"><span class="id" title="variable">eps</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#2f596a539cf733f1c05f7537bd65e225"><span class="id" title="notation">/</span></a>2 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#bpow"><span class="id" title="abbreviation">bpow</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Prop.Fprop_relative.html#prec"><span class="id" title="variable">prec</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1))%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a><br/>
(<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#eta"><span class="id" title="variable">eta</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#2f596a539cf733f1c05f7537bd65e225"><span class="id" title="notation">/</span></a>2 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#bpow"><span class="id" title="abbreviation">bpow</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#emin"><span class="id" title="variable">emin</span></a>)%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a><br/>
(<a class="idref" href="Flocq.Prop.Fprop_relative.html#eps"><span class="id" title="variable">eps</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#eta"><span class="id" title="variable">eta</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 0)%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a><br/>
(<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> (<a class="idref" href="Flocq.Core.Fcore_FLT.html#FLT_exp"><span class="id" title="definition">FLT_exp</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#emin"><span class="id" title="variable">emin</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#prec"><span class="id" title="variable">prec</span></a>) (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Znearest"><span class="id" title="definition">Znearest</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#choice"><span class="id" title="variable">choice</span></a>) <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a><br/>
<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">(</span></a>1 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#7de2d195108bdf12ab090711a555a032"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#eps"><span class="id" title="variable">eps</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#7de2d195108bdf12ab090711a555a032"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#eta"><span class="id" title="variable">eta</span></a>)%<span class="id" title="var">R</span>.<br/>
<br/>
<span class="id" title="keyword">Section</span> <a name="Fprop_relative.Fprop_relative_FLX"><span class="id" title="section">Fprop_relative_FLX</span></a>.<br/>
<br/>
<span class="id" title="keyword">Variable</span> <a name="Fprop_relative.Fprop_relative_FLX.prec"><span class="id" title="variable">prec</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a>.<br/>
<span class="id" title="keyword">Variable</span> <a name="Fprop_relative.Fprop_relative_FLX.Hp"><span class="id" title="variable">Hp</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Zlt"><span class="id" title="abbreviation">Zlt</span></a> 0 <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLX.prec"><span class="id" title="variable">prec</span></a>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="relative_error_FLX_aux"><span class="id" title="lemma">relative_error_FLX_aux</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">k</span>, (<a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLX.prec"><span class="id" title="variable">prec</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#208bafb0e148fe7fb7dcd812c227f4ee"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#239a40728d107295b3cb2c790f57f9e9"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Core.Fcore_FLX.html#FLX_exp"><span class="id" title="definition">FLX_exp</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLX.prec"><span class="id" title="variable">prec</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#k"><span class="id" title="variable">k</span></a>)%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">Variable</span> <a name="Fprop_relative.Fprop_relative_FLX.rnd"><span class="id" title="variable">rnd</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a>.<br/>
<span class="id" title="keyword">Context</span> { <span class="id" title="var">valid_rnd</span> : <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Valid_rnd"><span class="id" title="class">Valid_rnd</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLX.rnd"><span class="id" title="variable">rnd</span></a> }.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="relative_error_FLX"><span class="id" title="lemma">relative_error_FLX</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>,<br/>
(<a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#32263a1c8b01baecdff9deb038955bc9"><span class="id" title="notation">≠</span></a> 0)%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
(<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> (<a class="idref" href="Flocq.Core.Fcore_FLX.html#FLX_exp"><span class="id" title="definition">FLX_exp</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLX.prec"><span class="id" title="variable">prec</span></a>) <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLX.rnd"><span class="id" title="variable">rnd</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0f8d5ec6876eafaec2dca3581c24e3a0"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#1cc22ba6849531267d3b25ca7b262449"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#bpow"><span class="id" title="abbreviation">bpow</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLX.prec"><span class="id" title="variable">prec</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>)%<span class="id" title="var">R</span>.<br/>
<br/>
</div>
<div class="doc">
1+ε property in any rounding in FLX
</div>
<div class="code">
<span class="id" title="keyword">Theorem</span> <a name="relative_error_FLX_ex"><span class="id" title="lemma">relative_error_FLX_ex</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>,<br/>
<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">eps</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a><br/>
(<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#eps"><span class="id" title="variable">eps</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#1cc22ba6849531267d3b25ca7b262449"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#bpow"><span class="id" title="abbreviation">bpow</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLX.prec"><span class="id" title="variable">prec</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1))%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a> <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> (<a class="idref" href="Flocq.Core.Fcore_FLX.html#FLX_exp"><span class="id" title="definition">FLX_exp</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLX.prec"><span class="id" title="variable">prec</span></a>) <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLX.rnd"><span class="id" title="variable">rnd</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (<a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">(</span></a>1 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#7de2d195108bdf12ab090711a555a032"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#eps"><span class="id" title="variable">eps</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">)</span></a>)%<span class="id" title="var">R</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="relative_error_FLX_round"><span class="id" title="lemma">relative_error_FLX_round</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>,<br/>
(<a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#32263a1c8b01baecdff9deb038955bc9"><span class="id" title="notation">≠</span></a> 0)%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
(<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> (<a class="idref" href="Flocq.Core.Fcore_FLX.html#FLX_exp"><span class="id" title="definition">FLX_exp</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLX.prec"><span class="id" title="variable">prec</span></a>) <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLX.rnd"><span class="id" title="variable">rnd</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0f8d5ec6876eafaec2dca3581c24e3a0"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#1cc22ba6849531267d3b25ca7b262449"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#bpow"><span class="id" title="abbreviation">bpow</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLX.prec"><span class="id" title="variable">prec</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> (<a class="idref" href="Flocq.Core.Fcore_FLX.html#FLX_exp"><span class="id" title="definition">FLX_exp</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLX.prec"><span class="id" title="variable">prec</span></a>) <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLX.rnd"><span class="id" title="variable">rnd</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>))%<span class="id" title="var">R</span>.<br/>
<br/>
<span class="id" title="keyword">Variable</span> <a name="Fprop_relative.Fprop_relative_FLX.choice"><span class="id" title="variable">choice</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="relative_error_N_FLX"><span class="id" title="lemma">relative_error_N_FLX</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>,<br/>
(<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> (<a class="idref" href="Flocq.Core.Fcore_FLX.html#FLX_exp"><span class="id" title="definition">FLX_exp</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLX.prec"><span class="id" title="variable">prec</span></a>) (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Znearest"><span class="id" title="definition">Znearest</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLX.choice"><span class="id" title="variable">choice</span></a>) <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0f8d5ec6876eafaec2dca3581c24e3a0"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#2f596a539cf733f1c05f7537bd65e225"><span class="id" title="notation">/</span></a>2 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#bpow"><span class="id" title="abbreviation">bpow</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLX.prec"><span class="id" title="variable">prec</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>)%<span class="id" title="var">R</span>.<br/>
<br/>
</div>
<div class="doc">
1+ε property in rounding to nearest in FLX
</div>
<div class="code">
<span class="id" title="keyword">Theorem</span> <a name="relative_error_N_FLX_ex"><span class="id" title="lemma">relative_error_N_FLX_ex</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>,<br/>
<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">eps</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a><br/>
(<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#eps"><span class="id" title="variable">eps</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#2f596a539cf733f1c05f7537bd65e225"><span class="id" title="notation">/</span></a>2 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#bpow"><span class="id" title="abbreviation">bpow</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLX.prec"><span class="id" title="variable">prec</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1))%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a> <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> (<a class="idref" href="Flocq.Core.Fcore_FLX.html#FLX_exp"><span class="id" title="definition">FLX_exp</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLX.prec"><span class="id" title="variable">prec</span></a>) (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Znearest"><span class="id" title="definition">Znearest</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLX.choice"><span class="id" title="variable">choice</span></a>) <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (<a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">(</span></a>1 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#7de2d195108bdf12ab090711a555a032"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#eps"><span class="id" title="variable">eps</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">)</span></a>)%<span class="id" title="var">R</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="relative_error_N_FLX_round"><span class="id" title="lemma">relative_error_N_FLX_round</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>,<br/>
(<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> (<a class="idref" href="Flocq.Core.Fcore_FLX.html#FLX_exp"><span class="id" title="definition">FLX_exp</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLX.prec"><span class="id" title="variable">prec</span></a>) (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Znearest"><span class="id" title="definition">Znearest</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLX.choice"><span class="id" title="variable">choice</span></a>) <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0f8d5ec6876eafaec2dca3581c24e3a0"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#2f596a539cf733f1c05f7537bd65e225"><span class="id" title="notation">/</span></a>2 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#bpow"><span class="id" title="abbreviation">bpow</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLX.prec"><span class="id" title="variable">prec</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> (<a class="idref" href="Flocq.Core.Fcore_FLX.html#FLX_exp"><span class="id" title="definition">FLX_exp</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLX.prec"><span class="id" title="variable">prec</span></a>) (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Znearest"><span class="id" title="definition">Znearest</span></a> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLX.choice"><span class="id" title="variable">choice</span></a>) <a class="idref" href="Flocq.Prop.Fprop_relative.html#x"><span class="id" title="variable">x</span></a>))%<span class="id" title="var">R</span>.<br/>
<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative.Fprop_relative_FLX"><span class="id" title="section">Fprop_relative_FLX</span></a>.<br/>
<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="Flocq.Prop.Fprop_relative.html#Fprop_relative"><span class="id" title="section">Fprop_relative</span></a>.<br/>
</div>
</div>
<div id="footer">
<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a>
</div>
</div>
</body>
</html>
distrib
>
Mageia
>
6
>
armv5tl
>
media
>
core-release
>
by-pkgid
>
3c7997fe0e8405f6d7b5563e63d17a78
>
files
>
101
