OAI/Analysis/CircleDomains/Selection/ReversedResidualBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Reversal preserves the residual inequalities, with exactly reversed test intervals and unchanged parameter multiplicity.

  1. theorem OAI.CircleDomainRigidity.image_symm_Icc line 17
  2. theorem OAI.CircleDomainRigidity.residualIncidenceBound_reversed line 29
  3. theorem OAI.CircleDomainRigidity.residualConstraintFamily_reversed line 40