OAI/Analysis/CircleDomains/Rigidity/MeanCircleNullTrace.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual circle-valued mean has Haar-null free traces on each locally connected prior continuum. Two explicit argument cuts cover the punctured mask, so no family of local branches is assumed.

  1. theorem OAI.CircleDomainRigidity.mean_circle_null_trace_on_continuum line 22