====== std.theorem123 — das 123-Theorem ======
Das **123-Theorem** (Alon/Yuster 1995) begrenzt, wie stark sich die Nähewahrscheinlichkeit zweier unabhängiger, identisch verteilter Zufallsvariablen bei größerem Abstand steigern kann:
P(|X - Y| <= 2) < 3 * P(|X - Y| <= 1)
allgemein, für 0 < a < b:
P(|X - Y| <= b) < (2 * ceil(b/a) - 1) * P(|X - Y| <= a)
Die Ungleichung ist **strikt**, und die Konstante lässt sich nicht verbessern: sie wird beliebig genau erreicht, aber nie angenommen. Genau das macht sie als **Prüfung** brauchbar — wer eine Schätzung hat, die die Schranke erreicht oder überschreitet, hat einen Fehler in der Schätzung, kein Gegenbeispiel zum Theorem.
Seit lyxc 1.1.13B. → [[lyx_-_programmiersprache:units|Units]] · [[lyx_-_programmiersprache:units:math|std.math]] · [[lyx_-_programmiersprache:units:alloc|std.alloc]]
----
===== 1. Funktionen =====
^ Funktion ^ Bedeutung ^
| ''T123NahePaarStichprobe(data, n, t): f64'' | ''P(%%|%%X−Y%%|%% ≤ t)'' für eine Stichprobe: ''data'' zeigt auf ''n'' aneinandergereihte ''f64'', jeder Wert trägt ''1/n'' |
| ''T123NahePaar(werte, gewichte, n, t): f64'' | dasselbe für eine **gewichtete** Verteilung; die Gewichte dürfen um höchstens ''1e-9'' von 1 abweichen |
| ''T123Schranke(a, b): f64'' | ''2 * ceil(b/a) − 1'' — für ''a=1, b=2'' ergibt das die namensgebende **3** |
| ''T123VerhaeltnisStichprobe(data, n, a, b): f64'' | ''P(≤b) / P(≤a)'' — die Zahl, die das Theorem begrenzt |
| ''T123VerhaeltnisGewichtet(werte, gewichte, n, a, b): f64'' | dasselbe für die gewichtete Form |
| ''T123Gilt(werte, gewichte, n): bool'' · ''T123GiltStichprobe(data, n): bool'' | der Fall ''a=1, b=2'' |
| ''T123GiltAllgemein(werte, gewichte, n, a, b): bool'' | freie Wahl von ''a'' und ''b'' |
| ''T123Fehlerwert(): f64'' · ''T123IstFehler(x): bool'' | NaN als Fehlerwert erzeugen und erkennen |
===== 2. Beispiel =====
import std.theorem123;
import std.alloc;
fn main(): int64 {
var n: int64 := 5;
var data: int64 := alloc(n * 8);
var i: int64 := 0;
while (i < n) {
pokef64(data + i * 8, (i as f64) * 0.75);
i := i + 1;
}
Print("P(|X-Y| <= 1) = "); PrintF64(T123NahePaarStichprobe(data, n, 1.0));
Print("P(|X-Y| <= 2) = "); PrintF64(T123NahePaarStichprobe(data, n, 2.0));
Print("Verhaeltnis = "); PrintF64(T123VerhaeltnisStichprobe(data, n, 1.0, 2.0));
Print("Schranke(1,2) = "); PrintF64(T123Schranke(1.0, 2.0));
if (T123GiltStichprobe(data, n)) { PrintLn("Theorem haelt"); }
free(data, n * 8);
return 0;
}
P(|X-Y| <= 1) = 0.520000
P(|X-Y| <= 2) = 0.760000
Verhaeltnis = 1.461538
Schranke(1,2) = 3.000000
Theorem haelt
===== 3. Drei Punkte, die man wissen muss =====
* **Die Diagonale zählt mit.** Gezählt werden alle ''n×n'' geordneten Paare, ''i == j'' eingeschlossen. Das ist die Definition: ''X'' und ''Y'' sind unabhängig, sie dürfen denselben Wert treffen. Wer die Diagonale weglässt, rechnet „zwei Züge ohne Zurücklegen" — eine andere Größe, und für kleine ''n'' eine deutlich andere.
* **Die Schranke springt.** Sie hängt nur davon ab, //wie oft// ''a'' in ''b'' passt, nicht vom genauen Verhältnis: für ''b/a'' knapp über einer ganzen Zahl springt sie um 2 nach oben. Kein Rundungsfehler, sondern die Aussage.
* **Ein ''false'' ist eine Aussage über die Eingabe, nicht über das Theorem.** Das Theorem ist bewiesen; wer hier durchfällt, hat falsche Gewichte, vertauschte Werte oder einen zu kurzen Puffer. Deshalb meldet die Unit den Fall zusätzlich auf stderr, statt nur ''false'' zu liefern. Fehler kommen als **NaN** zurück (''T123IstFehler'').
> **Warum der Fehlerwert eine Funktion ist und keine ''con''.** Eine Rechnung im Initialisierer einer ''f64''-''con'' wird still falsch übersetzt: ''0.0 / 0.0'' kommt als ''0.0'' an, ''0.0 - 0.5'' als ''-8.0'', ''2.0 * 3.0'' als ''0.0'' (gemessen mit 1.1.13A, [[https://github.com/SEOLizer/LyX-Compiler/issues/1853|#1853]]). Reine Literale stimmen. ''T123Fehlerwert()'' rechnet das NaN deshalb aus **Variablen** — der Weg, der nachweislich trägt. Ein ''-1'' als Fehlerwert wäre keine Alternative: es ist eine gültige Zahl, und ''0'' beziehungsweise ''1'' würden als „nie" und „immer" gelesen — beides plausibel, beides falsch.
----
Letzte Aktualisierung: 2026-08-30 — Seite neu angelegt; Signaturen aus ''std/theorem123.lyx'', Beispiel gegen lyxc 1.1.14A gebaut und gelaufen.
Codebeispiele geprüft: gegen **lyxc 1.2.5C** übersetzt (Prüflauf 2026-09-08 über die gesamte Doku: 574 Vollprogramme, 0 echte Fehler; zusätzlich 5159 Aufrufe gegen die ''pub fn''-Signaturen in ''aurum/std'' gehalten, 0 Abweichungen).