OAI/MeasureTheory/Falconer/Estimates/PacketLogBounds.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Linear depth bounds for the dyadic losses used in packet preparation.

  1. theorem OAI.Falconer.bounded_planar_card_dyadic line 10
  2. theorem OAI.Falconer.packet_log_of_card_bound line 32
  3. theorem OAI.Falconer.bounded_planar_log line 36
  4. theorem OAI.Falconer.packet_incidence_log line 41