OAI/Analysis/CircleDomains/Probability/RecursiveLawLevelEstimates.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A recursively selected positive law supplies the visit and deletion estimates required by all earlier real and mean levels. No generic-level assumption remains in this application.

  1. theorem OAI.CircleDomainRigidity.RecursiveCodeLaw.generic_prior_levels line 19