OAI/MeasureTheory/Falconer/Radial/RadialPairSwap.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Radial Fubini for an original-label cap pair

The finite shell law and bounded measurable endpoint factors justify moving its integral inside both the angles and the original spatial labels. No spatial regularity or separation of the two angles is required.

  1. def OAI.Falconer.expandedCapTerm line 18
  2. theorem OAI.Falconer.expandedCapTerm_radial_swap line 28