OAI/Analysis/CircleDomains/Probability/SummableErrorExtraction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A vanishing nonnegative error has an explicit summable extraction. The selected indices still tend to infinity.

  1. theorem OAI.CircleDomainRigidity.exists_summable_error_extraction line 13