OAI/Analysis/CircleDomains/Probability/RecursiveLawConstruction.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Insert the actual prior-law presentation into the path-code data, and retain all quantitative outputs of the positive-law theorem in a recursion stage.

  1. def OAI.CircleDomainRigidity.endpointCodeData line 19
  2. def OAI.CircleDomainRigidity.RecursiveCodeGeometry.of_presentation line 31
  3. def OAI.CircleDomainRigidity.positiveRecursiveBudgets line 51
  4. def OAI.CircleDomainRigidity.RecursiveCodeLaw.of_positive_candidate line 63