OAI/Analysis/CircleDomains/Selection/AffineResidualBounds.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Affine restriction preserves the full family of residual incidence inequalities. Rational tests in the old parameter suffice, despite the generally irrational endpoints of the retained interval.

  1. theorem OAI.CircleDomainRigidity.residualIncidenceBound_affine_open line 21
  2. theorem OAI.CircleDomainRigidity.residualConstraintFamily_affine line 44