OAI/Analysis/CircleDomains/Selection/PresentedPriorLevels.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual countable real/mean presentations give generic prior-level estimates for the path law. Closedness, square-summable weights, and free weights are obtained from the stored coordinates and common marks.

  1. theorem OAI.CircleDomainRigidity.presented_prior_generic_levels line 19