OAI/Analysis/CircleDomains/Topology/CirclePartitionBands.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Positive smoothing of local circle branches preserves the limiting bands in every comparison branch. Connected sampling patches fix the integer transition before averaging.

  1. def OAI.CircleDomainRigidity.OpenPlanePartition.adjustedCircleMix line 19
  2. theorem OAI.CircleDomainRigidity.OpenPlanePartition.circleMix_eq_adjusted line 22
  3. theorem OAI.CircleDomainRigidity.OpenPlanePartition.adjustedCircleMix_mem_interval line 35
  4. theorem OAI.CircleDomainRigidity.OpenPlanePartition.adjustedCircleMix_eventual_interval line 68