OAI/Analysis/CircleDomains/LengthArea.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Circle domains, conformal removability, and conditional analytic rigidity from length and area estimates.

  1. abbrev OAI.CircleDomainRigidity.Sphere line 13

    Also declared: ComparatorChallenges/KoebeCircleDomains.lean:13 (same declaration text).

  2. abbrev OAI.CircleDomainRigidity.Mobius line 14

    Also declared: ComparatorChallenges/KoebeCircleDomains.lean:14 (same declaration text).

  3. def OAI.CircleDomainRigidity.sphereInv line 16

    Also declared: ComparatorChallenges/KoebeCircleDomains.lean:16 (same declaration text).

  4. def OAI.CircleDomainRigidity.finiteCoord line 19

    Also declared: ComparatorChallenges/KoebeCircleDomains.lean:19 (same declaration text).

  5. def OAI.CircleDomainRigidity.chart line 21

    Also declared: ComparatorChallenges/KoebeCircleDomains.lean:21 (same declaration text).

  6. def OAI.CircleDomainRigidity.chartSymm line 24

    Also declared: ComparatorChallenges/KoebeCircleDomains.lean:24 (same declaration text).

  7. def OAI.CircleDomainRigidity.IsConformalAt line 27

    Also declared: ComparatorChallenges/KoebeCircleDomains.lean:27 (same declaration text).

  8. def OAI.CircleDomainRigidity.IsConformalOn line 31

    Also declared: ComparatorChallenges/KoebeCircleDomains.lean:31 (same declaration text).

  9. def OAI.CircleDomainRigidity.IsConformalEquivalence line 34

    Also declared: ComparatorChallenges/KoebeCircleDomains.lean:34 (same declaration text).

  10. def OAI.CircleDomainRigidity.IsRoundClosedDisk line 39

    Also declared: ComparatorChallenges/KoebeCircleDomains.lean:39 (same declaration text).

  11. def OAI.CircleDomainRigidity.IsCircleDomain line 44

    Also declared: ComparatorChallenges/KoebeCircleDomains.lean:44 (same declaration text).

  12. def OAI.CircleDomainRigidity.OrientationPreserving line 49

    Also declared: ComparatorChallenges/KoebeCircleDomains.lean:49 (same declaration text).

  13. def OAI.CircleDomainRigidity.IsConformallyRemovable line 52

    Also declared: ComparatorChallenges/KoebeCircleDomains.lean:52 (same declaration text).

  14. theorem OAI.CircleDomainRigidity.IsConformalOn.mono line 56
  15. theorem OAI.CircleDomainRigidity.IsConformallyRemovable.of_isCompact_subset line 60
  16. theorem OAI.CircleDomainRigidity.isCircleDomain_univ line 66
  17. theorem OAI.CircleDomainRigidity.LengthArea.summable_mul_of_squares line 77
  18. theorem OAI.CircleDomainRigidity.LengthArea.hasSum_square_discrepancy line 86
  19. theorem OAI.CircleDomainRigidity.LengthArea.discrepancy_nonpos line 95
  20. theorem OAI.CircleDomainRigidity.LengthArea.equality_of_estimates line 114
  21. theorem OAI.CircleDomainRigidity.LengthArea.norm_deriv_eq_one_of_ae line 145
  22. theorem OAI.CircleDomainRigidity.LengthArea.affine_of_unit_derivative_on_open line 152
  23. theorem OAI.CircleDomainRigidity.LengthArea.affine_coefficients_of_principal_normalization line 176
  24. theorem OAI.CircleDomainRigidity.LengthArea.eq_id_of_affine_and_principal_normalization line 198
  25. theorem OAI.CircleDomainRigidity.LengthArea.affine_of_length_area_estimates line 212
  26. theorem OAI.CircleDomainRigidity.LengthArea.identity_of_length_area_estimates line 230