VariableWeightedPullback.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform distortion suffices for strong L2 convergence under a varying sequence of smooth weighted pullbacks. This applies to the actual inverse principal approximants in the reflection-conjugacy calculation.

lemma OAI.CircleDomainRigidity.exists_strong_variable_weighted_pullback line 14