OAI/Analysis/CircleDomains/Selection/ContinuousMeanIndexWitness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Continuous Sobolev branches of the actual descended mean circle map. Continuity is derived from avoidance of each physical point by the source law.

  1. theorem OAI.CircleDomainRigidity.continuous_meanIndex_rectangle_witness line 18