OAI/Analysis/CircleDomains/Uniformization/ScalarDistributionalLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A genuine distributional limit of the constructed scalar fillings. The scalar and both L² derivative fields are obtained by weak compactness; the derivative identities follow from the vanishing actual disk errors.

  1. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.distributional_identities_of_filled_weak_limits line 22
  2. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.exists_scalar_distributional_limit line 55