|
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
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
