OAI/Analysis/CircleDomains/Probability/SliceMeasurability.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Measurability from almost-everywhere continuous horizontal sections and measurable vertical sections on a dense set. Finite simple sampling provides the measurable approximants.

  1. theorem OAI.CircleDomainRigidity.aestronglyMeasurable_of_dense_measurable_slices line 22
  2. theorem OAI.CircleDomainRigidity.aestronglyMeasurable_of_ae_continuous_slices line 49