OAI/Analysis/CircleDomains/Topology/RadialDiskCompression.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

An explicit ambient disk compression. Its radial formula is the identity outside the unit disk, has parameter reciprocal as inverse, and compresses every fixed smaller disk as the parameter increases.

  1. def OAI.CircleDomainRigidity.diskCompressionDenom line 17
  2. def OAI.CircleDomainRigidity.diskCompression line 19
  3. lemma OAI.CircleDomainRigidity.diskCompressionDenom_pos line 22
  4. lemma OAI.CircleDomainRigidity.diskCompression_norm line 34
  5. lemma OAI.CircleDomainRigidity.diskCompression_eq_self line 40
  6. lemma OAI.CircleDomainRigidity.diskCompressionDenom_inverse line 44
  7. lemma OAI.CircleDomainRigidity.diskCompression_inverse line 66
  8. lemma OAI.CircleDomainRigidity.diskCompression_continuous line 73
  9. def OAI.CircleDomainRigidity.diskCompressionHomeomorph line 81
  10. lemma OAI.CircleDomainRigidity.diskCompression_norm_bound line 91
  11. lemma OAI.CircleDomainRigidity.exists_disk_compression line 103