OAI/Analysis/CircleDomains/Selection/SelectedHeightError.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The selected flattening and the nearly maximal deficit give an actual transported error witness with the prescribed small source energy.

  1. theorem OAI.CircleDomainRigidity.height_error_energy_mono line 14
  2. theorem OAI.CircleDomainRigidity.CompactScalarModel.FlattenedSourceSelection.exists_small_height_error line 26