OAI/MeasureTheory/Falconer/Graphs/CommonRowNormalization.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Normalize the rounded product rows into the bounded line chart without changing their first coordinate. All size losses are explicit.

  1. def OAI.Falconer.verticalQuarter line 10
  2. def OAI.Falconer.verticalFour line 11
  3. theorem OAI.Falconer.verticalQuarter_zero line 13
  4. theorem OAI.Falconer.verticalQuarter_one line 14
  5. theorem OAI.Falconer.verticalFour_verticalQuarter line 16
  6. theorem OAI.Falconer.verticalQuarter_verticalFour line 23
  7. theorem OAI.Falconer.verticalQuarter_injective line 30
  8. theorem OAI.Falconer.verticalQuarter_row_distance line 33
  9. theorem OAI.Falconer.verticalQuarter_row_separated line 46
  10. theorem OAI.Falconer.verticalQuarter_row_regular line 56
  11. theorem OAI.Falconer.quarter_adjusted_incident line 88
  12. theorem OAI.Falconer.quarter_adjusted_chart line 105