OAI/Analysis/CircleDomains/Uniformization/ActualVerticalJumpLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The constructed finite fillings have vanishing distributional errors. Consequently every weak limit of their two pairings satisfies the vertical weak derivative identity.

  1. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.filled_vertical_error_tendsto line 20
  2. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.vertical_weak_limit_identity line 37