OAI/MeasureTheory/Falconer/Incidence/WeakCoarsePacketGain.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The coarse packet gain with all numerical application costs absorbed into a single weak-regularity exponent.

  1. theorem OAI.Falconer.weak_coarse_packet_gain line 12