OAI/MeasureTheory/Falconer/Measures/PacketProductPower.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The product gain applies to the original fine pencils of a coarse packet. The proof constructs their row pencils by dilation and retains control of the actual original union.

  1. theorem OAI.Falconer.packet_product_power line 12