OAI/Analysis/CircleDomains/Sobolev/SmoothMeanCodeLevels.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Generic prior levels for the actual smoothed mean and its masked coordinate. The atlas and its weight estimates are derived from that coordinate, not supplied as a generic-intersection hypothesis.

  1. theorem OAI.CircleDomainRigidity.SmoothMeanPeriodData.ranked_code_generic_levels line 18