PerturbedMeanPeriodGraph.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Construction of the actual closed period-level graph from a compact mean law and a shared bounded continuous smoothing correction.

theorem OAI.CircleDomainRigidity.exists_perturbed_mean_period_graph line 19