LAProof.accuracy_proofs.sum_is_finite

Finite Sum Boundedness

This file establishes conditions under which floating-point summation remains finite (non-infinite, non-NaN). The central contributions are:
  • is_finite_sum_no_overflow': a helper lemma showing that the floating-point sum is finite whenever both summands are finite and no overflow occurs.
  • fun_bnd: a bound on individual list elements sufficient to guarantee that their floating-point sum does not overflow. This bound decreases monotonically as the list length grows, reflecting the accumulation of rounding error.
  • fun_bnd_le: monotonicity of fun_bnd, showing that the per-element bound for a list of length S n is no greater than that for length n.
  • finite_sum_from_bounded: the main theorem. Given a list of finite floating-point values each bounded in absolute value, the floating-point sum fs satisfying sum_rel_Ft is finite. The proof proceeds by induction on the list, using the fun_bnd_le monotonicity lemma to discharge the inductive hypothesis and explicit rounding-error arithmetic to close the overflow bound.

From LAProof.accuracy_proofs Require Import
  preamble
  real_lemmas
  common
  dotprod_model
  sum_model
  float_acc_lems
  fma_dot_acc
  sum_acc.

Section NAN.

Variable NAN : FPCore.Nans.

Overflow-free addition preserves finiteness

If x and y are finite floating-point numbers and their sum does not overflow (in the sense of Bplus_no_overflow), then their sum is is finite.

Lemma is_finite_sum_no_overflow' (t : type) :
  ∀ (x y : ftype t)
         (Hfinx : Binary.is_finite x = true)
         (Hfiny : Binary.is_finite y = true)
         (Hov : @Bplus_no_overflow t (FT2R x) (FT2R y)),
    Binary.is_finite (BPLUS x y) = true.

Per-element bound for finite summation

fun_bnd t n is the maximum absolute value that each element of an n-element list may have while still guaranteeing that the floating-point sum of the list is finite. It is defined as
fmax t / (1 + default_rel t) * 1 / (1 + n * (g t (n-1) + 1))
where the function g encodes the standard (1 + eps)^k - 1 rounding-error growth factor.

Definition fun_bnd (t : type) (n : nat) :=
  (@fmax t) / (1 + @default_rel t) × 1 / (1 + INR n × (@g t (n - 1) + 1)).

Monotonicity of fun_bnd

The per-element bound is non-increasing in the list length: a longer list requires each element to be smaller to keep the sum finite.

Lemma fun_bnd_le (t : type) (n : nat) :
  fun_bnd t (S n) ≤ fun_bnd t n.

Main theorem: element-wise bound implies finite sum

If every element of l is finite and sufficiently bounded then the floating-point sum fs satisfying sum_rel_Ft l fs is finite.
The proof proceeds by induction on l, using fun_bnd_le to transfer the per-element bound to the tail, then closing the overflow condition via explicit rounding-error arithmetic and algebraic manipulation.

Lemma finite_sum_from_bounded :
  ∀ (t : type) (l : list (ftype t))
         (fs : ftype t)
         (Hfs : sum_rel_Ft l fs),
    (∀ x, In x l →
       Binary.is_finite x = true ∧ Rabs (FT2R x) < fun_bnd t (length l)) →
    Binary.is_finite fs = true.

End NAN.