OAI/Analysis/CircleDomains/Topology/DyadicPathApproximation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Dyadic subdivision with quantitative oscillation and pointwise error preservation when two replacement paths are concatenated.

  1. def OAI.CircleDomainRigidity.leftHalf line 16
  2. def OAI.CircleDomainRigidity.rightHalf line 17
  3. lemma OAI.CircleDomainRigidity.dist_leftHalf line 19
  4. lemma OAI.CircleDomainRigidity.dist_rightHalf line 25
  5. def OAI.CircleDomainRigidity.dyadicSmallOscillation line 31
  6. lemma OAI.CircleDomainRigidity.dyadicSmallOscillation_of_modulus line 36
  7. lemma OAI.CircleDomainRigidity.exists_dyadicSmallOscillation line 60
  8. lemma OAI.CircleDomainRigidity.path_trans_pointwise_error line 70