OAI/MeasureTheory/Falconer/Estimates/PlanarSampling.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Original labels, slope coordinates and prescribed strip covers

These adapters connect the two uniform sampling stages to the exact finite Furstenberg obstruction. Every strip list remains indexed by its original direction label, including when slope coordinates coincide.

  1. def OAI.Falconer.slopePoint line 18
  2. theorem OAI.Falconer.slopePoint_zero line 20
  3. theorem OAI.Falconer.slopePoint_one line 21
  4. theorem OAI.Falconer.continuous_slopePoint line 23
  5. theorem OAI.Falconer.slopePoint_dist line 28
  6. theorem OAI.Falconer.slopePoint_ball_mass_le line 33
  7. def OAI.Falconer.incidentLabels line 44
  8. theorem OAI.Falconer.empirical_incidence_eq_card line 48
  9. theorem OAI.Falconer.empirical_incidence_card_lower line 56
  10. def OAI.Falconer.stripLineCandidates line 65
  11. theorem OAI.Falconer.stripLineCandidates_card_le line 68
  12. theorem OAI.Falconer.roundedIncidentLine_mem_stripLineCandidates line 75