OAI/Combinatorics/Progressions/Estimates/CanonicalCubeMinorThreshold.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.cubeMinorProbabilityConstant line 10
  2. def OAI.Erdos3.cubeMinorProbabilityScale line 14
  3. theorem OAI.Erdos3.cubeMinorProbabilityConstant_pos line 17
  4. theorem OAI.Erdos3.cubeMinorProbabilityScale_pos line 22
  5. def OAI.Erdos3.cubeMinorThreshold line 27
  6. theorem OAI.Erdos3.cubeMinorThreshold_pos line 32
  7. theorem OAI.Erdos3.cubeMinorThreshold_le_half line 39
  8. theorem OAI.Erdos3.cubeMinorThreshold_log_inv line 46
  9. theorem OAI.Erdos3.exists_cube_minor_thresholds line 67
  10. def OAI.Erdos3.cubeMinorVariableCount line 124
  11. def OAI.Erdos3.cubeMinorDegree line 127
  12. def OAI.Erdos3.canonicalCubeMinorThreshold line 130
  13. theorem OAI.Erdos3.canonicalCubeMinorThreshold_pos line 134
  14. theorem OAI.Erdos3.canonicalCubeMinorThreshold_le_half line 140
  15. theorem OAI.Erdos3.exists_canonical_cube_minor_thresholds line 146