OAI/Analysis/CircleDomains/Selection/RecursiveMeanCompatibility.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A recursive positive law gives compatibility for the next smoothed mean. Generic prior intersections follow from its retained real and mean data and candidate budgets.

  1. theorem OAI.CircleDomainRigidity.RecursiveCodeLaw.mean_coordinate_compatible line 18