OAI/MeasureTheory/Falconer/Incidence/FrozenPacketProduct.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Product counting for a local union carried by globally frozen packets. The local factor is arbitrary; no local incidence estimate is assumed.

  1. theorem OAI.Falconer.frozen_packet_card_product line 11