OAI/Analysis/CircleDomains/Selection/FlattenedHeightError.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Quantitative energy of the flattened height relative to the physical vertical coordinate. The bound tends to zero with the actual height error and the chosen flattening energy.

  1. theorem OAI.CircleDomainRigidity.norm_add_sq_le_twice line 13
  2. theorem OAI.CircleDomainRigidity.heightLimitGradient_vertical_error line 19
  3. theorem OAI.CircleDomainRigidity.ControlledHeight.flattened_energy_error line 25