OAI/MeasureTheory/Falconer/Incidence/VariableBaselineIncidence.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The baseline incidence estimate for unequal pencil sizes, as needed before and after weighted packet freezing.

  1. theorem OAI.Falconer.planar_variable_baseline_incidence line 11
  2. theorem OAI.Falconer.packet_size_from_variable_incidence line 41