OAI/MeasureTheory/Falconer/Incidence/QuarterPencilGeometry.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A fixed point contraction and its exact line map. This preserves the original incidence witnesses and the dyadic scale needed by regular gain.

  1. theorem OAI.Falconer.unlocalCellLine_four_dist line 11
  2. theorem OAI.Falconer.localCellLine_four_separated line 21
  3. theorem OAI.Falconer.localCellLine_four_regular line 33
  4. theorem OAI.Falconer.planarQuarter_eq_local line 57
  5. theorem OAI.Falconer.planarQuarter_incident line 61
  6. theorem OAI.Falconer.localCellLine_four_chart line 66