OAI/Combinatorics/Progressions/Linear/SmoothMatrixBlockBudget.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.matrixBlock_decide_eq_classical line 12
  2. theorem OAI.Erdos3.smoothMatrixBlock_bad_probability line 17
  3. theorem OAI.Erdos3.smoothMatrixBlock_threshold_log_inv line 37
  4. theorem OAI.Erdos3.embeddedMatrixDeterminantLip_le_exp line 53
  5. def OAI.Erdos3.smoothMatrixBlockMesh line 77
  6. theorem OAI.Erdos3.smoothMatrixBlockMesh_spec line 80
  7. theorem OAI.Erdos3.smoothMatrixBlockMesh_width_spec line 92
  8. theorem OAI.Erdos3.smoothMatrixBlockMesh_inv_le_exp_of_lip_bound line 104
  9. theorem OAI.Erdos3.smoothMatrixBlockMesh_inv_le_exp line 120
  10. def OAI.Erdos3.smoothMatrixBlockConstantLogBudget line 136
  11. def OAI.Erdos3.smoothMatrixBlockThresholdLogBudget line 139
  12. theorem OAI.Erdos3.smoothMatrixBlockConstantLogBudget_nonneg line 143
  13. theorem OAI.Erdos3.smoothMatrixBlockThresholdLogBudget_nonneg line 148
  14. theorem OAI.Erdos3.shiftedSmoothSublevelConstant_le_exp line 154
  15. theorem OAI.Erdos3.smoothMatrixBlock_scale_le_exp line 171
  16. theorem OAI.Erdos3.smoothMatrixBlock_threshold_inverse_le_exp line 178
  17. def OAI.Erdos3.smoothMatrixBlockMeshLogBudget line 189
  18. def OAI.Erdos3.smoothMatrixBlockWidthLogBudget line 193
  19. theorem OAI.Erdos3.smoothMatrixBlockMeshLogBudget_nonneg line 196
  20. theorem OAI.Erdos3.smoothMatrixBlock_actual_mesh_inverse_le_exp line 202
  21. theorem OAI.Erdos3.smoothMatrixBlock_actual_width_le_exp line 211
  22. theorem OAI.Erdos3.smoothMatrixBlock_bad_probability_of_exp_width line 233