OAI/NumberTheory/TwoPoint/Circuits/CircuitBernoulli.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The finite sampling calculation in the circuit approximation: a random subset hits a prescribed nonempty set exactly once with probability k*p*(1-p)^(k-1). No asymptotic input is used.

  1. def OAI.TwoPointCorrelations.bernoulliCubeLaw line 15
  2. lemma OAI.TwoPointCorrelations.bernoulliCubeLaw_pattern line 19
  3. def OAI.TwoPointCorrelations.singleBitPattern line 43
  4. def OAI.TwoPointCorrelations.singleHitScore line 45
  5. lemma OAI.TwoPointCorrelations.bernoulliCubeLaw_singleHitScore line 48
  6. lemma OAI.TwoPointCorrelations.single_hit_probability_lower line 76

    Source documentation

    A dyadic sampling scale with expected hit count between 1/4 and 1/2 has a uniformly positive chance of isolating one marked coordinate.

    lemma single_hit_probability_lower (k : ℕ) (hk : 0 < k) (p : ℝ)
    (hp : 0 ≤ p) (hsmall : (k : ℝ) * p ≤ 1 / 2)
    (hlarge : 1 / 4 ≤ (k : ℝ) * p) :
    1 / 8 ≤ (k : ℝ) * p * (1 - p) ^ (k - 1) := by
…