OAI/Analysis/CircleDomains/Selection/SelectedOldError.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The selected old coordinates obey the requested uniform and gradient norm errors, after choosing the squared energy budget below the tolerance.

  1. theorem OAI.CircleDomainRigidity.CompactScalarModel.FlattenedSourceSelection.old_errors line 15