OAI/Analysis/CircleDomains/Topology/GatedMeanCollar.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The full boundary side of the law alternative. The original physical start gate supplies the lower bound, its point-avoidance supplies the atomless boundary law, and the actual smoothed mean data supplies the smooth circle coordinate.

  1. theorem OAI.CircleDomainRigidity.exists_gated_mean_collar_lower_bound line 22