OAI/Analysis/CircleDomains/Selection/RectangleSliceData.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Fubini data for a single rectangle, retaining the actual measurable predicate and the actual L² density on almost every coordinate line.

  1. theorem OAI.CircleDomainRigidity.rectangle_ae_slices line 12
  2. theorem OAI.CircleDomainRigidity.rectangle_L2_line_integrable line 21