OAI/Analysis/CircleDomains/Selection/PriorityFinite.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Identification of the finite recursive interpolation with the priority-weight formula, for passage from local finite sums to the countable interpolation.

  1. theorem OAI.CircleDomainRigidity.priorityBlend_append line 15
  2. theorem OAI.CircleDomainRigidity.priorityResidual_append line 21
  3. theorem OAI.CircleDomainRigidity.priorityBlend_sub line 27
  4. def OAI.CircleDomainRigidity.priorityList line 39
  5. theorem OAI.CircleDomainRigidity.priorityList_succ line 42
  6. theorem OAI.CircleDomainRigidity.priorityList_residual line 46
  7. theorem OAI.CircleDomainRigidity.priorityList_value line 54
  8. theorem OAI.CircleDomainRigidity.priorityInfiniteValue_eq_finite line 69