OAI/Analysis/CircleDomains/Probability/NullImage.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Null images from connected-neighborhood oscillation bounds

The measure part of the trace-null argument: split an open neighborhood into its countably many connected components and pay for the diameter of each real image by the measure of its component. No measurability of the trace function or of its image is assumed.

  1. theorem OAI.CircleDomainRigidity.null_image_of_connected_open_oscillation line 19