OAI/Analysis/CircleDomains/Transfer/ModelPrioritySupport.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual horizontal priority selection retains both its gradient error and the energy of the altered support for the barrier estimate.

  1. theorem OAI.CircleDomainRigidity.CompactScalarModel.exists_horizontal_priority_with_support line 16