OAI/Analysis/CircleDomains/Selection/PreparedHeightSelection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Choose the actual model, height, common flattenings and priority supports after fixing the cutoff constants and the desired energy budget.

  1. theorem OAI.CircleDomainRigidity.exists_small_selected_height_data line 14