OAI/Combinatorics/Progressions/Probability/JointBooleanCutoffLaw.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.cutoff_loss_of_density_mass line 12
  2. theorem OAI.Erdos3.density_cutoff_test_error line 26
  3. def OAI.Erdos3.booleanCubeCutoff line 54
  4. theorem OAI.Erdos3.booleanCubeCutoff_contDiff line 60
  5. theorem OAI.Erdos3.booleanCubeCutoff_range line 68
  6. theorem OAI.Erdos3.booleanCubeGoodWeight_measure line 75
  7. def OAI.Erdos3.jointBooleanCutoff line 113
  8. theorem OAI.Erdos3.jointBooleanCutoff_contDiff line 120
  9. theorem OAI.Erdos3.jointBooleanCutoff_range line 128
  10. theorem OAI.Erdos3.jointBooleanGoodWeight_measure line 137
  11. theorem OAI.Erdos3.jointBooleanGoodWeight_test_error line 167