OAI/Analysis/CircleDomains/Selection/MeanPeriodFreeValues.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual period graph has the original mean value at every free dust point avoided by the selected law. Vanishing smoothing error leaves its limiting bands unchanged.

  1. theorem OAI.CircleDomainRigidity.period_graph_mean_free_value line 22