OAI/NumberTheory/TwoPoint/Circuits/CircuitIsolation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Independent repetition amplifies the single-hit experiment. These finite identities are the random-subset step of the circuit polynomial construction.

  1. def OAI.TwoPointCorrelations.isolatesOne line 15
  2. lemma OAI.TwoPointCorrelations.singleHitScore_eq_indicator line 18
  3. theorem OAI.TwoPointCorrelations.bernoulliCubeLaw_isolatesOne line 40
  4. lemma OAI.TwoPointCorrelations.FiniteLaw.probability_complement line 50

    Distinct definitions of this name: OAI/NumberTheory/TwoPoint/Bounds/SieveModel.lean:49 (different declaration text), OAI/NumberTheory/TwoPointCorrelations/SieveModel.lean:49 (different declaration text). Qualify references as OAI.TwoPointCorrelations.FiniteLaw.probability_complement@path.

  5. theorem OAI.TwoPointCorrelations.FiniteLaw.independent_failure line 61
  6. theorem OAI.TwoPointCorrelations.FiniteLaw.independent_failure_le line 71