OAI/Analysis/CircleDomains/Modulus/ChainPotentialOscillation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Real-valued oscillation and topological bands of the truncated chain distance. The closure argument retains all cluster values.

  1. def OAI.CircleDomainRigidity.realChainPotential line 18
  2. theorem OAI.CircleDomainRigidity.chainPotential_ne_top line 21
  3. theorem OAI.CircleDomainRigidity.realChainPotential_mem_Icc line 25
  4. theorem OAI.CircleDomainRigidity.realChainPotential_difference line 32
  5. theorem OAI.CircleDomainRigidity.clusterGraph_oscillation_of_neighborhood line 53
  6. theorem OAI.CircleDomainRigidity.clusterGraph_oscillation_of_jumps line 68