OAI/Analysis/CircleDomains/Reflection/ReflectionCoefficientExtension.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A bounded measurable coefficient on the base exterior extends over all reflected tiles. The extension is zero on the residual set and satisfies every generating reflection identity.

  1. lemma OAI.CircleDomainRigidity.exists_reflection_coefficient_extension line 14