OAI/Analysis/CircleDomains/Uniformization/ActualScalarJumpLimit.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 horizontal weak derivative identity.

  1. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.filled_horizontal_error_tendsto line 20
  2. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.horizontal_weak_limit_identity line 37