Quelle real_finite_sequences.pvs Sprache: PVS

real_finite_sequences: THEORY

  BEGIN

  IMPORTING ordered_finite_sequences[real, <=], reals@sigma_below

  s, s1, s2: VAR ne_seqs
  cf, cf1, cf2: VAR consensus_function

  eps, delta: VAR nnreal
  k: VAR posnat
  i: VAR nat

  diameter?(s): nnreal = max(s) - min(s)

% diameter?(s1 o s2)

  agreement_propagation: LEMMA
    cf1(s1) - cf2(s2) <= max(s1) - min(s2)

  similar?(s1, s2, eps): bool =
    (s1`length = s2`length) AND
    FORALL (i: below(s1`length)):
      s1`seq(i) - s2`seq(i) <= eps

  similar_sort: LEMMA
    similar?(s1, s2, eps) IMPLIES similar?(sort(s1), sort(s2), eps)

%  similar_reduce: LEMMA
%    similar?(s1, s2, eps) IMPLIES similar?(reduce(tau)(s1), reduce(tau)(s2), eps)

  inexact_consensus?(cf): bool =
    FORALL s1, s2, eps: similar?(s1, s2, eps) IMPLIES cf(s1) - cf(s2) <= eps

  sum(s): real = sigma[below(s`length)](0, s`length - 1, s`seq)

  sum_lower: LEMMA max(s) + (s`length - 1) * min(s) <= sum(s)
  sum_upper: LEMMA sum(s) <= (s`length - 1) * max(s) + min(s)

  mean(s): real = sum(s) / s`length

  min_le_mean: LEMMA min(s) <= mean(s)
  mean_le_max: LEMMA mean(s) <= max(s)

  midpoint(s) : real = mean(minmax(s))

  midpoint_def: LEMMA midpoint(s) = (min(s) + max(s)) / 2

  mean_lower: LEMMA s`length <= k IMPLIES (max(s) + (k - 1) * min(s)) / k <= mean(s)
  mean_upper: LEMMA s`length <= k IMPLIES mean(s) <= ((k - 1) * max(s) + min(s)) / k

  mean_consensus:     JUDGEMENT mean     HAS_TYPE consensus_function
  midpoint_consensus: JUDGEMENT midpoint HAS_TYPE consensus_function

  inexact_min:      LEMMA inexact_consensus?(min)
  inexact_max:      LEMMA inexact_consensus?(max)
  inexact_choose:   LEMMA inexact_consensus?(choose(i))
  inexact_mean:     LEMMA inexact_consensus?(mean)
  inexact_midpoint: LEMMA inexact_consensus?(midpoint)

  mean_convergence: THEOREM
      s1`length <= k AND
      s2`length <= k AND
      max(s1) - min(s2) <= delta + eps AND
      min(s1) - max(s2) <= eps
    IMPLIES
      mean(s1) - mean(s2) <= delta * (k - 1) / k + eps

  midpoint_convergence: COROLLARY
      max(s1) - min(s2) <= delta + eps AND
      min(s1) - max(s2) <= eps
    IMPLIES
      midpoint(s1) - midpoint(s2) <= delta / 2 + eps

  convergent?(cf, i, k): bool =
    FORALL s1, s2, delta, eps:
      s1`length <= i AND
      s2`length <= i AND
      max(s1) - min(s2) <= delta + eps AND
      min(s1) - max(s2) <= eps
    IMPLIES
      cf(s1) - cf(s2) <= delta * (k - 1) / k + eps

  convergent_mean    : LEMMA convergent?(mean, k, k + i)
  convergent_midpoint: LEMMA convergent?(midpoint, i, 2)


  END real_finite_sequences

quality97%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.