OAI/Analysis/CircleDomains/Modulus/PathIntervalOscillation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The diameter of a path image on a fixed parameter set is continuous in the uniform metric. Loop deletion decreases every interval diameter.

  1. def OAI.CircleDomainRigidity.pathOscillation line 14
  2. lemma OAI.CircleDomainRigidity.path_image_isBounded line 17
  3. lemma OAI.CircleDomainRigidity.pathOscillation_le_add line 21
  4. lemma OAI.CircleDomainRigidity.lipschitzWith_pathOscillation line 35
  5. lemma OAI.CircleDomainRigidity.continuous_pathOscillation line 46
  6. lemma OAI.CircleDomainRigidity.pathOscillation_erase_le line 50
  7. lemma OAI.CircleDomainRigidity.pathOscillation_erase_eq_zero line 64