====== 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).