Mathlib.Analysis.Certified­Contour­Interval­Arithmetic.Complex

Given a rational argument and a natural-number fuel level, the arctangent Taylor partial sum is the alternating rational series through degree $2f+1$.

Given a rational argument and a natural-number fuel level, the arctangent remainder scale is $|q|^{2f+3}/(2f+3)$.

Given a rational argument and a natural-number fuel level, the raw arctangent interval has endpoints equal to the Taylor partial sum minus and plus the remainder scale, respectively.

Given a natural-number fuel level, the raw π interval is four times the difference between four times the arctangent interval at $1/5$ and the arctangent interval at $1/239$.

For a natural-number fuel level, the π interval at that level is the raw π interval at level zero, and at every successor level is the intersection of the preceding π interval and the new raw π interval.

Given a positive rational target width, the π precision is eight times one plus the denominator of that target.

The certified real name for π has exact value π, uses the recursively refined π intervals as approximations, and uses the specified π precision to achieve each requested positive rational width.

Given a rational argument and a natural-number fuel level, the sine Taylor partial sum is the alternating rational sine series through degree $2f+1$.

Given a rational argument and a natural-number fuel level, the sine remainder scale is $|q|^{2f+3}/(2f+3)!$.

Given a rational argument and a natural-number fuel level, the cosine Taylor partial sum is the alternating rational cosine series through degree $2f$.

Given a rational argument and a natural-number fuel level, the cosine remainder scale is $|q|^{2f+2}/(2f+2)!$.

Given a rational argument and a natural-number fuel level, the raw sine interval has endpoints equal to the sine Taylor partial sum minus and plus the sine remainder scale, respectively.

Given a rational argument and a natural-number fuel level, the raw cosine interval has endpoints equal to the cosine Taylor partial sum minus and plus the cosine remainder scale, respectively.

Given a rational interval, its rational midpoint is the arithmetic mean of its lower and upper endpoints.

Given a rational interval, its rational radius is half its width.

Given a rational input interval and a natural-number fuel level, the raw sine image interval expands the midpoint sine interval by the input interval's radius.

Given a rational input interval and a natural-number fuel level, the raw cosine image interval expands the midpoint cosine interval by the input interval's radius.

For a rational input interval and a natural-number fuel level, the sine image interval at that level is the raw sine image interval at level zero, and at every successor level is the intersection of the preceding sine image interval and the new raw sine image interval.

For a rational input interval and a natural-number fuel level, the cosine image interval at that level is the raw cosine image interval at level zero, and at every successor level is the intersection of the preceding cosine image interval and the new raw cosine image interval.

For a rational interval, its squared interval is the interval from the square of its upper endpoint to the square of its lower endpoint when it lies strictly below zero, the interval from the square of its lower endpoint to the square of its upper endpoint when it lies strictly above zero, and the interval from zero to the larger squared endpoint when it contains zero.

For a rational number, the Newton upper-iterate sequence assigns the absolute value of the number plus one at iteration zero and one half of the sum of the preceding iterate and the number divided by that iterate at each later iteration.

For a rational number and an iteration count, the Newton lower square-root bound is the number divided by its Newton upper iterate at that count.

For a rational interval whose lower endpoint is nonnegative and a Newton iteration count, the square-root interval has lower endpoint equal to the Newton lower bound of the original lower endpoint, upper endpoint equal to the Newton upper bound of the original upper endpoint, and valid endpoint order.

Given a rational complex rectangle, its width is the larger of the widths of its real and imaginary coordinate intervals.

Given a rational complex rectangle, its maximum coordinate endpoint magnitude is the larger of the maximum absolute endpoint magnitudes of its real and imaginary coordinate intervals.

Given a rational real coordinate and a rational imaginary coordinate, the complex point rectangle is the zero-width rectangle containing $x+iy$.

Given a rational complex rectangle, its negative rectangle negates both coordinate intervals.

Given a first rational complex rectangle and a second rational complex rectangle, their difference rectangle adds the first rectangle to the coordinatewise negative of the second.

Given two rational complex rectangles, their product rectangle is obtained from the Cartesian complex-product formula using outward rational interval operations on the coordinate intervals.

Given a rational complex rectangle, its conjugate rectangle retains its real coordinate interval and negates its imaginary coordinate interval.

Given a rational complex rectangle, its squared-modulus interval is the sum of the sign-aware squares of its real and imaginary coordinate intervals.

Given a numerator rectangle, a denominator rectangle, and evidence that the denominator's squared-modulus interval excludes zero, the guarded quotient rectangle is the product of the numerator rectangle and the denominator's conjugate, with both resulting coordinate intervals divided by the denominator's squared-modulus interval.

Given two rational complex rectangles, their coordinatewise tightening is formed by tightening the real coordinate intervals and tightening the imaginary coordinate intervals.

Given a complex rational rectangle and a natural-number square-root fuel level, applying the rational square-root bounds at that fuel level to the rectangle's squared-modulus interval produces an executable enclosure of the complex norm.

Given a rational input interval and a natural-number fuel level, the raw exponential image interval is the input midpoint, the scalar exponential interval at that midpoint, the upper endpoint of the scalar exponential interval at the input's maximum absolute endpoint magnitude, and the midpoint exponential interval expanded by that upper bound times the input radius.

For a rational input interval and a natural-number fuel level, the exponential image interval at that level is the raw exponential image interval at level zero, and at every successor level is the intersection of the preceding exponential image interval and the new raw exponential image interval.

For a certified complex name and a requested positive rational tolerance, the refined rational rectangle is the rectangle selected by that name's tolerance-to-fuel rule.

For a rational real coordinate and a rational imaginary coordinate, the certified complex name of their complex point has that point as its exact value and the corresponding singleton rectangle at every fuel level.

For two certified complex names, their certified sum denotes the sum of their exact complex values and uses the coordinatewise sum of their equal-fuel rectangles.

For a certified complex name, the modulus approximation at each nonnegative fuel level is computed recursively: at zero it is the initial rectangle's modulus enclosure, and at each successor it is the intersection of the preceding approximation with the new modulus enclosure.

For a certified complex name and a requested positive rational tolerance, the modulus precision is the maximum of a fuel level that refines the input rectangle to a tolerance determined by its initial magnitude bound and an explicit Newton-iteration fuel bound.

For a certified complex name, its certified modulus name denotes the absolute value of its exact complex value and uses the recursive modulus enclosures with the stated precision rule.

Given a rational complex input rectangle and a natural-number fuel level, the raw complex-exponential rectangle multiplies the real-exponential interval of the real coordinate by the cosine and sine intervals of the imaginary coordinate to form its real and imaginary coordinates.

For a rational complex input rectangle and a natural-number fuel level, the complex-exponential rectangle at that level is the raw complex-exponential rectangle at level zero, and at every successor level is the intersection of the preceding rectangle and the new raw complex-exponential rectangle.

Given a certified complex number, its complex-exponential magnitude scale is two plus the absolute upper endpoint of the level-zero scalar-exponential interval evaluated at the maximum absolute real-coordinate endpoint of its level-zero enclosure.

Given a natural-number stage index, the complex-exponential stage tolerance is the positive rational number $1/(n+1)$.

Given a certified complex number and a natural-number stage index, the inner complex-exponential tolerance is the stage tolerance divided by sixteen times the complex-exponential magnitude scale.

Given a certified complex number and a natural-number stage index, the complex-exponential input tolerance is the inner tolerance divided by four times the complex-exponential magnitude scale.

Given a certified complex number and a natural-number stage index, the complex-exponential stage input rectangle is the input's approximation at the precision required by that stage's input tolerance.

Given a certified complex number and a natural-number stage index, the complex-exponential stage fuel is the stage input rectangle, the inner tolerance divided by eight, the resulting trigonometric Taylor-fuel bound, and the larger of that bound and the two scalar-exponential precision bounds.

Given a certified complex number and a natural-number stage index, the complex-exponential stage rectangle evaluates the complex exponential on that stage's input rectangle using that stage's fuel.

For a certified complex number and a natural-number stage index, the complex-exponential name approximation at that level is the stage-zero rectangle, and at every successor level is the intersection of the preceding name approximation and the new stage rectangle.

Given a certified complex number and a positive rational target width, the complex-exponential precision is the denominator of that target.

Given a certified complex number, the certified complex-exponential name has exact value the complex exponential of the input value, uses the recursively refined complex-exponential rectangles as approximations, and uses the stated precision rule for requested positive rational widths.

Given a positive rational tolerance, a natural-number operation count, a rational magnitude bound, and evidence that this bound is nonnegative, the canonical contour schedule allocates one third of the tolerance to each error budget and selects its input precision, mesh size, and fuel from the stated rational data.

Given a contour schedule, a mesh-endpoint index, and a primitive-operation index, the circle-node trace event records exactly those three quantities.

Given a contour schedule and a natural-number endpoint index, the rational rectangle enclosing the corresponding pure-imaginary circle angle has real coordinate zero and imaginary coordinate $2πk/m$, where $m$ is the schedule's mesh size.

Given a rational radius, a contour schedule, and a natural-number endpoint index, the scheduled circle-node rectangle is the rational-interval evaluation of $r\exp(2πik/m)$ using that schedule's angle enclosure and fuel.

Given a rational radius and a positive rational target width, the internal circle tolerance is the smaller of $\mathrm{target}/(256(|r|+1))$ and $1/1024$.

Given a rational radius and a positive rational target width, the circle input precision is the π-approximation precision selected for their internal circle tolerance.

Given a rational radius, a natural-number mesh size, and a positive rational target width, the circle exponential fuel is the larger of the zero-input exponential precision and an explicit trigonometric Taylor-fuel bound computed from the internal circle tolerance.

Given a rational radius, a contour schedule, and a natural-number endpoint index, the exact circle node is the complex number $r\exp(2πik/m)$, where $m$ is the schedule's mesh size.

For a contour program, the structural operation count of one contour node is the sum of the operation counts of its numerator and denominator maps plus two operations for guarded division and multiplication by the circle point.

Given a rational real numerator coordinate, a rational imaginary numerator coordinate, a rational circle radius, and the condition that the radius is strictly positive, the constant-over-unit contour program has the indicated constant numerator, unit denominator, and radius.

For a contour program, a schedule, and a nonnegative node index, the node rectangle is the scheduled rational rectangle for the circle point at that index.

For a contour program and a rational common error target, the pair of map-width bounds consists of the target plus the target multiplied by the numerator map's width amplification, and the analogous quantity for the denominator map. These are width bounds for a nonnegative target, which is how the evaluation uses them (with a positive rational target); a negative target gives negative numbers.

For a contour program, uniform bounds on its numerator and denominator values, a rational separation bound, and a rational common error target, the node-error propagation bound is obtained by forming the two map-width bounds, adding the numerator bound to its width bound, adding the denominator bound to its width bound, forming a bound for the division numerator, forming its width bound, forming the denominator squared-modulus width bound, forming the quotient width bound, forming the quotient magnitude bound, and combining quotient and circle-point errors. The quotient terms divide by the separation, so this is a valid propagation bound only for positive separation, as assumed by the soundness results; at separation zero those terms are zero by the division convention.

For a contour program, uniform bounds on its numerator and denominator values, and a positive rational separation bound, the node-error scale is one plus the absolute value of the node-error propagation bound evaluated at target one.

For a contour program, uniform bounds on its numerator and denominator values, a positive rational separation bound, and a positive rational tolerance, the canonical node target is the smaller of one and the tolerance divided by three times the node-error scale.

Given a rational real numerator coordinate, a rational imaginary numerator coordinate, a rational circle radius, and the condition that the radius is strictly positive, the value bounds for the constant-over-unit contour program bound its numerator coordinates by the larger absolute numerator coordinate and its denominator coordinates by one.