From 54ddf3b072430e225360d8e0e25a2d990d07cfc8 Mon Sep 17 00:00:00 2001
From: Kjetil Orbekk <kjetil.orbekk@gmail.com>
Date: Sun, 27 Aug 2017 14:17:27 -0400
Subject: Add: induction argument

---
 src/main.rs | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/src/main.rs b/src/main.rs
index eda1c01..9243c1f 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -27,7 +27,21 @@ fn some<R: rand::Rng, T: Iterator<Item = Result<String, io::Error>>>(
             let victim = r.gen_range(0, n);
             result.remove(victim);
             push(&mut result, n, line);
+
+            // Assumption: |result| contains m random elements from the (i-1)
+            // first lines.
+            //
+            // |line| is in result with n/i probability (if expression)
         }
+        // An arbitrary line0 occuring before line was in result with
+        // probability m/(i-1).
+        //
+        // P(line0 is still in result) =
+        //   m/i * (1 - 1/m) + (1 - m/i) =
+        //   m/i - 1/i + 1 - m/i = 1 - 1/i = (i-1) / i
+        //
+        // The probability that an arbitrary line from the i first lines is in
+        // |result| is: m/(i-1) * ((i-1)/i) = m/i. The induction holds.
     }
     return Ok(result);
 }
-- 
cgit v1.2.3