OAI/Analysis/CircleDomains/Topology/SphereCoefficient.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Borel complex coefficient fields on the concrete sphere, with an explicit value at infinity.

  1. def OAI.CircleDomainRigidity.sphereCoefficient line 16
  2. lemma OAI.CircleDomainRigidity.sphereCoefficient_coe line 18
  3. lemma OAI.CircleDomainRigidity.sphereCoefficient_infty line 21
  4. lemma OAI.CircleDomainRigidity.sphereCoefficient_measurable line 24
  5. def OAI.CircleDomainRigidity.circleReflectionPhase line 35
  6. def OAI.CircleDomainRigidity.sphereReflectionPhase line 38
  7. lemma OAI.CircleDomainRigidity.circleReflectionPhase_norm line 41
  8. lemma OAI.CircleDomainRigidity.sphereReflectionPhase_norm line 48
  9. lemma OAI.CircleDomainRigidity.circleReflectionPhase_measurable line 53
  10. lemma OAI.CircleDomainRigidity.sphereReflectionPhase_measurable line 58
  11. lemma OAI.CircleDomainRigidity.roundDiskReflection_infty line 61
  12. lemma OAI.CircleDomainRigidity.roundDiskReflection_center line 68
  13. lemma OAI.CircleDomainRigidity.sphereReflectionPhase_reflection line 72