def MillerRabin.IsMillerRabinWitness (N a : ℕ) : Prop

Predicate stating that a is a Miller-Rabin witness for compositeness of N: i.e., writing N - 1 = 2^s * d with d odd and s > 0, neither a^d ≡ 1 (mod N) nor a^(2^r * d) ≡ -1 (mod N) holds for any 0 ≤ r < s.

def MillerRabin.oddIntRange (k : ℕ) : Finset ℕ

The set of odd integers in the interval [2^(k-1), 2^k].

noncomputable def MillerRabin.nonWitnessPairs (k : ℕ) : Finset (ℕ × ℕ)

The set of pairs (N, a) where N is an odd integer in [2^(k-1), 2^k], a ∈ [1, N-1], and a is not a Miller-Rabin witness for N.

noncomputable def MillerRabin.primeNonWitnessPairs (k : ℕ) : Finset (ℕ × ℕ)

The subset of nonWitnessPairs k for which N is actually prime.

theorem MillerRabin.damgard_landrock_pomerance (k : ℕ) (hk : 2 ≤ k) : ↑(primeNonWitnessPairs k).card / ↑(nonWitnessPairs k).card ≥ 1 - ↑k ^ 2 * 4 ^ (2 - √↑k)

Damgård-Landrock-Pomerance bound (Theorem 11.11): for a random odd integer N ∈ [2^(k-1), 2^k] and a random a ∈ [1, N-1], the conditional probability that N is prime given that a is not a Miller-Rabin witness for N is at least 1 - k^2 · 4^(2 - √k).