OAI/Analysis/CircleDomains/Transfer/ModelSelectedBounds.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Uniform bounds on the actual selected priority traces. The selected horizontal values are values on the model complement, not extra data.

  1. theorem OAI.CircleDomainRigidity.CompactScalarModel.outside_of_projection_outside line 15
  2. theorem OAI.CircleDomainRigidity.CompactScalarModel.finiteCoord_bound_of_projection_outside line 20
  3. theorem OAI.CircleDomainRigidity.CompactScalarModel.horizontalSection_trace_bound line 29
  4. theorem OAI.CircleDomainRigidity.CompactScalarModel.FlattenedSourceSelection.value_bound line 38
  5. theorem OAI.CircleDomainRigidity.CompactScalarModel.FlattenedSourceSelection.priority_trace_bound line 51