OAI/Analysis/CircleDomains/Probability/RectangleMeasurability.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Local ACL gives a measurable representative on the open rectangle. This avoids any analyticity assumption on the finite-chain infimum.

  1. theorem OAI.CircleDomainRigidity.aestronglyMeasurable_on_rectangle_of_ACL line 16