OAI/Analysis/CircleDomains/Selection/ControlledHeight.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Quantitative data proved for the actual nearly extremal height.

  1. structure OAI.CircleDomainRigidity.ControlledHeight line 13
  2. theorem OAI.CircleDomainRigidity.CompactScalarModel.exists_controlled_height line 31
  3. theorem OAI.CircleDomainRigidity.ControlledHeight.level_continuum line 60