HammingException.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.sum_pow_hammingDist line 9

Source documentation

The Hamming-distance generating polynomial of a Boolean cube.

theorem sum_pow_hammingDist {m : ℕ} (x : Fin m → Bool) (t : ℝ) :
    (∑ y : Fin m → Bool, t ^ hammingDist x y) = (1 + t) ^ m := by
…

theorem OAI.Problem337.sum_pairs_pow_hammingDist line 24

Source documentation

The exact exponential moment for uniformly counted pairs of Boolean strings.

theorem sum_pairs_pow_hammingDist (m : ℕ) (t : ℝ) :
    (∑ xy : (Fin m → Bool) × (Fin m → Bool), t ^ hammingDist xy.1 xy.2) =
      (2 * (1 + t)) ^ m := by
…

theorem OAI.Problem337.hamming_chernoff_factor line 35
Source documentation
A numerical Chernoff estimate with the constants used in the manuscript.
```
theorem hamming_chernoff_factor (m : ℕ) :
    (2 : ℝ) ^ ((m : ℝ) / 4) * (3 / 4 : ℝ) ^ m ≤
      Real.exp (-(m : ℝ) / 16) := by
…
```

theorem OAI.Problem337.hamming_exception_count line 49

Source documentation

Fewer than one quarter differing coordinates is an exponentially small fraction of all ordered pairs of Boolean strings.

theorem hamming_exception_count (m : ℕ) :
    ((Finset.univ.filter (fun xy : (Fin m → Bool) × (Fin m → Bool) =>
      (hammingDist xy.1 xy.2 : ℝ) < (m : ℝ) / 4)).card : ℝ) ≤
      (4 : ℝ) ^ m * Real.exp (-(m : ℝ) / 16) := by
…