OAI/Analysis/CircleDomains/Selection/RealBandPaidThreshold.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual real-coordinate band levels satisfy the paid-threshold conclusion used in the local variation argument.

  1. theorem OAI.CircleDomainRigidity.real_band_paid_threshold line 14